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" <[email protected]> wrote:
> On 12 Jun 2015, at 7:11 , Raoul Duke <[email protected]> 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 > [email protected] > https://sel4.systems/lists/listinfo/devel >
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
