std.domain

For domains, as OCaml 5’s: computations run truly at once, each on a thread of the system of its own, and what synchronises them — cells every domain reads and writes (Atomic), mutexes and conditions. The base a scheduler is written on, in heff: its workers are domains. Import it by a name, import std.domain as Domain.

Caution

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

import co
import std.domain as Domain
import std.io

-- | `n` added to the counter, one at a time
adding : {e : HFunctor}
       -> {{dm : Domain.domain <: e}}
       -> Domain.Atomic Int
       -> Int
       -> Co e Unit
adding counter 0 = pure ()
adding counter n = do
  _ <- Domain.fetchAdd counter 1
  adding counter (n - 1)

counted : {e : HFunctor}
        -> {{io : stdio <: e}}
        -> {{dm : Domain.domain <: e}}
        -> Co e Unit
counted = do
  counter <- Domain.newAtomic 0
  with s := Domain.scope do
    _ <- Domain.spawn s (adding counter 1000)
    _ <- Domain.spawn s (adding counter 1000)
    pure ()
  n <- Domain.get counter
  print (debug n)

Operation	What it does
with s := scope do ss	ss run with s a scope: the with waits, at its end, for every domain spawned in it
spawn s c	c run on a domain of its own, one of the scope’s; this one goes on
cancel s	the scope’s mark set: no domain stopped
cancelled s	whether the mark is set: by cancel, a domain of the scope failing, or its body
join d	the domain’s answer, waiting for it to end
tried c	c run here: Right its answer, or Left why where it fails
fail why	this domain fails as why says: a tried’s Left handed on
cores	how many domains the machine runs at once
newAtomic v	a cell holding v, for every domain
get a / set a v	what it holds; … and it holds v now
cas a seen v	it holds v now, where it held seen: whether it did
fetchAdd a n	n added to the number it holds: what it held
newMutex / lock m / unlock m	a mutex, held by one domain at a time
newCondition	a condition, for domains to wait on
wait c m	m let go of, until the condition is signalled, then held again
signal c / broadcast c	one domain waiting on c woken; … every one
newQueue	a queue, for every domain: what is put in it is taken out once
put q v / take q	v put at the back, never waiting; the front taken out, waiting while empty
forever v	v, and all it holds, kept for as long as the program runs: counted by no domain
rooted c	c’s custodian the runtime’s custodians, for a world that names none: its withs in their custody, a failure at the root the program’s

cas compares by identity, as OCaml’s Atomic.compare_and_set: a number of a word or a constructor without fields is itself, anything else the value that was read, not an equal one built again. A wait may end without a signal: what it waits for is checked again, in a loop. A domain’s failure is its joiner’s, as it failed — unless the join is in a tried, which gives the failure back as a Left instead: so a failure of this domain’s own (an abandon, a runtime’s), or of one it joins, is caught where it is to be; fail hands a failure caught on, its words kept, as a join does. What is put in a queue is handed to the one domain that takes it, first in first out: a take waits while the queue is empty, a put never waits.

Domains are spawned in a scope, and only there: structured concurrency. with s := Domain.scope do ss runs ss here, in the block’s world with scoped, the scope’s own, and, at its end, waits for every domain spawned in the scope, the body free to do other work meanwhile. spawn s c is scoped’s: only the body spawns in the scope. c is a computation of the world around the with, which has no scoped, so a domain cannot spawn in its own scope — one that wants domains of its own opens a scope of its own. A domain of the scope that fails fails the scope: the with fails, once all of them have ended, as the first to fail did; one where the body fails, as the body did.

Cancelling is cooperative: the scope carries a mark, set by cancel, or where one of its domains fails, or its body does, and each domain looks at it where it chooses (cancelled) and winds up as it chooses. No domain is stopped from outside: stopped at an arbitrary operation, it would keep a mutex it holds locked, and the release of what it holds would not run. A domain in a call of the system that waits, or in a loop with no operation, ends only where it looks at the mark; a loop that never ends is fuel’s to stop. A body left by a throw handled outside the with (an exception’s) leaves its domains running, not waited for.

A domain’s computation is of the world around its scope’s with, and every handler between there and the program’s world runs it too, on its domain (a domain of the runtime’s can only be given the program’s world’s computations, and those it is given are the spawn’s, handled on their way to it); tried’s runs here, at the call, in what is around it. So the schedulers written on domains — cml’s, boc’s — take their threads and behaviours as closed computations of their own world instead, and each runs them on its workers, in a scope of its own, with none of the handlers around where they were spawned.

