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