On 21 Aug 2017, at 03:00, Thomas Dundon 
<[email protected]<mailto:[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/

Gernot
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to