What runs the domains is the backend’s runtime, the program the same on each. A domain, a cell, a mutex and a condition are the runtime’s own, held by the program as values of no constructor, and each is freed with the program’s last reference to it — a cell letting go of what it holds, a domain of its answer. The C backend’s (domain.provider.c): a domain is a thread of the system, a cell is changed atomically, a mutex and a condition are the system’s. What a domain gives back is shared (heff_share), not copied; what a domain is given, and what is put in a queue, is moved where the domain giving it held it alone (heff_move: counted by the taker alone from then on), and shared otherwise. A domain whose last reference goes while it still runs is freed as its thread ends. The program ends where main does, domains not joined with it.

JavaScript’s (domain.provider.js): one domain, as one core runs threads. The domains take turns, each at its operations of this effect: at each, the others ready go first, so a domain waiting for a cell another changes lets it be changed. One waiting on a mutex, a condition or a domain’s end waits there, the others going on. cores is 1. A program whose domains all wait, for one another, stops there, said by nothing: the page cannot tell it from one waiting for something of the world’s.

Domain

data Domain a

A domain whose answer is an a. (The runtime’s own, a foreign value: no value of the program has it.)

Atomic

data Atomic a

A cell holding an a, for every domain. (The runtime’s own, a foreign value: no value of the program has it.)

Mutex

data Mutex

A mutex. (The runtime’s own, a foreign value: no value of the program has it.)

Condition

data Condition

A condition. (The runtime’s own, a foreign value: no value of the program has it.)

Queue

data Queue a

A queue of as, for every domain: what one domain puts in, exactly one domain takes out, first in first out. (The runtime’s own, a foreign value: no value of the program has it.)

domain

domain : HFunctor

For OS threads, domains: spawned and joined, a failure caught, and what they share — atomics, mutexes, conditions and queues.

join

join : {e : HFunctor}
     -> {a : Type}
     -> {{dm : domain <: e}}
     -> Domain a
     -> Co e a

The domain’s answer, waiting for it to end; where it failed, this one fails as it did.

tried

tried : {e : HFunctor}
      -> {a : Type}
      -> {{dm : domain <: e}}
      -> Co e a
      -> Co e (Either String a)

c run here, on this domain, its failure caught: Right its answer, or Left why where it fails — abandons (heff:abandon), fails in the runtime, or joins a domain that failed — the rest of c not run.

fail

fail : {e : HFunctor} -> {a : Type} -> {{dm : domain <: e}} -> String -> Co e a

This domain fails as why says, as one joined fails where the domain it joins failed: caught by a tried around it, Left why, and else the domain’s — or, on main’s, the program’s, said. So a failure caught (a tried’s Left) is handed on as it came, its words kept; "heff:abandon", an abandon’s, abandons.

cores

cores : {e : HFunctor} -> {{dm : domain <: e}} -> Co e Int

How many domains the machine runs at once: its cores, as the system says (1 where it does not).

newAtomic

newAtomic : {e : HFunctor}
          -> {a : Type}
          -> {{dm : domain <: e}}
          -> a
          -> Co e (Atomic a)

A cell holding v, for every domain.

get

get : {e : HFunctor} -> {a : Type} -> {{dm : domain <: e}} -> Atomic a -> Co e a

What the cell holds.

set

set : {e : HFunctor}
    -> {a : Type}
    -> {{dm : domain <: e}}
    -> Atomic a
    -> a
    -> Co e Unit

… and it holds v now.

cas

cas : {e : HFunctor}
    -> {a : Type}
    -> {{dm : domain <: e}}
    -> Atomic a
    -> a
    -> a
    -> Co e Bool

The cell holds v now, where it held seen (compared by identity): whether it did.

fetchAdd

fetchAdd : {e : HFunctor}
         -> {{dm : domain <: e}}
         -> Atomic Int
         -> Int
         -> Co e Int

n added to the number the cell holds: what it held.

newMutex

newMutex : {e : HFunctor} -> {{dm : domain <: e}} -> Co e Mutex

A mutex, held by no domain.

lock

lock : {e : HFunctor} -> {{dm : domain <: e}} -> Mutex -> Co e Unit

The mutex held by this domain, waiting while another holds it.

unlock

unlock : {e : HFunctor} -> {{dm : domain <: e}} -> Mutex -> Co e Unit

… let go of: it fails where this domain does not hold it.

newCondition

newCondition : {e : HFunctor} -> {{dm : domain <: e}} -> Co e Condition

A condition, for domains to wait on.

wait

wait : {e : HFunctor} -> {{dm : domain <: e}} -> Condition -> Mutex -> Co e Unit

