Fair schedulers

March 8th, 2008 by Hancock

From 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.

4 Responses to “Fair schedulers”

1. Jared Says:

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

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!

3. Hank Says:

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 reader
monad, 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.

4. Vicar Says:

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?