> 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