The mutex, held by this domain, let go of until the condition is signalled, and held again before it goes on. It may end without a signal: what it waits for is checked again.

signal

signal : {e : HFunctor} -> {{dm : domain <: e}} -> Condition -> Co e Unit

One domain waiting on the condition woken, if one is.

broadcast

broadcast : {e : HFunctor} -> {{dm : domain <: e}} -> Condition -> Co e Unit

Every domain waiting on the condition woken.

newQueue

newQueue : {e : HFunctor}
         -> {a : Type}
         -> {{dm : domain <: e}}
         -> Co e (Queue a)

A queue, for every domain, holding nothing yet.

put

put : {e : HFunctor}
    -> {a : Type}
    -> {{dm : domain <: e}}
    -> Queue a
    -> a
    -> Co e Unit

v put at the back of the queue, for one domain to take; never waits.

take

take : {e : HFunctor} -> {a : Type} -> {{dm : domain <: e}} -> Queue a -> Co e a

The front of the queue taken out, this domain’s alone now; waits while the queue is empty.

forever

forever : {e : HFunctor} -> {a : Type} -> {{dm : domain <: e}} -> a -> Co e a

v itself, kept for as long as the program runs, with all it holds: counted by no domain from now on, as a definition’s value is, and never let go of — for what every domain reads all through a run, made once (a scheduler’s cells, say), whose count would otherwise be changed by each domain at once. What it holds is kept too: a cell’s or a queue’s contents are not, being changed.

Scope

data Scope s (w : HFunctor)

A scope of domains, with s := Domain.scope do: its domains and its cancel mark. s is the region of the with that made it, so the scope cannot leave the block; w is the world of the block around, its domains’ world.

scoped

scoped : HFunctor -> HFunctor

A scope’s body’s own: domains spawned in the scope, computations of w, the world of the block around the with. Only the body has it, not a domain’s computation: no domain spawns in its own scope.

Scoping

data Scoping

What a with s := Domain.scope do opens: a scope of domains.

scope

scope : Scoping

with s := Domain.scope do ss: ss run here, in the block’s world with scoped, its own, s a scope its domains are spawned in (spawn s c); the with waits, at its end, for every domain spawned in it, and comes to what ss came to.

spawn

spawn : {e : HFunctor}
      -> {w : HFunctor}
      -> {s a : Type}
      -> {{sp : scoped w <: e}}
      -> Scope s w
      -> Co w a
      -> Co e (Domain a)

c run on a domain of its own, one of the scope’s; this one goes on. The scope’s with waits for it at its end, and join gives its answer. Where it fails, the scope is cancelled, and fails at its end as the first of its domains to fail did. Only the scope’s body spawns in it: c is of the world around the with, w, where there is no scoped; each handler between there and the program’s world runs it too, on its domain.

cancel

cancel : {e : HFunctor}
       -> {w : HFunctor}
       -> {s : Type}
       -> {{dm : domain <: e}}
       -> Scope s w
       -> Co e Unit

The scope cancelled: its mark set. No domain of it is stopped: each looks at the mark where it chooses (cancelled), and winds up as it chooses.

cancelled

cancelled : {e : HFunctor}
          -> {w : HFunctor}
          -> {s : Type}
          -> {{dm : domain <: e}}
          -> Scope s w
          -> Co e Bool

Whether the scope is cancelled: by cancel, or as one of its domains failed, or its body did.

instanceBinderScope

instance instanceBinderScope : Binder Scoping

A with of a scope: its name the scope, of the world of the block around, its body in that world with scoped, and the with comes to what the body came to.

instanceHolderScope

instance instanceHolderScope : {e : HFunctor}
                             -> {{dm : domain <: e}}
                             -> Holder
                               e
                               Scoping
                               (\s -> Scope s e)
                               (\w -> scoped w <+> w)
                               (\r -> r)

A scope held by a with: made, the body run with it, and every domain spawned in it waited for at the body’s end — where the body fails too, the scope cancelled first. Then the with fails as the body did, or as the first of the scope’s domains to fail did, or comes to the body’s answer.

rooted

rooted : {e : HFunctor}
       -> {a : Type}
       -> {{dm : domain <: e}}
       -> Co (e <+> Custodian.custodian) a
       -> Co e a

c, its custodian’s operations the runtime’s custodians’, as a world with the custodian’s effect has them: the things its withs hold in their custody, a failure that reaches the root the program’s. So a world without that effect — a main that does not name it — has custodians all the same, through the domains’, whose provider passes the operations on; and c’s is the only one in its world. In a world with the custodian’s effect, c’s are under the one current where it runs.