L4-based microkernel on Intel SCC

2014-06-04 Thread Masti Ramya Jayaram
Hi all, In fact, I am looking for a micro-kernel based hypervisor (like L4:pistachio or Fiasco) to run on the SCC. The only pointer I found was a port of Fiasco OS for Intel SCC recently (http://os.inf.tu-dresden.de/papers_ps/partheymueller-beleg.pdf) and would like to try this. I had a few

Re: l4re compilation

2014-06-04 Thread Ramya Masti
Adam Lackorzynski adam at os.inf.tu-dresden.de writes: Yes, please stick with 4.8 for now. Adam Thanks Adam! I will try that then. ___ l4-hackers mailing list l4-hackers@os.inf.tu-dresden.de

Re: Question about cross core IPC

2014-06-04 Thread Yuxin Ren
Thank you for your reply. But I think you misunderstand my questions. First, my question is whether there is a lock. Are you sure there is no lock for sender_list? I think the data has to be manipulated by multiple context as we can send to the same receiver at the same time in different cores.

seL4 will go open source on 29 July

2014-06-04 Thread Gernot Heiser
… via the portal http://sel4.systems. This site will start accumulating info through the next few weeks, please check there for updates (or subscribe to the mailing list). For those who haven’t heard about seL4: - it’s the latest L4 microkernel developed by NICTA. - according to the

Re: seL4 will go open source on 29 July

2014-06-04 Thread Sartakov A. Vasily
Hello. This is a really great news. Will you publish the haskell model and proof? … via the portal http://sel4.systems. This site will start accumulating info through the next few weeks, please check there for updates (or subscribe to the mailing list). For those who haven’t heard

Re: seL4 will go open source on 29 July

2014-06-04 Thread Gernot Heiser
On 5 Jun 2014, at 14:23 , Sartakov A. Vasily sarta...@ksyslabs.org wrote: This is a really great news. Will you publish the haskell model and proof? Yes, the lot! Gernot signature.asc Description: Message signed with OpenPGP using GPGMail ___