L4-based microkernel on Intel SCC
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 questions though: a. Is the public version of fiasco compatible with the SCC? If not, is it possible to get it? b. Since SCC uses a different compiler set (much older than gcc 4.4), does the compilation work out of the box? c. Finally, has anyone run L4Linux on top of the SCC? Thanks in advance, Ramya ___ l4-hackers mailing list l4-hackers@os.inf.tu-dresden.de http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
Re: l4re compilation
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 http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
Re: Question about cross core IPC
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. Of course there may be not lock even for multicore, but I do not think only disable interrupt is enough. If there is no lock, I want to know how they do cross core synchronization without locks. Second, IPI operations are useful for me. But I also want to know the code on IPC path to use IPI. Can you tell me where is the code on IPC path to invoke IPI operations? Thanks so much. On Tue, Jun 3, 2014 at 5:57 PM, Adam Lackorzynski a...@os.inf.tu-dresden.de wrote: Hi, On Sun Jun 01, 2014 at 05:15:06 -0800, Yuxin Ren wrote: I am learning the IPC code in the Fiasco kernel. I have some questions here. If the receiver is not ready, we will add the sender to the sender_list. But I did find any lock to protect the sender_list. So if two threads at different cores try to add themselves to the sender_list at the same time, how can we guarantee the we are safe to do so? So if there's no lock then the data structure will only ever be manipulated by a single context (and preemption disabled as required). When sender and receiver are at different cores, we have to use IPI to communicate. Where is the code on IPC path to use IPI? I imagine the code around IPI should be complex, so it is great if someone can tell me the logic about it, especially about how we protect data structures, using locks or any other lock-free algorithm. Ipi is the base class that implements IPI functionality. So for example see for Ipi::send in context.cpp. Around that are functions that allow to call functions on remote cores etc, also in context.cpp. Adam -- Adam a...@os.inf.tu-dresden.de Lackorzynski http://os.inf.tu-dresden.de/~adam/ ___ l4-hackers mailing list l4-hackers@os.inf.tu-dresden.de http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers ___ l4-hackers mailing list l4-hackers@os.inf.tu-dresden.de http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
seL4 will go open source on 29 July
… 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 performance figures on http://l4hq.org, it’s the fastest L4 kernel around (let me know if you have performance data to contribute) - it’s the world’s first and only OS kernel with a formal security proof, extending from high-level statements of confidentiality and integrity enforcement all the way down to the binary - it’s proved functionally correct (i.e. bug-free implementation of the spec) - it’s the first and only protected-mode OS with a complete and sound timing analysis, and as such the only credible platform on which to do hard real-time in protected mode - it’s the foundation for DARPA’s high-assurance UAV project (http://trustworthy.systems/projects/TS/SMACCM/) … and it will soon be free! Gernot___ l4-hackers mailing list l4-hackers@os.inf.tu-dresden.de http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
Re: seL4 will go open source on 29 July
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 about seL4: - it’s the latest L4 microkernel developed by NICTA. - according to the performance figures on http://l4hq.org, it’s the fastest L4 kernel around (let me know if you have performance data to contribute) - it’s the world’s first and only OS kernel with a formal security proof, extending from high-level statements of confidentiality and integrity enforcement all the way down to the binary - it’s proved functionally correct (i.e. bug-free implementation of the spec) - it’s the first and only protected-mode OS with a complete and sound timing analysis, and as such the only credible platform on which to do hard real-time in protected mode - it’s the foundation for DARPA’s high-assurance UAV project (http://trustworthy.systems/projects/TS/SMACCM/) … and it will soon be free! -- Sartakov A. Vasily sarta...@ksyslabs.org signature.asc Description: Message signed with OpenPGP using GPGMail ___ l4-hackers mailing list l4-hackers@os.inf.tu-dresden.de http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
Re: seL4 will go open source on 29 July
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 ___ l4-hackers mailing list l4-hackers@os.inf.tu-dresden.de http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
