It would be particularly neat to do a fault-tolerant implementation of the
seL4 API and a refinement proof that it implemented the spec when the
number of concurrent failures was limited.
On Jun 12, 2015 4:40 AM, "Gernot Heiser"
On 12 Jun 2015, at 7:11 , Raoul Duke
wrote: In general, a high-availability system should have the following software services I want to develop a high-availability system on seL4, can anyone give me some suggestions?
Does that have to all be in the OS? To what degree could it be a library independed of OS?
What is the “OS” becomes a bit relative with a true microkernel (which QNX isn’t). But you’re right if you think this should certainly not be part of the *kernel*.
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