---------- Forwarded message ----------
From: <Ihor.Kuz@data61.csiro.au>
To: <devel@sel4.systems>
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 <dundon.thomas@gmail.com> 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