The original design of the kernel was that whatever user-level service established the mappings (e.g. the root task) could provide the translation info to whomever needs it. Depending on the design of the system built on seL4, it could be as simple as base limit info in the case of static systems, in an ideal case. A mapping table in the case of fragmented allocation.

 

Obtaining the mapping info via system calls has the disadvantage of kernel entry and exit (overhead), though you could populate a mapping table with each call.

 

Also note that system calls are not necessarily accurate either in the case of dynamic systems, unless the mappee has some kind of contract with the mapper to not change the mapping, e.g. a pinning API or similar. If you have a pinning API, you can get the current translation info with the pin RPC.

 

The current frame translate method was a originally a work around an immature user-level that has made it “out in the wild”, so to speak.

 

We have not thought hard about security implications of translate on a page directory, as AFAIK, we had no motivation for an additional translate on top of an existing translate, on top of what could be done at user-level with some book keeping (and complexity).

 

-          Kevin