cml

Concurrent ML (Reppy), on std.domain: threads that meet at channels, and events, their synchronous operations, composed before one of them is committed. An event is a computation run up to its commit point: a send waits for its receiver and a recv for its sender, each a base event; choose runs each of several branches up to its first base event and commits one of them, what follows that base event the wrap, the others abandoned — told so where they asked, by withNack. The threads run on as many domains as the machine has cores. Import it by a name, import cml as CML.

Caution

Unstable: concurrency in heff is not settled. What this module offers may change, or go, in any release.

import cml as CML
import co
import std.domain as Domain

-- | what comes on `a`, one more, sent on `b`, for ever
ponger : {e w : HFunctor}
       -> {{cm : CML.cml w <: e}}
       -> CML.Chan w Int
       -> CML.Chan w Int
       -> Co e Unit
ponger a b = do
  x <- CML.recv a
  CML.send b (x + 1)
  ponger a b

-- | main and one thread: 0 sent there, and 1 back
pinged : {e w : HFunctor} -> {{cm : CML.cml w <: e}} -> Co e Int
pinged = do
  a <- CML.newChan
  b <- CML.newChan
  CML.spawn (ponger a b)
  CML.send a 0
  CML.recv b

-- | `Just 1`, the threads on domains
pingedHere : {w : HFunctor}
           -> {{dm : Domain.domain <: w}}
           -> Co w (Maybe Int)
pingedHere = do
  with _ := CML.threads do
    pinged

Operation	What it does
spawn c	c, of the scheduler’s world cml w <+> Custodian.custodian <+> w, is a thread of its own, its withs giving to the custodian this one’s give to here; this one goes on
yield	the next thread’s turn; this one’s again after those ready
newChan	a channel, of what its type says
send ch x	x on ch, once a thread takes it: waits for the receiver; a base event
recv ch	what a thread sends on ch, once one does: waits for the sender; a base event
newIVar	an ivar, holding nothing yet
putIVar iv x	iv holds x now, its readers given it; once, a second put abandons; never waits
readIVar iv	what iv holds, waiting until it does; a base event
never	a base event never ready
choose cs	one of the branches: each run to its first base event, one of those committed, at random where several can be
withNack f	f nack, the nack nack ready once a choose is left without this branch
awaitNack nack	once nack is ready, its choose left without its branch; a base event
scheduled c	c and its threads run, on domains, in the scheduler’s world w, which need name no custodian: Just main’s answer, or Nothing where every thread waits; failing as the first thread that failed
scheduledWithReactor c	the same, a thread’s operation of the world that would wait pending in its domain’s reactor, the others going on
with _ := threads do ss	scheduled’s, ss main, a with: the block’s world with cml and a custodian, the with done once its threads are
with _ := threadsWithReactor do ss	scheduledWithReactor’s, as a with

An event is a computation, and its base events are operations: a send, a recv, an ivar’s read, a nack’s await, never. Run alone, an event is its first base event, committed once it can be, the thread waiting until then, and what follows. In a choose, each branch is run, in order and on this thread, up to its first base event — what comes before it is done as it comes, a guard’s work: a channel made, a request sent, a thread spawned — and that base event is the branch’s commit point; a branch that ends before one is ready at once, its value what it ends with, and a choose in a branch is that branch’s base events, so a protocol of several messages is one event, put in a choose with others and committed at once, which is what Go’s select cannot do. Where one of the base events can be committed now — a sender waiting at the channel of a recv, a receiver at the channel of a send, an ivar written, a branch ended — it is, one of them drawn at random where several can (as Reppy’s CML and Racket’s sync choose: no branch has priority over another); else the thread waits at every one of them, and goes on when another thread’s base event meets one. The branch committed goes on from its base event: what follows it is the wrap, as effectful as any statements. The others are abandoned at their commit points, and each withNack met on the way to one of them, not on the way to the one committed, has its nack ready: the branches not chosen told so. Under scheduledWithReactor, an operation of the world is a base event too, where it would wait: a socket read, a request, a sleep, pending in the reactor of the domain that started it; in a choose, committed once it is done, where no other base event was first, and else let go of, undone — so a branch of Time.sleep d is a time limit. However a choose is left, the branches not taken are told: a thread whose guard work in a choose fails, after a withNack there, has each nack made so far ready before it fails, and is counted no more; and a thread the run drops before it goes on from a choose — waiting there, or met and not yet run again, where main is done or every thread waits — has its offer withdrawn and every nack of that choose ready, once the domains have stopped, none failed. No thread of the run takes a turn after that, so such a nack readies none of them: it is for those reading it from elsewhere, a run of the scheduler inside one of the threads, or one after it. A choose run alone, in a computation an operation of w holds (below), tells no nack.

