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:
The number of most significant bits that are stripped from the address is specified in the capability to the CNode that you are resolving to.
That is, if you are in the middle of the resolving process somewhere, and there is a CNode cap that points to a CNode of size n, the cap itself will have a field “guard-size”.
The address is shifted left by that amount, and the next n bits are used to resolve inside this CNode.
The process then either terminates (e.g. all address bits are used), or continues if at that slot there is another CNode cap pointing to the next CNode.
I take it that the slot designation is a bit string with a length.
There are several ways to represent such; I suggest two here.
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.
Sec 3.3.1: “It then compares that CNode’s guard value against the most significant bits of the capability address.”
I think this is poorly worded.
I speculate that it should say:
The guard from the examined capability is k bits long for some integer k.
(The capability encodes k.)
If the high k bits of the capability address do not match the bits of the guard then the lookup fails.
Note that the capability address supplied by the user mode program itself has a length for the lookup procedure speaks of “remaining bits” therein.
“there are remaining bits (following the radix bits)
in the capability address”.
This may be the place to define ”depth” used sometimes to qualify “capability addresses”.
Ahh: Section 3.3.2 defines the phrase “depth limit”.