Re: [seL4] mpu vs mmu

21 Aug 2017


      Thanks for the information.  Looking at eChronos now.
...
---------- Forwarded message ----------
From: 
To: 
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, Gernot.Heiser@data61.csiro.au wrote:
On 21 Aug 2017, at 03:00, Thomas Dundon  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
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel