ThreadId

def Control.Concurrent.PosNat : Type

A positive natural number. Used for ThreadId.id to encode at the type level that thread IDs are always $\ge 1$.

$$\text{PosNat} := \{n : \mathbb{N} \mid n > 0\}$$

Equations

• Control.Concurrent.PosNat = { n : Nat // n > 0 }

instance Control.Concurrent.instNonemptyPosNat : Nonempty PosNat

@[implicit_reducible]

instance Control.Concurrent.instBEqPosNat : BEq PosNat

Equations

• Control.Concurrent.instBEqPosNat = { beq := fun (a b : Control.Concurrent.PosNat) => a.val == b.val }

@[implicit_reducible]

instance Control.Concurrent.instHashablePosNat : Hashable PosNat

Equations

• Control.Concurrent.instHashablePosNat = { hash := fun (p : Control.Concurrent.PosNat) => hash p.val }

@[implicit_reducible]

instance Control.Concurrent.instToStringPosNat : ToString PosNat

Equations

• Control.Concurrent.instToStringPosNat = { toString := fun (p : Control.Concurrent.PosNat) => toString p.val }

@[implicit_reducible]

instance Control.Concurrent.instReprPosNat : Repr PosNat

Equations

• Control.Concurrent.instReprPosNat = { reprPrec := fun (p : Control.Concurrent.PosNat) (n : Nat) => reprPrec p.val n }

structure Control.Concurrent.ThreadId : Type

A handle to a forked concurrent thread.

• id : PosNat — unique identifier, $\ge 1$ by construction (monotonic counter).
• task — the underlying Task so we can IO.wait on it.
• cancelToken — cooperative cancellation via Std.CancellationToken.

The id field is never reused within a process (monotonic counter).

• id : PosNat
• task : Task (Except IO.Error Unit)
• cancelToken : Std.CancellationToken

@[implicit_reducible]

instance Control.Concurrent.instBEqThreadId : BEq ThreadId

Equations

• Control.Concurrent.instBEqThreadId = { beq := fun (a b : Control.Concurrent.ThreadId) => a.id == b.id }

@[implicit_reducible]

instance Control.Concurrent.instHashableThreadId : Hashable ThreadId

Equations

• Control.Concurrent.instHashableThreadId = { hash := fun (t : Control.Concurrent.ThreadId) => hash t.id }

@[implicit_reducible]

instance Control.Concurrent.instToStringThreadId : ToString ThreadId

Equations

• Control.Concurrent.instToStringThreadId = { toString := fun (t : Control.Concurrent.ThreadId) => toString "ThreadId(" ++ toString t.id ++ toString ")" }

@[implicit_reducible]

instance Control.Concurrent.instReprThreadId : Repr ThreadId

Equations

• Control.Concurrent.instReprThreadId = { reprPrec := fun (t : Control.Concurrent.ThreadId) (x : Nat) => Std.Format.text (toString "ThreadId(" ++ toString t.id ++ toString ")") }

Forking

def Control.Concurrent.forkIO (action : IO Unit) : IO ThreadId

Fork a new green thread. The action is submitted to Lean's thread pool via IO.asTask (default priority) — O(1), no dedicated OS thread spawned. Millions of green threads can be active simultaneously.

$$\text{forkIO} : \text{IO}\ \text{Unit} \to \text{IO}\ \text{ThreadId}$$

let tid ← forkIO do
  IO.println "hello from green thread"

The returned ThreadId can be used with killThread for cooperative cancellation, or with waitThread to join.

Equations

• One or more equations did not get rendered due to their size.

def Control.Concurrent.forkFinally {α : Type} (action : IO α) (finally_ : Except IO.Error α → IO Unit) : IO ThreadId

Fork a green thread that calls finally with the outcome, whether the action succeeded or threw.

$$\text{forkFinally} : \text{IO}\ \alpha \to (\text{Except}\ \text{IO.Error}\ \alpha \to \text{IO}\ \text{Unit}) \to \text{IO}\ \text{ThreadId}$$

Modelled after Haskell's forkFinally.

Equations

• One or more equations did not get rendered due to their size.

Thread control

def Control.Concurrent.killThread (tid : ThreadId) : BaseIO Unit

Cooperatively cancel a thread. Sets the thread's CancellationToken.

$$\text{killThread} : \text{ThreadId} \to \text{BaseIO}\ \text{Unit}$$

Note: Unlike GHC's killThread, this is cooperative. The target thread must check Std.CancellationToken.isCancelled or use cancellation-aware primitives to actually stop.

Equations

• Control.Concurrent.killThread tid = (Control.Concurrent.ThreadId.cancelToken✝ tid).cancel

def Control.Concurrent.threadDelay (μs : Nat) : BaseIO Unit

Suspend the current thread for at least $\mu s$ microseconds.

$$\text{threadDelay} : \mathbb{N} \to \text{BaseIO}\ \text{Unit}$$

Maps to IO.sleep (millisecond granularity, so we round up: $\text{ms} = \lceil \mu s / 1000 \rceil$).

Equations

• Control.Concurrent.threadDelay μs = IO.sleep ((μs + 999) / 1000).toUInt32

def Control.Concurrent.yield : BaseIO Unit

Yield execution to other threads. Equivalent to IO.sleep 0.

$$\text{yield} : \text{BaseIO}\ \text{Unit}$$

Equations

• Control.Concurrent.yield = IO.sleep 0

Fair green threads

def Control.Concurrent.forkGreen (action : Green.Green Unit) : IO ThreadId

Fork a fair green thread. The Green computation never blocks pool threads when awaiting — suspensions use BaseIO.bindTask to register continuations, freeing the pool thread for other work.

$$\text{forkGreen} : \text{Green}\ \text{Unit} \to \text{IO}\ \text{ThreadId}$$

Use Green.await, Green.takeMVar, etc. inside the action to suspend without blocking.

See Hale.Control.Concurrent.Green for termination, liveness, and fairness guarantees.

Equations

• One or more equations did not get rendered due to their size.

def Control.Concurrent.waitThreadGreen (tid : ThreadId) : Green.Green Unit

Await a thread's completion inside a Green computation, without blocking the pool thread.

$$\text{waitThreadGreen} : \text{ThreadId} \to \text{Green.Green}\ \text{Unit}$$

Equations

• One or more equations did not get rendered due to their size.

Waiting

def Control.Concurrent.waitThread (tid : ThreadId) : IO Unit

Wait for a thread to finish and return its result. Re-throws if the thread threw an exception.

$$\text{waitThread} : \text{ThreadId} \to \text{IO}\ \text{Unit}$$

Equations

• One or more equations did not get rendered due to their size.