boc

Behaviour-oriented concurrency (Cheeseman et al., OOPSLA 2023), on std.domain: a cown holds a value; when c body spawns a behaviour, which later, once, with every cown of c its own at once, is given what they hold and gives back what they are to hold after it. Behaviours whose cowns overlap run one after another, in the order they were spawned; the others run at once, on as many domains as the machine has cores. A behaviour takes its cowns all at once, never one and then another, so behaviours do not deadlock on them. Import it by a name, import boc as BOC.

Caution

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

import boc as BOC
import co
import custodian as Custodian
import std.domain as Domain

-- | `n` moved from one account to the other: one behaviour on both
paid : {e w : HFunctor}
     -> {{bc : BOC.boc w <: e}}
     -> BOC.Cown w Int
     -> BOC.Cown w Int
     -> Int
     -> Co e Unit
paid from to n = do
  with x := from
       y := to do
    x := x - n
    y := y + n

-- | alice given 10, then 5 paid to bob; what bob has then, written
-- | by a last behaviour on bob, which comes after the others on him
bobs : {e w : HFunctor}
     -> {{bc : BOC.boc w <: e}}
     -> {{dm : Domain.domain <: e}}
     -> {{dw : Domain.domain <: w}}
     -> Co e (Domain.Atomic Int)
bobs = do
  alice <- BOC.newCown 0
  bob <- BOC.newCown 0
  with a := alice do
    a := a + 10
  paid alice bob 5
  seen <- Domain.newAtomic 0
  with b := bob do
    Domain.set seen b
  pure seen

-- | the behaviours run, every one done: what bob has, 5
bobHas : {e : HFunctor}
       -> {{dm : Domain.domain <: e}}
       -> {{cu : Custodian.custodian <: e}}
       -> Co e Int
bobHas = do
  seen <-
    BOC.scheduled
      (\why -> Domain.fail why)
      (bobs (bc := _) (dm := _) (dw := _))
  Domain.get seen

Operation	What it does
newCown v	a cown holding v
when c body	a behaviour spawned on the cown c, or a tuple of them; this one goes on
with a := c do ...	the same, its body statements, a what c holds (more cowns, a binding each)
with a := c where p do ...	the same, its body run once p holds of what the cowns hold: until then, the behaviour waits for one p reads to be written
with r := BOC.await act do ...	act, of the world, run outside every behaviour; the body a behaviour once it has come to r; this one goes on
with a := c / r := BOC.await act do ...	the same, the body a behaviour on c once act has come to r
with r := BOC.awaitFirst a b do ...	a and b raced: the body once the first has come to its value, r Left or Right it, the other given up
scheduled failed c	c and its behaviours run, on domains, every behaviour waited for; failed why where one fails
scheduledWithReactor failed c	the same, each domain running acts awaited in a reactor of its own, every act waited for too
scheduled (batch := n) failed c	either, each domain running at most n behaviours in a row before the others ready get their turn (64 when not given)

A behaviour’s body is given what its cowns hold, a tuple as the cowns are ((a, b, log) hands it an (x, y, l), nesting to the left), and gives back their new contents, the same shape: Cowns says what a cown or a tuple of them holds. A with of cowns is a behaviour too, each cown bound to a name (with x := from and y := to under it), its statements the body, the names what they hold, set to change it: only the cowns whose names it sets are written back, and the with comes to (). A with of cowns with a condition, with a := c where p do ..., is a behaviour that, once it has its cowns, checks p of what they hold: where it does not hold, the behaviour lets go of them, untouched, and waits until a behaviour writes a cown whose name p reads; then it is queued again on all of them, behind that one, and checks p again (the paper’s whenever). One still waiting once every other behaviour is done is dropped, its body never run. The body is a closed computation of the scheduler’s world, boc w <+> w, run on whichever domain takes it, later: none of the handlers around the when (or the with) is around it — a recover, a state, a resource of a with — so what it needs it opens itself, or is given as a value. It may spawn behaviours, on its own cowns too (they run after it), and do what else the scheduler’s world allows, whose providers must then be safe on threads. A body that waits holds its cowns while it waits, and every behaviour behind it on them waits too: what it would wait for it awaits instead (below). There is no barrier: a behaviour that is to come after others on a cown is spawned after them on it, and scheduled gives main’s answer once every behaviour is done. The same cown twice in one when is abandoned when the when runs.

So a behaviour runs before every behaviour spawned after it on a cown they share, wherever in the source it is. A report meant to say what the cowns hold once a server is done, written as a with of them as the server starts, runs first, before any request, and says what they held then: it reads as “at the end” and is not. What is to come after the server is spawned once the server is done, in the body of the with that runs then — after the act that waits for the server’s end (r := BOC.await (Signal.wait [Terminate])), say — where it comes after every behaviour spawned before it on those cowns.

A behaviour is a user of a custodian, not one of its things, as a cml thread is: it takes the custodian current where it is spawned — k in a with k := Custodian.custody do (or contained), else the one current where scheduled runs — and its body runs with that one current, so the things its withs hold are in its custody, and the behaviours it spawns take it too. An act awaited, and the behaviour after it, take the one current at the await, and the act is one of its things, as what a with holds is: under scheduledWithReactor, where that custodian is shut down while the act waits, the act is given up — its wait taken out of the reactor, what comes after it let go of — and the behaviour after it is never spawned. So a server’s /stop that shuts down the custody its acts were awaited in — with k := Custodian.custody do around them — lets go of the act waiting for a signal, and the run ends. One that has come to its value is not given up: its behaviour is spawned. There is no handle to give up one act: an act given a custody of its own, shut down, is that. awaitFirst a b does it for two: it awaits both in a custody of its own, and the first to come to its value shuts it down. No shutdown stops a behaviour. A with of a custodian in a body is the body’s, for its extent, since a behaviour runs to its end without waiting. The custodian is the one of the scheduler’s world: scheduled asks for custodian <: w, and a main that runs it names custodian in its world.

A behaviour whose body fails — abandons, or fails in the runtime — is done with that: its cowns hold what they held, since what they are to hold is written after the body (Domain.tried catches the failure). Then scheduled’s failed, given why, is run, a computation of the world, on the behaviour’s domain while the behaviour still holds its cowns: one after it on them comes after that. Then the cowns are handed on as if the behaviour had ended, and the other behaviours, and main, go on. failed runs on whichever domain a behaviour fails on, at once with the others, so what it does must be safe on threads. A failed that itself fails is the scope’s: scheduled, once every behaviour is done, fails as the first such failed did, its words kept, instead of giving main’s answer (the others are not stopped): \why -> Domain.fail why makes any failure of a behaviour the run’s, as it came.

A behaviour runs from its start to its end and never waits on the world: what it would wait for — a connection accepted, a socket read, a sleep — it awaits, as Verona’s behaviours do, by a with whose last binding is r := BOC.await act. The with waits for nothing, and the behaviour goes on: act, a computation of the scheduler’s world w (no when in it, nor an await), runs outside every behaviour, and once it has come to its value, the body is a behaviour of its own, r that value — of the scheduler’s world too, as a when’s body is, since it runs later, elsewhere. With cowns bound before it (with x := c and r := BOC.await act under it; several cowns, a tuple of them to one name, x := (c0, c1)), it is a behaviour on them, spawned only then: no cown is held while the act waits, and behaviours on a cown awaiting acts come in the order their acts came to their values. What an act fails at is its value, for the body to handle — Net.read’s Either NetError Bytes, a time limit its own (Net.read (timeout := 5000) c n); failed hears only a body that fails.

import boc as BOC
import co
import std.duration as Duration
import std.time

-- | a second's sleep awaited, then 1 added to the count, by a
-- | behaviour on it: the count is held by none meanwhile
ticked : {e w : HFunctor}
       -> {{bc : BOC.boc w <: e}}
       -> {{clock : time <: w}}
       -> BOC.Cown w Int
       -> Co e Unit
