Thanks for the information.  Looking at eChronos now.

>
> ---------- Forwarded message ----------
> From: <[email protected]>
> To: <[email protected]>
> Cc:
> Bcc:
> Date: Sun, 20 Aug 2017 23:57:34 +0000
> Subject: Re: [seL4] mpu vs mmu
>
> > On 21 Aug 2017, at 8:05 am, [email protected] wrote:
> >
> > On 21 Aug 2017, at 03:00, Thomas Dundon <[email protected]> wrote:
> >>
> >> Does an MPU, e.g. on a Cortex M3, provide enough functionality to
> support seL4?
> >
> > No, it doesn’t. The seL4 model is fundamentally based on the ability to
> virtualise hardware resources.
> >
> > If you don’t have that, then you can’t dod much more than a
> memory-protected RTOS. If you’re after an RTOS with a (not yet complete)
> verification story, look at eChronos: https://ts.data61.csiro.au/
> projects/TS/echronos/
> >
>
> In particular we have some work in the pipeline that adds (ARM
> Cortex-M3/4) MPU support to eChronos (it’s currently in the process of
> being code-reviewed and will be released after that).
>
> Ihor.
>
>
>
> _______________________________________________
> Devel mailing list
> [email protected]
> https://sel4.systems/lists/listinfo/devel
>
>
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to