std.thread

For OS threads: work run truly at once, on std.domain’s domains — a pool of them mapping a function over a list (parMap), a computation run on n of them, each given its index (spread), and Parallel handled by them, each side a domain (inThreads). A library: no provider of its own.

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

-- | the primes below `n`
primesBelow : Int -> Int
primesBelow n = List.length (List.keepIf isPrime (List.range 2 (n - 1)))
  where
  isPrime : Int -> Bool
  isPrime k = List.all (\d -> k % d /= 0) (List.range 2 (k / 2))

counted : {e : HFunctor}
        -> {{io : stdio <: e}}
        -> {{dm : Domain.domain <: e}}
        -> Co e Unit
counted = do
  n <- cores
  counts <- parMap n (\i -> primesBelow (1000 * (i + 1))) (List.range 0 7)
  print (debug counts)
  names <- parMap 4 (\s -> s ^ "!") ["a", "b", "c"]
  print (joinWith " " names)
  squares <- spread 4 (\i -> pure (i * i))
  print (debug squares)

Each asks for std.domain’s effect, so it runs wherever domains do, in JavaScript’s one domain too.

A task may take and give values of any type.
f and the values are shared with the domains, not copied: a large value every task reads is in memory once.
Updating a shared value copies it while another domain holds it.
If a task fails, the others stop taking more, and the caller fails as the first failed task did, in the list’s order: the program fails as it would have, one domain doing all.

A spread’s domains each run the computation it is given, effects and all: what each prints, it prints.

Safe in threads at once: pure code and the definitions it reads, std.io (each write is whole), and std.reference’s cells (locked). Not safe:

exit in any thread ends the process.
A provider’s own tables are its own to lock. Among the library’s, std.progress locks its own, and the others keep none.
One thread letting go of a host’s thing while another uses it is the providers’ to prevent.
Windows is not tested.

A provider that starts threads, as std.domain’s does, says so, on a line of its own:

#define HEFF_THREADS 1

The whole program is then built for threads. A program none of whose providers says it is built as before, and runs as fast as before. What such a provider uses, of the C runtime:

Function	What it does
`heff_share(v)`	mark `v` shared, before handing it to another thread
`heff_try(f, x, &out)`	run `f x`, catching a failure: `NULL`, or why it failed
`heff_fail_again(why)`	fail, in the joining thread, as the thread did
`heff_thread_start(&t, run, arg)`	start a thread with a large stack
`heff_thread_end()`	give the thread’s memory back as it ends
`heff_freeze(v)`	make `v` immortal: never freed or counted
`HEFF_TLS`	declare per-thread state

parMap

parMap : {e : HFunctor}
       -> {{dm : Domain.domain <: e}}
       -> {b a : Type}
       -> Int
       -> (b -> a)
       -> List b
       -> Co e (List a)

f of each of xs, by n domains (the caller one of them), each taking the next value as it ends one: the answers, in order. f and each value are shared with the domains, not copied. A task that fails stops the others taking more, and the first that failed, in the list’s order, fails the caller. One domain, or one value, is the caller alone.

cores

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

How many threads the machine runs at once: its cores, as the system says (1 where it does not), as std.domain’s cores.

threaded

threaded : {e : HFunctor}
         -> {{dm : Domain.domain <: e}}
         -> {a b x : Type}
         -> ParallelF a b (Co e) x
         -> Co e x

Parallel into Co e, each side a domain: the left this one, the right one of its own, in a scope of their own. A side’s pure work is done where it is handled, before its domain starts, unless it comes after an operation or after later (parallelIn says so): parallelIn (later (\u -> fib n)) .... Where both fail, the left’s failure is the caller’s, as one domain doing both would have failed.

inThreads

inThreads : (a : Type)
          -> (b : Type)
          -> (e : HFunctor)
          -> {{dm : Domain.domain <: e}}
          -> Handler (parallel a b <+> e)

Parallel handled by domains, into Co e: the rest of the world left as it is.

spread

spread : {e : HFunctor}
       -> {{dm : Domain.domain <: e}}
       -> {a : Type}
       -> Int
       -> (Int -> Co e a)
       -> Co e (List a)

c 0 to c (n - 1) at once, each on a domain (c 0 this one), in a scope of their own: their answers, in order. c is a computation of the world here: each domain runs it with the handlers between here and the program’s world, and holds what it is given shared. Where some fail, the first, in order, fails the caller, once all have ended. Fewer than one, none.