ticked count = do
  with n := count
       _ := BOC.await (sleep (Duration.seconds 1)) do
    n := n + 1

Under scheduledWithReactor, each domain has a group of std.reactor’s of its own: an act awaited by a behaviour is started there once that behaviour is done, pending there with the others while it waits, and after every 64th behaviour the domain takes the acts come to their values — a look at every act pending there, which costs as many as there are — spawning the behaviours after them, which it keeps in its slot as it would one a body spawned, and the rest in a queue of its own. A domain with no behaviour to run takes one from another’s queue; with none there either and acts pending, it waits in its reactor, until one comes to its value or a behaviour is put in a queue. The run ends once no behaviour runs or is ready and no act is pending: a server whose listener is closed ends once its connections are done. An act awaited by main is started by a behaviour on no cown, on whichever domain takes it. An act that itself fails — abandons, or fails in the runtime, not an error it comes to — is as a body that fails: failed is given why, on the domain it ran on, the with’s body is never run, and every other act and behaviour goes on (it held no cown, so none is let go of). Each step of an act runs under a catch for that, as a body does. Under scheduled, an act is run where it is awaited, there and then, the behaviour holding its domain and its cowns until it is done: scheduled is for programs that await nothing.

The scheduling is the paper’s, as Verona’s runtime has it: each cown has a queue, kept as the last request for it, and a behaviour is spawned in two phases. First it comes to the queue of each of its cowns, in the order of the cowns, by swapping itself in as the last request, linked behind the one before it; then each of its requests is marked come, and only then may one behind it link to it. It counts the cowns it still waits for (and one more, for its spawning) and runs when none is left. When it ends, each of its requests hands its cown to the one linked behind it, or, where none is, takes itself out as the last. No lock is held for any of it: a request is a cell (Domain.Atomic) holding its link, changed by cas, and told from the others by the cell it is. A behaviour whose turn has come is put in a queue (Domain.Queue) the domains running behaviours take from — unless its turn came by a behaviour running on one of those domains, spawning it or ending and handing it a cown: then that domain keeps it, one at a time, and runs it next itself, as the paper’s threads keep a batch of their own, until it has run its batch in a row, when it puts the next in the queue, so the others are not starved; a behaviour spawned by main is put in the queue. Under scheduledWithReactor, a domain keeps those beyond the one in a queue of its own instead — a cell changed by cas, no lock — and runs them after it, in their order; a domain with nothing to run takes the front of another’s, and a domain that puts one there wakes a domain waiting, where one does. Only the shared queue, and a domain about to wait, take a lock. The order behaviours run in is the cowns’ queues’ still: one comes to a domain’s queue only once its turn has come.

The batch is 64 behaviours, or what batch is given (scheduled (batch := 16) failed c). Longer batches keep a chain of behaviours on one domain, its cowns’ cells warm there, and go through the queue — its lock, and waking the domain that takes from it — less often; the behaviours waiting in the queue wait for them meanwhile. On 14 cores, 64 chains of 5000 behaviours, each spawning the next on its cown once an act it awaited came back, ran 1.17 million behaviours a second on 14 domains with batches of 64, 1.02 million with 16 and 0.51 million with 4. std.http.bocserver, 256 connections on 14 domains, answered 92 to 93 thousand requests a second with batches of 64 or 16, with a 99th percentile of 5 ms and the slowest in 9 to 15 ms, and 86 thousand with 4, no faster at the tail. A shorter batch lets the behaviours in the queue in sooner, at the cost of the chains; worth it where one domain’s chains keep many others waiting.

A behaviour is never stopped partway — its body runs to its end, holding its cowns — so the one a domain keeps would wait for the end of the body it runs, however long that goes on. The domain counts the operations of that body as it hands them on (the world’s, and when and newCown), and at every 256th puts the behaviour it keeps in the queue, which wakes a domain waiting there to take it: a behaviour kept waits for at most 256 operations of the body. A body that computes long doing none holds its domain, and the one kept, until it ends; that is the program’s to avoid.