The threads are the scheduler’s, a handler in the language, and the domains are their workers: a thread is a resumption, run by a worker from where it stopped to where it next ends, gives up its turn (yield), or waits at a base event. A thread readied by one a worker runs — spawned, or met by its base event — is kept in that worker’s slot, the next it runs, where the slot is empty, and no domain is woken for it: a thread that hands a value on and then waits hands its domain on to the one it readied, no domain waking and no mutex taken. The others ready are in one queue under a mutex, which a worker takes from when its slot is empty, waiting on a condition while the queue is empty too; a domain waiting there is woken for each put in, where one waits. A worker that has run 64 (batchLimit) from its slot in a row puts the next behind those in the queue, where any are, so that they are not passed over; one with nothing to do takes a thread from another’s slot before it waits; and a thread’s slot is emptied into the queue before an operation of the world’s, which may hold its domain a while. yield puts the thread behind those ready, in its slot only where none is. The worker counts a thread’s steps, each operation of it the worker handles, as an engine of Chez Scheme’s counts its fuel: a thread that has gone on for 256 (fuelPerRun) since the worker took it, without stopping, is put behind those ready as at a yield where another is ready — in the slot or the queue — and the worker takes the next, its slot’s first, so that no thread is passed over for one that goes on, and none needs a timer; where none is ready, it goes on, its fuel full again, and a thread alone pays the count only. A thread that waits leaves an offer at each of its base events’ channels and ivars: one cell (Domain.Atomic) for all of them, claimed once, by Domain.cas, by whichever other thread’s base event meets one of them first, which readies the waiting thread with what came; so a waiting thread occupies no worker, and a choose commits one base event at most. What a readied thread does next is left to the worker that takes it (its turn is a function of that worker, its continuation unapplied until then): the one readying it applies nothing of another thread’s, and holds no mutex while a thread computes. Committing, a thread holds the mutexes of its channels and ivars, each once, in the order of their numbers, from looking for a partner until its offers are left, so that no thread misses a partner leaving its offer meanwhile, and none waits for another round a cycle; with them held it first asks of each base event whether it can be committed, claiming nothing, then draws one of those that can and claims its partner — where the partner’s offer was claimed meanwhile, through another channel, that one is dropped and another drawn. The offers waiting at a channel are a deque (one step to put at the back, however many wait); the partner is drawn from among the first few unclaimed at its front (window, 4), the others put back before the rest in their order, so that the choice among several waiting is not first come first served, yet every waiter reaches the front and is met (offers found claimed are dropped as they are met). The draws are a linear congruential sequence, its last kept in one cell of the scheduler’s, so that in JavaScript, where one domain takes turns, a program draws the same each run. scheduled counts the threads running or ready, one more for a thread as it is readied (before the one readying it may itself wait), one fewer for one that waits or ends (one put behind those ready, by a yield or by its fuel, is counted still): at none left before main is done every thread waits at a base event, a deadlock, and it comes to Nothing. Main’s answer ends it all, the other threads dropped where they stopped. A thread gives up its domain at its operations alone, and its fuel is counted at them: long pure work in a thread, with no operation in it, cannot be stopped, and holds its domain until it comes to one — the threads there wait for it, the one in its slot too, until a domain with nothing to do takes it, or the thread comes to an operation of the world’s. That is the program’s own to weigh: a pure loop that is to give the others their turns performs yield every so many rounds, what comes after it computed once the yield has taken effect. A computation held by an operation of w (Domain.tried c holds c) is run alone, as the operation does it: its spawns, channels and ivars are the scheduler’s, but a base event in it has no thread to meet, and is abandoned — unless it is in a choose with a branch that ends before its own.

A thread is a closed computation of the scheduler’s world, cml w <+> w: spawn c takes c as it is, and none of the handlers around the spawn — a recover, a state, a with’s resource — is around the thread, which runs on, on another domain, after they are done. What a thread needs it opens itself (its own attempt, its own with), or is given as a value (a channel, a socket, a nack). So each thread is under its own handlers alone, however many generations spawned it. A choose’s branches are not threads: they run in the choosing thread, in what is around the choose, and so in its world.

A thread’s world has a custodian of the scheduler’s, cml w <+> custodian <+> w, which covers the one outside. The scheduler’s world w need not name one: scheduled connects its custodian to the runtime’s custodians, through the domains’ (Domain.rooted), so a main that starts cml names none. The scheduler itself runs in w alone: only a thread’s operation of the world is run so connected, each by itself, and the scheduler’s own operations — a handoff’s dozen or two — cross no handler for it. A thread is a user of a custodian, not one of its things: what it carries is which custodian its withs give to, the one theirs gave to where it was spawned, and no shutdown stops it. A with k := Custodian.custody do (or contained) in a thread is answered by cml, as Racket’s parameterize is: the body stays in the thread — it waits at a channel, and gives up its turn, as anywhere else — and its withs give to k for its extent, the one before after it. That is the thread’s computation’s, carried by its continuation wherever its turns are taken, so no other thread’s withs give to k, and a throw that leaves the body leaves k with it. The custodian’s other operations are passed on to the one outside, k current there for them: a thing given it, a custodian made, a release kept. So one thread may serve each of its connections in a contained custodian of its own.

A thread that fails — abandons, fails in the runtime, or a throw no handler of its own hears comes to the scheduler’s world as a failure — is done with that, caught by the worker running it, which goes on with its loop: the other threads are not stopped. (One catch around a worker’s whole loop, not one around each turn; main’s turns, alone, each catch their own, so that a failure of main’s is known as such.) The scope collects it: once the run is over — main done, or every thread waiting — and the domains stopped, the first failure of a thread is the scope’s, scheduled (or the with) failing as that thread did, its words kept (Domain.fail), caught by a Domain.tried around it as a Left. A failure of main’s own ends the run there, as main’s answer would, the other threads dropped, and is the scope’s the same way.

Under scheduledWithReactor, each worker opens a group of the reactor on its domain, its threads’ operations of the world started there: one done at once goes on, one pending stops its thread, counted still (no deadlock while the world may come), and the worker takes its step once it is done, the thread readied in its slot. A worker asks its reactor, not waiting, every 8 (roundsBetween) rounds; with nothing to take and something pending, it waits in the reactor instead of on the condition, and a domain putting a turn among those ready where none waits on the condition wakes it there, as it does to stop. A choose whose branch’s operation is pending starts it in a group of its own, within the worker’s: committed by a partner, the choice’s group is closed by that worker, which the partner asks to, its operations let go of on the domain whose they are.

Chan

data Chan (w : HFunctor) a

A channel of as, of threads run in the world w: a rendezvous, a sender and a receiver each waiting for the other. (Its number, which orders the mutexes a sync holds; its mutex; the senders and the receivers waiting at it.)

IVar

data IVar (w : HFunctor) a

An ivar: a variable of threads run in the world w, written once and read any number of times, each reader waiting until it is written — a signal. (Its number, its mutex, what it holds, and the readers waiting for it.)

cml

cml : HFunctor -> HFunctor

For CML threads run in the world w: spawned and yielding, channels and ivars made, and events synced on. A thread’s world is cml w <+> custodian <+> w: the custodian there is the scheduler’s, which covers the one outside.

