The title of the first chapter, “Kernel Services and Objects”, illuminates an important difference in describing and reasoning about these systems, but not, I think, a difference in the systems. Of necessity some objects are implemented in the kernel, or at least I can imagine no other way. In some sense every invocation by user mode code to something outside its own address space is a system call. In an equally profound sense each such invocation is the invocation of some object, necessarily via the kernel. These senses are incompatible even when the real underlying mechanism is the same. It will confound some that the correctness of some user mode programs does not depend on whether some particular invocation point is to a kernel object, or to a user mode object.
Each of these two styles has its own advantages in reasoning.
Section 1 notes three things ‘proven’ about seL4 kernel:
See this regarding the ‘take-grant’ model.
In section 2.2 I see the phrase “which consists of a send followed by a Receive from the same object” which confuses me. I think they are explaining that their Call can be defined in terms of the more primitive Send and Receive. If the call is to an endpoint then I would hope that that endpoint is not ‘busy’ while the recipient is working on a reply. One attraction to the endpoint design is several readers of one endpoint to provide concurrent servers of the same service. The detailed description of seL4_Call() below seems to contradict the introduction.
The seL4_Call system call is almost exactly like the Keykos call operation, including generation and destruction of a reply cap, or return key. The seL4 reply cap goes to a special slot in their TCB but can be moved to and from that slot and thus reply caps can get scattered around. Like Keykos they all disappear when one of them is used.
Section 2.4 introduces Untyped Memory and caps thereto. Such a cap does not allow direct reading or writing of such memory. I am confused by “frame objects”.
Section 2.4.1 on reusing memory is analogous to the Keykos mechanisms. Raw Keykos space was in the form of range keys to disk which held “home positions” of objects, whether or not they were ever swapped out. Raw seL4 space is Untyped memory. Pages and nodes Keykos disk space are firmly segregated at disk format time.
I think there is a terminology conflict here. In Keykos we say that two slots in the same or different nodes may hold the same capability (key) and thus that there is just one key. I think that in seL4 they count the occurrences and would count two caps in the same situation. With this interpretation their “capability derivation tree” is almost exactly like the Keykos backchain.
Bt calling seL4_CNode_Revoke() seL4 nullifies all caps to the CNode with no effect on its content. We should add that to Keykos. Selective revocation of a particular cap is more expensive, more general and requires foresight. I have not previously realized that revocation had these two meanings. Keykos has a limited form of seL4 revoke which we call “sever”. We could and should extend our sever.
Section 3. Several places refer to minting new capabilities as if this were a separate kernel action. In Keykos you called the object and asked for a weaker capability—no general kernel function.
“This mechanism can be used by servers to restore sole authority to an object they have made available to clients, ...”
We were on the verge of adding this useful feature for about a year, but did not get around to it.
Section 3.1.1: seL4 caps are 16 bytes—same as in-core Keykos keys.
Section 3.1.2:
It seems to be a mistake to let the holder of a cap mint a new cap like the old with a new badge of holder’s choosing.
But what 3.1.2 seems to grant is denied by 4.2.1!
A seL4 call deposits a reply cap in the TCB of the recipient.
There is an op to move that out of there: seL4_CNode_SaveCaller.
Is there an op to move it back?
What is an “outstanding send”?
------
I am skipping ahead.
I suspect that there is a problem with ordering of information.
Sec 3.1.4: Small Quibble: Recent Keykos talk is careful to delegate the meaning of rights bits to the code that defines the behavior of the object designated by the cap. The few times the kernel examines the databyte is for caps to kernel objects. See this.
Sec 3.2: “If, however, it was the last typed capability to an object, this object will now be destroyed by the kernel, cleaning up all remaining in-kernel references and preparing the memory for re-use.” Garbage collection, of sorts. The footnote requires close study.
Keykos has a few arbitrary limits on levels of derivation (Meters and memory keys). seL4 limits some similar derivations perhaps to solve the same problem. I somewhat prefer the Keykos solution.
At this point in my reading I fear that is impossible to add paging to seL4. It seems that once references to a new object have been distributed then it cannot survive reallocation of its underlying RAM.
The end of this section describes some sort of synergy.
In Section 3:
If you map the Keykos space bank onto the seL4 Untyped_Memory then there arises the issue of overallocation. A bank has a limit and if I make two sub banks each with a limit then the limits of the subbanks may sum to more than the limits on the original bank. This is a useful pattern which I think Untyped_Memory lacks. Also I think that the Untyped_Memory is the unit of real space reuse. This requires a great deal of preplanning in the form of estimating size.
Section 3.3: See Describing Guarded Addressing
Sec 4.2.2: “A received capability has the same rights as the original, except if the receiving endpoint capability lacks the Write right. In this case, the rights on the sent capability are diminished, by stripping the Write right from the received copy of the capability.”
This sounds like the Keykos kernel’s sensory stuff:
“A received capability has the same rights as the original, except if the receiving endpoint capability lacks the Write right. In this case, the rights on the sent capability
are diminished, by stripping the Write right from the received copy of the capability.”
“If the n-th capability in the message refers to the endpoint through which the message is sent, the capability is unwrapped: its badge is placed into the n-th position of the receiver’s badges array, and the kernel sets the n-th bit (counting from the least significant) in the capsUnwrapped field of the message tag. The capability itself is not transferred, so the receive slot may be used for another capability.”
This sounds like a synergy mechanism.
It might even be an efficient one!
Sec. 6.3: The “domains” of seL4 sound like a primitive tool for the management of covert channels. Keykos designed but did not implement any such tools.
Sec. 7: Both Keykos and seL4 emphasize parallels between data and caps.
I think I need a list of seL4 kernel invariants to understand their text.
Perhaps I should write one for Keykos.
I think that by “frame” they mean what we mean by “page”.
“Before a 4 KiB frame can be mapped, a page table covering the range that the frame will be mapped into must have been mapped, otherwise seL4 will return an error.”
By analogy in Keykos you merely put a page key in a node slot, in a node that will be used to define a segment.
What system call responds with an error in seL4?
Sec 7.2: The system call seL4 ARM PageTable Map:
I am surprised that they view this as an invocation of the page table, since it is the page directory which is modified.
That seems anomalous.
The same anomaly pertains to putting a page in the page table.
I presume there are caps to pages.
Sec 9.1: The table 9.1 is a very useful tool in testing your understanding of the kernel.