Cown

data Cown (w : HFunctor) a

A cown holding an a, of behaviours run in the world w.

Cowns

theory Cowns c where
  World : HFunctor
  Contents : Type
  width : Int
  spread : List Bool -> List Bool
  handles : c -> List (Handle World)
  read : (Domain.domain <: World) -> c -> Co World Contents
  write : (Domain.domain <: World)
        -> c
        -> List Bool
        -> Contents
        -> Co World Unit

What a behaviour can be on: a cown, or a tuple of them ((a, b, c), nesting to the left); the world their behaviours run in, what they hold, how many cowns, their queues, and how what they hold is read and written — written where its Bool says, one a cown, in order. spread makes those Bools from a with’s, one a name: its names bound along the pairs to the right (with a := c0, b := (c1, c2) and c := c3 binds (c0, ((c1, c2), c3))), the last to what is left, each name’s Bool for every cown it holds.

instanceCownsCown

instance instanceCownsCown : {w : HFunctor} -> {a : Type} -> Cowns (Cown w a)

A cown: what it holds.

instanceCownsPair

instance instanceCownsPair : {c d : Type}
                           -> {{l : Cowns c}}
                           -> {{r : Cowns d @ { World = l.World }}}
                           -> Cowns (c, d)

Two (each a cown or a tuple) of one world: the pair of what they hold.

boc

boc : HFunctor -> HFunctor

For behaviours on cowns, run in the world w: cowns made, behaviours queued on them, each run once its cowns are free, and acts of the world awaited, outside every behaviour. A behaviour’s body is a computation of the scheduler’s world, boc w <+> w: no handler around the when is around it.

newCown

newCown : {e : HFunctor}
        -> {w : HFunctor}
        -> {a : Type}
        -> {{bc : boc w <: e}}
        -> a
        -> Co e (Cown w a)

A cown holding v.

when

when : {c : Type}
     -> {e : HFunctor}
     -> c
     -> {{cw : Cowns c}}
     -> {{bc : boc cw.World <: e}}
     -> (cw.Contents -> Co (boc cw.World <+> cw.World) cw.Contents)
     -> Co e Unit

A behaviour on the cowns cs, one or a tuple of them, spawned; this one goes on. Its turn comes once every behaviour spawned before it on any of them is done; then body is given what they hold, a tuple as cs is, and what it gives back is what they hold after. The body is a computation of the scheduler’s world, boc w <+> w, no handler around the when around it: what it needs, it opens itself, or is given as a value. The same cown twice is abandoned.

instanceBinderCown

instance instanceBinderCown : {w : HFunctor} -> {a : Type} -> Binder (Cown w a)

A with of a cown: a behaviour on it, spawned (with a := c do ...: a what it holds); this one goes on, and the with comes to nothing.

instanceBinderCowns

instance instanceBinderCowns : {w : HFunctor}
                             -> {a b : Type}
                             -> {{cw : Cowns (Cown w a, Cown w b)}}
                             -> Binder (Cown w a, Cown w b)

A with of two cowns, each bound to a name (with a := c0 and b := c1 under it): one behaviour on both, which takes them at once.

instanceBinderCownsMore

instance instanceBinderCownsMore : {w : HFunctor}
                                 -> {a d f : Type}
                                 -> {{cw : Cowns (Cown w a, (d, f))}}
                                 -> Binder (Cown w a, (d, f))

… of more cowns (with a := c0, b := c1 and c := c2): one behaviour on all of them, which takes them all at once.

instanceHolderCown

instance instanceHolderCown : {e : HFunctor}
                            -> {w : HFunctor}
                            -> {a : Type}
                            -> {{bc : boc w <: e}}
                            -> Holder
                              e
                              (Cown w a)
                              (\s -> a)
                              (\x -> boc w <+> w)
                              (\r -> Unit)

