Terminology Map

Notions are described by Keykos terms.

key: capability.
node: CNode. They are both mutable arrays of caps. A node has 16 slots, a CNode has 2ⁿ where n is chosen at node creation time.
slot: slot. In common: A slot is a mutable place to hold a cap. Caps reside only in slots. Slots occur only in nodes/CNodes. All Keykos slots hold a key including number keys DK(n). seL4 slots may be empty where the Keykos slot would hold DK(0).
General Keys Node slot: CSpace root. That part of an obeyer (domain — thread) that holds the caps that user mode code can name in an invocation. It is just the 16 caps in Keykos but a tree’s worth in seL4 which the call the “capability space”.
domain: Thread or (TCB thread control block). They both obey user mode programs found in storage constructs of the respective systems. Those programs can access such memory and invoke and pass and receive caps in messages. The seL4 (IPC) Endpoint is without a direct Keykos counterpart but a domain can serve as such.
domain service key: TCB cap.
message: message. Part of an IPC mechanism. Both are transient meaning that they are not found in a system state. They are both composed of data and capabilities. They are both addressed by a key/cap.
Order: method. This is part of the data part of a message conventionally serving as a method identifier in OO speak.
data byte: badge. The same as the Keykos databyte.
sever: revoke. Keykos and seL4 literature use “revoke” differently. seL4 “revokes” by what would called “sever” in Keykos. Keykos boasts being able to indirect any sort of cap. I don’t known about seL4 yet. Keykos has not implemented sever completely yet.
…: endpoint. A mailbox thru which seL4 messages conceptually pass. Keykos rejected this idea because any use case we saw could be done with and extra domain, and the cases were rare. In seL4 a thread can take messages from different endpoints. I would like to see a use case for this.
Address space: Address space. I see no recursive concept for segments in seL4, at least that the kernel knows of.
Domain keeper slot: exception-handler endpoint. In Keykos one of the special slots of a domain which tells the kernel who to notify (what key to invoke) when the program gets in trouble. Analogous in seL4.

Keykos	seL4
Domain keeper slot	exception-handler endpoint
return key	reply capability
Number key or DK(0)	Invalid capability
Fork	seL4_Send
Return	seL4_NBSend
Call	seL4_Call
exit block	seL4_IPCBuffer
order	seL4_MessageInfo_t
Kernel Innards
backchain, allocation count	capability derivation tree

I have seen no analog to the recursive Keykos kernel segment function.
Keykos considered what seL4 calls an ‘endpoint’ but decided that in those use cases where an endpoint was better, an extra domain would serve nearly as well.
seL4 segregates capabilities from data, like Keykos.
‘reply’ capabilities are “use once” and vanish along with their copies upon invocation, as in Keykos.
Neither Keykos nor seL4 kernels buffer messages, (nor does the seL4 endpoint).
Modern CPUs hold operands in registers and use load and store operations to move data between memory and registers. Early CPUs often addressed operands in memory. seL4 tends to address cap operands in “memory”. Keykos imagines 16 cap registers into which to move operands before they are used. This might or might not be a tactical error.

Interdefinability

Domains vs. Threads & Endpoints

Keykos Function in seL4
- To get a domain:
  - Create a thread and a synchronous endpoint.
  - Endow the domain with the unique read cap to the endpoint.
  - The cap to the TCB is sort of the domain key.
  - The write cap to the endpoint is sort of the start key.
seL4 function in Keykos
- To get an asynchronous endpoint
  - Create a domain.
  - The domain requests of its creator a start key and the resulting return key becomes the read cap to the endpoint. When that return key is called the domain enters a co-routine with the consumer.
  - A start key to the domain serves as write key to endpoint.
- To get a thread
  - Create a domain
  - …

Comparing definition of memory

In Keykos we buy a node, format it as a segment node, request a segmode key from the node key, place that key in a place so as to define memory for some domain, and on demand the kernel builds memory maps to define the space.

In seL4 we choose some untyped memory and turn it into a a mapping table entry. We get back a capability to do things to that map.

Both seem sound to me. An interesting contrast.

Keykos has considerable kernel hair in mapping memory, but a simple C-list. seL4 has considerable kernel hair in their C-list, but a simple construction of virtual memory. An interesting contrast.

Keykos attempts to make kernel objects uniform across hardware architectures. Of course there are some differences in domains between architectures. seL4 exposes more of the memory map hardware than Keykos. There is an seL4 kernel object called the page table whereas Keykos has the segment node. Perhaps seL4 is closer to the hardware in this case. I do not object.

Keykos provides primitive intermediation for meters and segments. It arbitraily limits the depth of these seL4 has no such semi-recursive kernel services, but several schemes to ameliorate this.

Badged seL4 caps are derived from caps with zero badges.
Keykos start keys with Databytes are derived from domain service caps.
Not much difference.
Both seL4 and Keykos deliver functionality of hardware debugging facilities. Major IBM OSes omitted this.

To invoke

3 seL4 primitive sys calls are Send, Receive and Yield. 3 primitive Keykos sys calls are Call, Return and Fork. In seL4 the pair Send-Receive (which they call Call) produce the effect of Keykos Call including the ‘reply cap’. the reply cap goes to a special slot in the recipient but there is free flow between that slot and others. Bare seL7 Send is like Keykos Fork. seL4 Yield is just giving up the remaining of a time slot. I don’t know why we did not need this in Keykos. Perhaps less exposure to polling strategies.