Reply To: Memory Allocation

Turf change is opaque to the running code and may vary in implementation. It occurs only during Portal transit during call or return hardware operations.

In a typical form, permissions are represented in three ways: the set of Well Known Regions, the Permission Lookaside Buffer, and a table in memory. The WKRs are reloaded during Portal transit; the PLB is scrubbed by transit; and each turf has its own table whose base is in a dedicated hardware register. A check is made to a particular WKR based on the kind of reference, then to the PLB, then to the table. Implementations may vary in such things as to whether the PLB is single-level or multi, and whether table search is hardware or software varies.

Mill does not have the SeL4 problem of needing to know permissions at thread creation. Because we use a grant model rather than a capability model, you can create a turf with no permissions at all and then add permissions dynamically later by subsequent grants of permission.