A behaviour on a cown held by a with: its body’s names set are what the cown holds after it; one only read is not written back.

instanceHolderCowns

instance instanceHolderCowns : {e : HFunctor}
                             -> {w : HFunctor}
                             -> {a b : Type}
                             -> {{cw : Cowns (Cown w a, Cown w b)}}
                             -> {{bc : boc cw.World <: e}}
                             -> Holder
                               e
                               (Cown w a, Cown w b)
                               (\s -> cw.Contents)
                               (\x -> boc cw.World <+> cw.World)
                               (\r -> Unit)

… on two cowns.

instanceHolderCownsMore

instance instanceHolderCownsMore : {e : HFunctor}
                                 -> {w : HFunctor}
                                 -> {a d f : Type}
                                 -> {{cw : Cowns (Cown w a, (d, f))}}
                                 -> {{bc : boc cw.World <: e}}
                                 -> Holder
                                   e
                                   (Cown w a, (d, f))
                                   (\s -> cw.Contents)
                                   (\x -> boc cw.World <+> cw.World)
                                   (\r -> Unit)

… on more.

instanceWaiterCown

instance instanceWaiterCown : {e : HFunctor}
                            -> {w : HFunctor}
                            -> {a : Type}
                            -> {{bc : boc w <: e}}
                            -> Waiter
                              e
                              (Cown w a)
                              (\s -> a)
                              (\x -> boc w <+> w)
                              (\r -> Unit)

A behaviour on a cown held by a with with a condition, with a := c where p do ...: once it has the cown, p checked of what it holds; where it does not hold, the cown let go of, untouched, and the behaviour waits until a behaviour writes it, then is spawned again, behind that one (the paper’s whenever).

instanceWaiterCowns

instance instanceWaiterCowns : {e : HFunctor}
                             -> {w : HFunctor}
                             -> {a b : Type}
                             -> {{cw : Cowns (Cown w a, Cown w b)}}
                             -> {{bc : boc cw.World <: e}}
                             -> Waiter
                               e
                               (Cown w a, Cown w b)
                               (\s -> cw.Contents)
                               (\x -> boc cw.World <+> cw.World)
                               (\r -> Unit)

… on two cowns: let go of both, and waiting on those p reads.

instanceWaiterCownsMore

instance instanceWaiterCownsMore : {e : HFunctor}
                                 -> {w : HFunctor}
                                 -> {a d f : Type}
                                 -> {{cw : Cowns (Cown w a, (d, f))}}
                                 -> {{bc : boc cw.World <: e}}
                                 -> Waiter
                                   e
                                   (Cown w a, (d, f))
                                   (\s -> cw.Contents)
                                   (\x -> boc cw.World <+> cw.World)
                                   (\r -> Unit)

… on more.

Await

data Await (w : HFunctor) a

What a with awaits, r := BOC.await act or r := BOC.awaitFirst a b: it comes to an a, outside every behaviour, and the with’s body is a behaviour once it has. (An act of the world w; or a race, which, in a behaviour of its own, awaits its acts, given what comes after the first.)

await

await : {w : HFunctor} -> {a : Type} -> Co w a -> Await w a

act awaited by a with: with r := BOC.await act do ....

awaitFirst

awaitFirst : {w : HFunctor}
           -> {a b : Type}
           -> {{dm : Domain.domain <: w}}
           -> {{cu : Custodian.custodian <: w}}
           -> Co w a
           -> Co w b
           -> Await w (Either a b)

a and b awaited by a with, raced: with r := BOC.awaitFirst a b do ..., r Left what a came to or Right what b did, whichever came to its value first. Both are awaited in a custody of their own, under the one current; the first to come to its value shuts it down, which gives up the other, and the body is a behaviour on that one’s value alone. A time limit is a race with a sleep. Under scheduled, which runs each act where it is awaited, a is run, then b, and a comes first.