spawn

spawn : {e : HFunctor}
      -> {w : HFunctor}
      -> {{cm : cml w <: e}}
      -> Co ((cml w <+> Custodian.custodian) <+> w) Unit
      -> Co e Unit

c, a thread of its own; this one goes on. c is a computation of the scheduler’s world, cml w <+> Custodian.custodian <+> w: no handler around the spawn is around it, so what it needs — a recover, a state, a resource — it opens itself, or is given as a value.

yield

yield : {e : HFunctor} -> {w : HFunctor} -> {{cm : cml w <: e}} -> Co e Unit

The next thread’s turn; this one’s again after those ready.

newChan

newChan : {e : HFunctor}
        -> {w : HFunctor}
        -> {a : Type}
        -> {{cm : cml w <: e}}
        -> Co e (Chan w a)

A channel of as.

newIVar

newIVar : {e : HFunctor}
        -> {w : HFunctor}
        -> {a : Type}
        -> {{cm : cml w <: e}}
        -> Co e (IVar w a)

An ivar, holding nothing yet.

putIVar

putIVar : {e : HFunctor}
        -> {w : HFunctor}
        -> {a : Type}
        -> {{cm : cml w <: e}}
        -> IVar w a
        -> a
        -> Co e Unit

The ivar holds v now, every thread waiting to read it given it; once: a second put is abandoned. Never waits.

send

send : {e : HFunctor}
     -> {w : HFunctor}
     -> {a : Type}
     -> {{cm : cml w <: e}}
     -> Chan w a
     -> a
     -> Co e Unit

v sent on the channel, once a thread takes it: waits for the receiver. A base event: in a choose, its branch’s commit point.

recv

recv : {e : HFunctor}
     -> {w : HFunctor}
     -> {a : Type}
     -> {{cm : cml w <: e}}
     -> Chan w a
     -> Co e a

What a thread sends on the channel, once one does: waits for the sender. A base event.

readIVar

readIVar : {e : HFunctor}
         -> {w : HFunctor}
         -> {a : Type}
         -> {{cm : cml w <: e}}
         -> IVar w a
         -> Co e a

What the ivar holds, waiting until it is written. A base event.

never

never : {e : HFunctor}
      -> {w : HFunctor}
      -> {a : Type}
      -> {{cm : cml w <: e}}
      -> Co e a

A base event never ready: waits for ever, and in a choose is never the one committed.

choose

choose : {e : HFunctor}
       -> {w : HFunctor}
       -> {a : Type}
       -> {{cm : cml w <: e}}
       -> List (Co e a)
       -> Co e a

One of the branches: each run, in order, up to its first base event — what comes before it done as it comes, a guard’s work — then one of those base events committed, whichever can be, one drawn at random where several can, none with priority over another; where none can, whichever is met first. A branch that ends before any base event is ready at once, its value what it ends with. The branch committed goes on from its base event, what follows it the wrap; the others are abandoned there, each withNack of theirs told. A choose in a branch is that branch’s base events.

Nack

data Nack (w : HFunctor)

A nack, of threads run in the world w: ready once the choose its branch is in is left without that branch. Only withNack makes one, and only awaitNack waits for it: no thread readies it, the scheduler does. (The ivar the scheduler writes.)

withNack

withNack : {e : HFunctor}
         -> {w : HFunctor}
         -> {a : Type}
         -> {{cm : cml w <: e}}
         -> (Nack w -> Co e a)
         -> Co e a

f given its nack, the computation run: f nack, run as the rest of its branch, and nack ready once the choose it is in is left without this branch — another committed, its guard work failed, or its thread dropped before going on from it — so a thread waiting for it (awaitNack nack, a base event) knows it was not chosen. A value, not a computation of this thread’s world, so that a thread spawned in the guard, of the scheduler’s world, can be given it. Outside a choose, or where its branch is the one committed and its thread goes on, nack is never ready.

awaitNack

