Archive for November, 2006

Asking for stream processors

Tuesday, November 28th, 2006 by Wouter

Thorsten started by talking about Ask: a total fragment of Haskell. Key features include:

  • Ask distinguishes between data and codata.
  • Ask incorporates some kind of first-order predicate logic.
  • Ask has both quotient types and subtypes

Thorsten would like to use Ask as a pedagogical tool. You can reason about Ask programs very nicely. For example, you could use Ask to construct a pure model of I/O fuctions.

Conor would like to use Ask to justify what is happening in Haskell’s type system and introduce something a bit like dependent types. Conor speculated how one could allow constructor patterns to appear freely within types. Having a total fragment of your language is very important here – otherwise you lose all hope of having a somewhat sane type system. I’m paraphrasing a lively discussion, so forgive me if I got something wrong.

Afterwards, I talked a bit about arrows and stream processors. Thorsten and I claim that John Hughes’s example of stream processors as arrows are not really arrows. There are two alternative definitions of composition, both which fail to satisfy all the arrow laws. The definition of first and the laws that it must satisfy is where most of the problems are. On the other hand, the stream processors do carry a coproduct structure. We speculated how we could then generalize the definition of arrow to allow other monoidal structures.

A Toy Kernel

Friday, November 3rd, 2006 by Hancock

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.