Dear Anna, Thank you very much for quick reply. I was curious specifically about seL4. eChronos, in my view is much different - it doesn't have the concept of Capabilities or temporal partitioning. These 2 features make seL4 extremely attractive for safety critical applications. This is why I was interested if Cortex-R was in the roadmap. Anyway, you message does answer my question, thank you! Piotr

10/07/2018 03:21 Anna.Lyons@data61.csiro.au:

Hi Piotr,

For platforms without MMUs, take a look at eChronos[1], which is a small RTOS that does support MPUs. seL4 only targest systems with MMUs.

Thanks Anna.

[1] https://ts.data61.csiro.au/projects/TS/echronos/ ________________________________________ From: Devel on behalf of piotr@skrzypek.eu Sent: Monday, 9 July 2018 5:17 PM To: devel@sel4.systems Subject: [seL4] Future plans w.r.t. Cortex-R

Dear seL4 Maintainers,

Could you please share what are your future support plans w.r.t. ARM Cortex-R family - the 'reliable' and 'real-time' side of ARM portfolio?

Cortex-R implementations include interesting safety features i.a. lockstep processing. It feels like a good match for seL4 safety-oriented philosophy. However, Cortex-R processors have MPU instead of MMU, which seems to be ruling them out for now. Are there any plans to have an seL4 'MPU' branch in order to support these kind of processors?

Thank you in advance, Piotr Skrzypek

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Dear Gernot, I agree that for a long time the MPU-based microcontrollers were rather small, perhaps with only few hundreds kB of flash and internal SRAM. Indeed, for this kind of system, virtualization of guest operating systems makes little sense. But this is not the case anymore. Looking at the specifications for ARM Cortex-R52 - it is as powerful as Cortex-A series, includes hardware virtualization support, but is inherently based on MPU (to avoid time nondeterminism of TLB miss). For this target, building a temporal and memory - partitioned applications does make a lot of sense. The MPU of Cortex-R52 is pretty fine grained too - the region can be defined with the resolution of 64 bytes. Nevertheless, of course there is no (virtual) address translation and the number of regions is limited and not automatically reloaded from main memory (I am not sure if that immediately rules out the caps approach). I believe, however, that ARM will continue this path and the future Cortex-R releases will still be based on MPU. Cortex-R also seems to be the preferred target for the safety critical industry. E.g. the new ARM based radiation-hardened processor for space is based on Cortex R52: (http://dahlia-h2020.eu/). Kind regards, Piotr

10/07/2018 10:18 Gernot.Heiser@data61.csiro.au:

On 10 Jul 2018, at 18:06, piotr@skrzypek.eu wrote:

...

Dear Anna,

Thank you very much for quick reply.

I was curious specifically about seL4. eChronos, in my view is much different - it doesn't have the concept of Capabilities or temporal partitioning. These 2 features make seL4 extremely attractive for safety critical applications. This is why I was interested if Cortex-R was in the roadmap.

As Anna said, seL4 targets systems with a full MMU, and trying to bend it to fit an MPU wouldn’t make sense. The advantage of caps is that they give you fine-grained access control. But without a full MMU, you don’t get fine-grained protection from the hardware, the model doesn’t make sense there.

Similarly, the temporal isolation model only makes sense if you have relatively complex systems comprised of components with different levels of trustworthiness. An MPU-based microcontroller is just not the right platform for such a system (which almost inevitably uses virtualisation for supporting legacy components).

Gernot _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel