On 31.08.2015, at 18:55, Raymond Jennings 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.