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
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:
10/07/2018 10:18 Gernot.Heiser(a)data61.csiro.au:
On 10 Jul 2018, at 18:06, piotr(a)skrzypek.eu wrote:
Thank you very much for quick reply.
I was curious specifically about seL4. eChronos, in my view is much
it doesn't have the concept of Capabilities or temporal partitioning. These
features make seL4 extremely attractive for safety critical applications.
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
Devel mailing list