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 <[email protected]
<mailto:[email protected]>> wrote:
On 4 Nov 2015, at 17:43 , Adrian Danis <[email protected]
<mailto:[email protected]>> 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
[email protected]
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