instanceBinderAwait

instance instanceBinderAwait : {w : HFunctor}
                             -> {a : Type}
                             -> Binder (Await w a)

A with of an act awaited, with r := BOC.await act do ...: r what the act comes to; the with comes to nothing at once.

instanceBinderCownsAwait

instance instanceBinderCownsAwait : {c : Type}
                                  -> {w : HFunctor}
                                  -> {a : Type}
                                  -> {{cw : Cowns c @ { World = w }}}
                                  -> Binder (c, Await w a)

A with of cowns and an act awaited, the act the last binding (with x := c and r := BOC.await act under it): x what c, a cown or a tuple of them, holds, and r what the act comes to.

instanceHolderAwait

instance instanceHolderAwait : {e : HFunctor}
                             -> {w : HFunctor}
                             -> {a : Type}
                             -> {{bc : boc w <: e}}
                             -> Holder
                               e
                               (Await w a)
                               (\s -> a)
                               (\x -> boc w <+> w)
                               (\r -> Unit)

An act awaited by a with: the act run outside every behaviour, and once it has come to its value, the body a behaviour on no cown, given it. The behaviour asking goes on at once.

instanceHolderCownsAwait

instance instanceHolderCownsAwait : {e : HFunctor}
                                  -> {w : HFunctor}
                                  -> {c a : Type}
                                  -> {{cw : Cowns c @ { World = w }}}
                                  -> {{bc : boc w <: e}}
                                  -> Holder
                                    e
                                    (c, Await w a)
                                    (\s -> (cw.Contents, a))
                                    (\x -> boc w <+> w)
                                    (\r -> Unit)

… and with cowns: once the act has come to its value, the body a behaviour on them, spawned then — so behaviours on a cown are in the order their acts came to their values — its names set what they hold after it, as a with of the cowns alone.

scheduled

scheduled : {w : HFunctor}
          -> {a : Type}
          -> {batch : Int := 64}
          -> {{dm : Domain.domain <: w}}
          -> {{cu : Custodian.custodian <: w}}
          -> (String -> Co w Unit)
          -> Co (boc w <+> w) a
          -> Co w a

c and the behaviours it spawns, run on as many domains as the machine has cores (Domain.cores), every behaviour waited for: main’s answer. A behaviour whose body fails is done with that, its cowns holding what they held: failed why is run on its domain, while it still holds them, and the others go on. Where a failed fails too, this fails as the first such failed did, once every behaviour is done, instead of giving the answer; where main fails, every behaviour is waited for, and this fails as main did. An act awaited (await) is run where it is awaited, there and then, the behaviour holding its domain, and its cowns, until it is done. A behaviour runs with the custodian current where it was spawned, w’s. A domain runs at most batch behaviours in a row that it made ready itself before the others ready get their turn: fewer, for the others to wait less; more, for long chains of behaviours to run faster.

scheduledWithReactor

scheduledWithReactor : {w : HFunctor}
                     -> {a : Type}
                     -> {batch : Int := 64}
                     -> {{dm : Domain.domain <: w}}
                     -> {{cu : Custodian.custodian <: w}}
                     -> {{rx : Reactor.reactor <: w}}
                     -> (String -> Co w Unit)
                     -> Co (boc w <+> w) a
                     -> Co w a

scheduled, each domain waiting on the world through a reactor of its own (std.reactor’s, the C backend’s): an act awaited (await) is run outside every behaviour, started in the reactor of the domain whose behaviour awaited it once that behaviour is done, and the behaviour that is to follow it spawned on that domain once it has come to its value. A domain with no behaviour to run and acts pending waits in its reactor, until one has come to its value, or a behaviour is ready. Every behaviour, and every act awaited, is waited for, but an act given up: one whose custodian is shut down while it waits, its with’s body never run. An act that fails — abandons, or fails in the runtime — is as a body that fails: failed given why, its with’s body not run, the others going on. batch as scheduled’s.