Nottingham FP Lab Blog

A Toy Kernel

by Hancock on November 3, 2006.
Tagged as: Lunches.

Motivation:

The toy kernels people are looking at are ugly, random piles of conventional operating system features.
This makes them mathematically intractable; but we need good, clean theories to guide system programming.

Here is, in an approximate form the simplest toy kernel that I know works (because I actually implemented something like it for a database machine, and because something else like it has been very successful in factory automation, ATMs, etc). It has a core of just 3 kernel calls (and one other that I suspect might be required), plus two primitives that dynamically introduce and cull concurrency (that I suspect are not always necessary).

At the moment I am just staring at the primitives. They are *synchrous*, implying that message passing requires no intermediate buffers; however unlike Occam, CSP etc there is an asymmetry in the two parties to a message transfer: one is a server (which takes control), and one is a client (which waits for control to be returned).

Types:
Sid — set of server/thread identifiers
Cid — set of command/request identifiers
Msg — set of communicable values

Abbreviation:
X+ = X + 1 — “Maybe”, used for alerts.

Kernel Interface:
command : Sid Msg -> IO(Sid Msg)+ –
get : IO (Cid Msg)+ — alertable: server waits for a client (or wakeup)
respond : Cid Msg -> IO 1 — commit: server discharges client’s call
forward : Sid Cid Msg -> IO 1 — pass on client to another server

alert : Sid -> IO 1 — ensure that Sid wakes up sometime soon.

split : IO(2 Sid)+ — fork, exchanging identifiers and which is which
die : IO 0

Remark:
Cid could be taken to be Sid. But conceivably, command identifiers could be universally unique.

I ignore error cases, such as sending to a non-existent server.

Semantics:
we represent the state of a system by a multiset of threads, which can be in various states:

Eligible to run
Awaiting response from t : Tid
Awaiting request (from anyone)

Each thread has a tid. There is an infinite supply of unused Tids. The tid is really an identifier for a message stream, in which requests from different threads are interleaved.

For each thread t, let WResp(t) be the set of threads awaiting response from t : Tid. This defines the graph of a relation between threads.

The semantics of the primitives is given by saying what effect each primitive has on the state of the system. Some points which may not be obvious:

A server may respond to a request only if the request is waiting for a response from it. (And not from some other server.)
Instead of responding to a request, a server may forward it (rewriting the message) to another server; as if the server had responded and the client had immediately sent the new request to the new server. This transfers the responsibility for responding to the new server.
A thread that sends to a itself deadlocks. Deadlocks can be more circuitous. Deadlocked threads can be garbage collected.

The run-time system picks a thread that is eligible to run, and evaluates it till its WHNF is one of the primitives in the kernel interface; then performs the required action, and updates the state of the thread. (The state of a thread has type IO 0.)
The system terminates when no thread is eligible to run.

Vague observations, remarks:

There are two blocking primitives. (Actually, perhaps Split should be considered blocking. )
We are quite interested in those threads which eventually perform a communication. Otherwise, the thread might as well not exist. (A thread can be killed by removing its capacity to communicate.)

As subsets, we are interested in some of or more than:

* those processes that eventually block in Get (idle servers)
* those processes that make a finite sequence of requests, and ultimately die.
* and various other “eventuality” and “perpetuality” properties.

* One would like to understand the interplay between folds and unfolds in the implementation of a toy system.

* It may be that one can enhance the expressiveness of the type system (making distinctions of interest for building concurrent systems) by introducing
IO* A — the free monad over an IO interface functor
IO% A — the analogous greatest fixed point
nu(IO) = IO% 0

and some such stuff.

Conjecture:

There is, in some precise mathematical sense, an equivalence between the notion of a server thread, and a queue of client threads waiting to be consumed by the server.