The kernel · L2 and L4

Channels

Tasks talk only through channels. A channel carries an exact number of messages, or, a stream, as many as its sender sends before closing it, each of an exact size, through a ring of slots in kernel memory. Who may send and receive, and how often, is fixed before the system is built, and sysp checks every task keeps to it.

Copied, never shared

Sender's bufferin its own heap; it keeps it after sending
send
copies →
The channel's ringslots in the kernel's mail buffer; no task can reach it
recv
copies →
Receiver's bufferin its own heap

A message is copied twice: into the kernel on send, out of it on recv. No task ever holds a pointer into another task's memory, so a task's memory really is its own. The cost is two copies of small messages, which sysk accepts.

Try a channel

Pick one of the pipeline system's channels (tests/pipeline/system.sysk, where every channel carries an exact count). Each sender holds a Tx handle with its share of the messages; the receiver holds the Rx. Send and receive, and watch the ring. The buttons follow the same rules sysp enforces: a handle with nothing left cannot send, and a handle can be closed only when it has nothing left.

The ring

Every channel's ring sits in one kernel buffer, mail, at an offset the manifest decides; the table below is the default system's. A ring of depth d for messages of n bytes is d · n bytes. The kernel keeps, per channel, where the next message is written (wr), where the next is read (rd), and how many wait (queued). After a copy, a position moves on by n, or back to 0 if another message would not fit before the end: (if (> (+ (+ w n) n) r) 0 (+ w n)). The kernel invariant says every position leaves room for a message and queued is between 0 and the depth, so every copy is proven to stay in its ring.

ChannelMessagesBytes eachDepthRingIn mail atSendersReceiver

While the system runs, a task holding a Sys can read each channel as a file, /chan/NAME: its size and depth, how many messages wait, whether it has ended, and who sends and receives (sysk 028; Files). In the shell: cat /sys/chan/screen.

The protocol is the contract

A handle is a resource struct: the channel, the messages left, the bytes per message, and whether the channel is a stream (below); a receiving end also records whether it has received a stream's end. send requires an exact channel (tx-exact), (> (. out left) 0) and a message of exactly (. out bytes), and ensures the handle is one message further on. close-tx, a kernel call taking the kernel, requires (tx-done out): no messages left. A task states its side of the protocol in its precondition, and the manifest's numbers must match it. Here is the producer:

So each of these is a compile error, not a run-time surprise: sending once too often, sending the wrong size, sending with a receive handle, closing before the conversation is over, forgetting to close, copying a handle, or a manifest whose counts or sizes disagree with the tasks.

Sending and waiting are one step. send checks for a free slot and copies into it inside one atomic block. If the ring is full it calls wait from inside the block, which lets every other task run once, and checks again when it comes back, so no other task can take the slot in between. recv does the same for an empty ring.

Several senders, one receiver

In the pipeline system, the log channel has five senders and one receiver, the UART printer. Each sender's handle carries its share, written in the manifest as (tx log 3); the shares add up to the channel's count. Nothing in the kernel had to change for this: the ring and the counts already worked. The printer does not know the order lines arrive in and does not need to: it loops (while (> (rx-remaining in) 0) …) until its handle is spent. In the default system the shell receives the output of each job the same way: a stream whose senders are the job's programs (The shell).

A job's channels (sysk 017) are channels of the pool, with fixed sizes and depths. Before a job starts, every pool channel is made empty and open again, which keeps each ring in order; who holds which end, and how many messages each carries, come from the job and its programs' contracts (Jobs).

Two pool channels can be a service (sysk 031): (service files (bytes 576)) makes the streams files-ask and files-reply, and the task that (serves files) holds their other ends, a Service, for the life of the system. Starting a job marks the service fresh when the job binds its ask channel; the server's alt sees that as ready, service-open takes the job's requests, service-reply the stream for its replies, and service-close ends that stream once the job's requests have ended. The kernel keeps only which state the service is in, idle, asked or lent, and the contracts carry why a job's channels are never emptied under an open lease: a client finishes only once it has received the replies' end (Files for jobs).

Streams: conversations of unknown length

A channel declared without a message count, (keys (bytes 1) (depth 16)), is a stream (sysk 015): its one sender sends any number of messages with send-more and then closes it; close-tx marks the channel ended. Its receiver calls recv-more, which gives the next message (true) or, once the channel has ended and every message has been received, the end (false), recorded in the handle. The end comes after every queued message and stays. rx-ended, in the library, says whether that end has been received, so a loop can run until it has; alt counts an ended stream as ready, so a task waiting on several sources sees the end like a message. The rule against closing early is one rule for both protocols: close-rx requires (rx-done in), which means no messages left on an exact channel and the end received on a stream. Which protocol a handle has is fixed by the wiring that mints it, from the manifest, and a task states it in its precondition: (tx-left out 3) says exact, (tx-stream out) and (rx-open in) say stream.