On 31.08.2015, at 18:55, Raymond Jennings
<shentino(a)gmail.com> wrote:
I noticed that unlike mach, L4 does not directly manage virtual memory, but instead farms
out address space, page directory, and page table capabilities to userspace and lets
userspace decide what pages to map and where.
You’re right, but note that there’s a careful distinction here: seL4 does manage *access*
to virtual memory, but it avoids imposing a management *policy* on user-level. That’s a
key part of how seL4 works.
Does this imply that virtual memory abstraction is
userspace responsibility?
That is correct.
The idea is that it is impossible to predict what the correct management policy is at
kernel level and that it is not necessary to do so. User-level can implement whatever
policy is required efficiently, usually in a library layer, so you don’t have to deal with
it directly as an application programmer.
This way it is possible for example to have a number of extremely simple, static VM
mappings for small components that you’d like to do formal verification on and at the same
time have a fully dynamic virtual machine monitor running next to these without
compromising on security or verification feasibility.
Cheers,
Gerwin
________________________________
The information in this e-mail may be confidential and subject to legal professional
privilege and/or copyright. National ICT Australia Limited accepts no liability for any
damage caused by this email or its attachments.