You can find the seL4 code on github at www.github.com/seL4/seL4, more information about it, as well as how to use it, can be found at http://sel4.systems/

Please note that the current multi-kernel implementation by Michael Von Tessin is only for the x86 architecture, and we do not have any published source code to provide examples on how to use it.

The existing multi-kernel code is more or less considered legacy at this point, and will be removed from the code base at some point in the future. There is a student currently investigating better and more appropriate ways to support a multi-kernel seL4, although it is unclear how long until this leads to an actual implementation.

While we have no examples, here are some links to places in the seL4 kernel code that should give you a place to get started reading and understanding how the implementation works, and then how to use it.
https://github.com/seL4/seL4/blob/master/Kconfig#L237
https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/cmdline.c#L162
https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/cmdline.c#L172
https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/bootinfo.h#L51
https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/bootinfo.h#L56

Adrian

On Thu 05-Nov-2015 5:26 AM, Mehdi Amiri wrote:

Dear Adrian,
Regarding the sel4 multi kernel experience,  I have read the paper from Michael von Testing "The clustered multikernel..", is the multi kernel code available somewhere ?
Best Regards
Mehdi


On Wed, Nov 4, 2015, 10:59 Gernot Heiser <gernot@nicta.com.au> wrote:
On 4 Nov 2015, at 17:43 , Adrian Danis <Adrian.Danis@nicta.com.au> wrote:

The kernel is indeed not reentrant and always runs with interrupts disabled whilst in the kernel. This lock is an old artifact from an experiment where seL4 was ran as a multikernel across multiple CPU nodes.

a proper multicore implementation is on the roadmap and scheduled for release in the near future

Gernot


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel


_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel