## Fair schedulers

March 8th, 2008 by HancockFrom time to time, I try to put report things in this blog. If someone (local) can tell me how to put tags in so stuff like ASCII “art” comes out nice, I’d be grateful. It is beyond me. “code” doesn’t work.

This lunchtime was in 2 bits. First Hank spoke, about what he called “functional operating systems”. He seemed to mean combinations of continuous stream processing functions involving fair stream schedulers.

What is a fair stream scheduler? A function

`m : Stream A -> Stream B -> Stream (A + B)`

whose value always contains infinitely many inL’s and infinitely many inR’s.

Hank claimed that any such function could be represented by a program of type:

`M = nu ((A->)* . (B ->)+. (A->))`

where `F*`

denotes the free monad over `F`

, and `F+ = F . F*`

.

He gave the constructors of (A->)* X the names Ret and Rd:

Ret : B -> (A->)* B

Rd : (A -> (A->)* B) -> (A ->)* B

The idea is as follows.

First, define

eat' : (A->)* (C) -> Str A -> ([A], C, Str A) eat' (Ret c) as = ([],as) eat' (Rd f) (a:as) = let (al,c,op) = eat (f a) in (a:al,c,op)

Now, let’s define

schd : M -> Str A -> Str B -> Str (A +B) schd m as bs = let t = elim m (al,f,as') = eat' t as : ([A], (B -> (B ->)* ((A ->) M)), Str A) t' = f (hd bs) (bl,g,bs') = eat' t' (tl bs) : ([B], (A ->) M, Str B) m' = g (hd as') in (map inL al) ++ [inR (hd bs)] ++ (map inR bl) ++ [inL (hd as)] ++ schd m' (tl as') bs'

In essence, m eats 0 or more A’s, then one or more B’s, then an A, then loops. As m reads things, we pass them through, appropriately

tagged to the output.

Hank asserted, in a voice of thunder, that the output of such a function contained infinitely many inR’s, and infinitely many inL’s; moreover that any such interleaving was the output of such function. He conjectured that

nu ((A->)* . (B ->)+. (A->))

= nu ((B->)* . (A ->)+. (B->))

and then began to talk rather obscurely about circuits

/| _________ |\\ / |---->| f |---->| \\ / | --------- | \\ +-> | _________ | m >-+ | \\ |---->| g |---->| / | | \\ | --------- | / | | \\|---->out in---->|/ | | V +<----------------------------------+

which "worked properly" for any choice of scheduler m, suggesting that at any rate he had made sense of the "for any", and that working

properly" might be, minimally, something like continuity (from in to out). He said this idea might help understanding delay-insensitive circuitry, or circuitry which is insensitive to buffering.

This all seemed to be in the context of the work Hank and Dirk and Neil had done some while ago in "stream eating". which represented continuous functions of type Str A -> Str B by nu ((A->)* (B \times)). There is a recent draft here.

March 8th, 2008 at 3:56 am

I’ve never been able to get the code tag to work. Try <pre>.

March 8th, 2008 at 2:40 pm

For the ascii art, use the html tags, or replace spaces with entities.

I’m afraid I don’t understand what a “free monad over smtg” is..

But isn’t faire scheduling a simple matter of fair threads (coopĂ©rative threading) with no path of execution containing an infinity of progression steps before a call to the scheduler? I’ll have to re-read your article when the indentation is better ^^

P!

March 8th, 2008 at 11:10 pm

Adrien: The free monad F* over a functor F can be defined by

`F* A = mu X. A + F X`

. And`mu`

here indicates the initial algebra of

`X |-> A + F X`

.When F is the functor

`X |-> B -> X`

, ie the readermonad,

`F* A`

is the type of wellfounded trees(no infinite paths from the root) branching over B, with leaves

labelled by elements of A. Such a tree can be interpreted as a

program that reads a finite sequence of B’s, then terminates, yielding

an A. The wellfoundedness is here crucial to enforce termination.

I’m sorry, it wasn’t well explained. Moreover I’m not at all sure I’m

on the right track. (FP lunch is a venue where one can be a bit

unbuttoned…). I should have mentioned: besides

merge : (Str A > Str (A + B)

one needs a function

split : Str (A + B) -> (Str A >

to be left inverse. But the type of split is wrong. Its domain is really the set of

streams that have infinitely many inL’s and inR’s. My suggestion is that the

definition of this concept involves a nested fixpoint

nu ((A ->)* . (B->)+ . (A->))

where nu means: final coalgebra. So, mu’s nested inside nu’s.

By the way, I’m pretty sure there is a paper of David Park’s from the 70′s which (in part) discusses precisely this concept.

April 1st, 2008 at 5:22 pm

I have been able to write in Haskell the bijection claimed:

nu ((A->)* . (B ->)+. (A->))

= nu ((B->)* . (A ->)+. (B->))

My question now is, how does this generalize to fair scheduling of more than 2 streams?