The continuation receives both the computed value and the current computer memory. Therefore return invokes it with unchanged computer memory, while sequencing installs a continuation that passes the produced value and updated computer memory to the next computation:
result :: a -> M a
result x k s = k x s
bind :: M a -> (a -> M b) -> M b
bind p f k s = p (\x s' -> f x k s') sFor left identity, expand the two definitions:For right identity,For associativity, both groupings reduce to the same expression:By function extensionality, these establish all three monad laws:
Apply the memory interface before invoking the supplied continuation:
get :: Location -> M Value
get a k s = k (contents s a) s
put :: Location -> Value -> M ()
put a v k s = k () (update s a v)
new :: M Location
new k s = let (a,s') = fresh s in k a s'A read preserves computer memory; a write changes it but returns the unit type value; an allocation uses the updated computer memory returned by
fresh. The continuation always receives the latest computer memory:Capturing a continuation retains the destination, while the computer memory is supplied when that destination is eventually invoked. The required Haskell definitions are:
callcc :: (Cont a -> M a) -> M a
callcc f k s = f k k s
withc :: Cont a -> M a -> M a
withc saved p _current s = p saved s
callccPrim :: [Value] -> M Value
callccPrim [Function f] =
callcc (\k -> f [Continuation k])
withcPrim :: [Value] -> M Value
withcPrim [Continuation k,v] = withc k (result v)In
callcc, the handler f k initially runs with the same current continuation k. If it returns normally, its result goes there. If it invokes withc with a saved continuation, the current destination is discarded. In particular,The primitive interface receives values, because the surrounding call-by-value interpreter has already evaluated its arguments. Thus the expression supplied as the second argument of withc is evaluated once, before withcPrim transfers its value. Wrapping that value with result implements precisely the remaining transfer; the primitive must not try to evaluate it a second time. Neither operation restores a saved snapshot of computer memory.Keep a FIFO queue of runnable continuations in shared computer memory. Removing a continuation from its head transfers control with
nil; suspending a runnable computation appends its continuation at the rear. A single scheduler group also needs a terminal continuation so that finishing the last computation cannot return through an obsolete invocation of fork.The following is
FunMem, including the shared initialization and helper definitions. run(main) starts a scheduler group; nested fork calls use that same group.val ready = new(); ready := nil;
val stop = new();
rec append(xs,ys) =
if xs = nil then ys else head(xs) : append(tail(xs),ys);
val enqueue(k) =
ready := append(!ready,k:nil); nil;
val dispatch() =
if !ready = nil then withc(!stop,nil)
else let val k = head(!ready) in
ready := tail(!ready); withc(k,nil);
val run(main) =
callcc(lambda (done)
stop := done; ready := nil;
main(); dispatch());
val fork(f) =
callcc(lambda (parent)
enqueue(parent); f(); dispatch());
val yield() =
callcc(lambda (current)
enqueue(current); dispatch())At
fork, the parent is queued before f() starts. The child runs immediately. Its ordinary return value is ignored by sequencing into dispatch(). At yield, the current computation joins the rear, then the oldest runnable computation is removed from the front. If there was no other runnable computation, these operations select the just-captured continuation, so the caller resumes immediately with nil.The invariant is that each suspended runnable computation has exactly one entry in
ready, ordered by the time it most recently became suspended and runnable. A running computation is absent from that FIFO queue. Neither appending nor removing an entry suspends, so these operations are indivisible relative to this cooperative multitasking scheduler. Completing a child removes the child from consideration permanently; it is never enqueued by its completion wrapper.For the paper's example, call the initial computation and the forked computation . The FIFO queue and writes evolve as follows:
Thus the observable list, read after the scheduler group finishes, isThe scheduler exit is used only when no runnable continuations remain. A main computation can place its desired final observable value in shared computer memory and read it after
run returns. This wrapper also permits already-forked computations to finish if the initial computation finishes before them. Each run creates one active scheduler group; calls of run are not nested.Represent a binary semaphore by a two-element list containing the addresses of its busy flag and its waiting FIFO queue. A blocked continuation belongs to the waiting FIFO queue, not the scheduler's runnable FIFO queue. These definitions extend the
FunMem scheduler from the preceding part:val semaphore() =
let val busy = new() in
let val waiting = new() in
busy := false; waiting := nil; busy : waiting : nil;
val acquire(s) =
let val busy = head(s) in
let val waiting = head(tail(s)) in
if !busy then
callcc(lambda (blocked)
waiting := append(!waiting,blocked:nil); dispatch())
else (busy := true; nil);
val release(s) =
let val busy = head(s) in
let val waiting = head(tail(s)) in
if !waiting = nil then (busy := false; nil)
else let val next = head(!waiting) in
waiting := tail(!waiting); enqueue(next); nilA newly created semaphore is free. Acquiring it while free marks it busy and immediately returns
nil. Acquiring it while busy captures the remainder of the caller, appends that continuation to the waiting FIFO queue, and dispatches a runnable computation. No runnable copy of the blocked caller is retained.When a waiting caller exists,
release keeps the busy flag true: the released permit is reserved for that caller. It removes exactly one waiting continuation and appends it to the scheduler's runnable FIFO queue. It does not invoke dispatch, so the releasing computation keeps running. A newcomer cannot steal the reserved permit during the interval before the released caller resumes. That caller's captured continuation resumes after acquire with nil, already possessing the permit.These are FIFO semaphores; the question only requires selecting one waiter, so choosing the oldest is a valid stronger discipline. The updates contain no suspension except at the explicit blocking point, making them atomic relative to this cooperative multitasking scheduler. As allowed in the paper, invalid releases and executions in which every remaining computation is blocked need no error handling; the latter are deadlocks, not a way to make progress. Articles by others on the same topic
There are currently no matching articles.