awaitNack : {e : HFunctor}
          -> {w : HFunctor}
          -> {{cm : cml w <: e}}
          -> Nack w
          -> Co e Unit

Once the nack is ready: its choose left without its branch. A base event, as an ivar’s read is.

scheduled

scheduled : {w : HFunctor}
          -> {a : Type}
          -> {{dm : Domain.domain <: w}}
          -> Co ((cml w <+> Custodian.custodian) <+> w) a
          -> Co w (Maybe a)

c and the threads it spawns, run on as many domains as the machine has cores (Domain.cores): Just main’s answer, the other threads dropped where they stopped; or Nothing where main is not done and every thread waits at a base event, a deadlock. A thread’s operation of the world is done where it is, holding its domain until it is. A thread that fails is done with that, the others going on; once the run is over, this fails as the first one that failed did (main’s failure ends the run). It runs in the threads’ world w, which need not name a custodian: the one in the threads’ world, which their withs give to, has the runtime’s custodians outside it, reached through the domains’ (Domain.rooted), or, where w names one, the one current where this runs.

scheduledWithReactor

scheduledWithReactor : {w : HFunctor}
                     -> {a : Type}
                     -> {{dm : Domain.domain <: w}}
                     -> {{rx : Reactor.reactor <: w}}
                     -> Co ((cml w <+> Custodian.custodian) <+> w) a
                     -> Co w (Maybe a)

scheduled, each domain waiting on the world through a reactor of its own (std.reactor’s, the C backend’s): a thread’s operation of the world that would wait — a socket read, an accept, a request sent, a sleep — is pending, the thread waiting, as at a base event, and the others running meanwhile; it goes on, on that domain, once the operation is done. In a choose, such an operation pending in a branch is that branch’s base event: committed once it is done, where no other was first, and else let go of, undone — a request not sent, a sleep not slept — so choose [recv ch, Time.sleep d] waits on the channel no longer than d. A thread waiting on the world is no deadlock.

Threads

data Threads

The threads of a with _ := CML.threads do: its body cml’s main thread, run as scheduled runs one.

threads

threads : Threads

with _ := CML.threads do ss: ss cml’s main thread, in the world of the block around with cml’s own (cml w <+> custodian <+> w, ss spawning, sending, choosing), it and the threads it spawns run on domains, as by scheduled; the with comes to Just the body’s value, or Nothing where every thread waits. The with is done once the scheduler is: no thread of it goes on after the block. The block’s world w need not have the custodian’s effect, as under scheduled, and a main that starts its threads names none.

ThreadsWithReactor

data ThreadsWithReactor

… and of a with _ := CML.threadsWithReactor do, run as scheduledWithReactor runs one.

threadsWithReactor

threadsWithReactor : ThreadsWithReactor

with _ := CML.threadsWithReactor do ss: CML.threads, each domain waiting on the world through a reactor of its own, as by scheduledWithReactor.

instanceBinderThreads

instance instanceBinderThreads : Binder Threads

A with of cml’s threads: no name, its body in a world with cml, and the with comes to what main’s answer is.

instanceBinderThreadsWithReactor

instance instanceBinderThreadsWithReactor : Binder ThreadsWithReactor

… with a reactor.

instanceHolderThreads

instance instanceHolderThreads : {e : HFunctor}
                               -> {{dm : Domain.domain <: e}}
                               -> Holder
                                 e
                                 Threads
                                 (\s -> Unit)
                                 (\w -> (cml w <+> Custodian.custodian) <+> w)
                                 (\r -> Maybe r)

cml’s threads held by a with: the body scheduled, its value main’s.

instanceHolderThreadsWithReactor

instance instanceHolderThreadsWithReactor : {e : HFunctor}
                                          -> {{dm : Domain.domain <: e}}
                                          -> {{rx : Reactor.reactor <: e}}
                                          -> Holder
                                            e
                                            ThreadsWithReactor
                                            (\s -> Unit)
                                            (\w ->
                                               (cml w <+> Custodian.custodian)
                                               <+> w)
                                            (\r -> Maybe r)

… with a reactor.