Concerning Section 3.3.1: The phrase “the most significant bits of the capability address” is unclear. How many significant bits? Perhaps it is a constant number fixed upon building the kernel. The phrase “guarded page tables” does not appear elsewhere on the web site. Elsewhere this suggests the first guard value is found in the first table entry. This does not agree with your text unless the capability in the TCB is an ‘honorary table entry’. That page speaks of bits in the table entries whereas in the case of seL4 table entries are capabilities. I would not object to a guard which is a small integer in such a capability.
Googling we find that this paper, by Leidke defers to either “Address space sparsity and fine granularity” which seems not to be on line, or Page table structures for fine-grain virtual memory which is. This latter paper has the sentence “Therefore, each entry is augmented by a bit string g of variable length, which is referred to as a guard.”. Different mapping entries can have different guard lengths. If the guarded entry refers to another table the question is, “Which address bits index into the next table?”. This paper does not say when the address found in the entry is a page origin or a table of further entries. Following references to online papers does not answer this question.
Gerwin Klein responds to email with this rather clear explanation:
These papers speak of mapping table entries with guards. The original paper to which this page is a comment, speaks of the guard being a property of the CNode. I doubt that the implementation keeps the guard in the CNode. If different capabilities to the same CNode are supposed to hold the same guard value, how is this accomplished. From what I guess is the situation it would be better to fess up the the fact that the guard is in the cap and allow various guards to be different caps to the same CNode.
Other issues arise such as whether a CNode capability without write permission in the path to the slot nullifies a store into that slot. I presume that it does. The Keykos ‘sensory’ question arises.
Curiously this “guarded page table” pattern arises in Keykos in another context: memory addresses, where the Keykos kernel endeavors to offload details of how host hardware mapping tables from user code. We did not succeed in describing those lucidly either.