Skip to content

stdlib.thread

Threading

Generated from v0.65.7. 5 source files, 67 documented symbols.

local.xi

type ThreadLocal

ThreadLocal[T] - storage holding one value of T per thread.

Field Type
init fn() -> T
value T
initialized Bool
fn thread_local_new[T](init: fn() -> T) -> ThreadLocal[T]

Create thread-local storage with a lazy initializer. Params: init - the initializer invoked on first access. Returns: uninitialised thread-local storage. Complexity: O(1).

  • Postcondition: result.initialized == false
fn tls_get[T](tl: &mut ThreadLocal[T]) -> T

Read the calling thread's value, initializing on first access. Params: tl - the thread-local (mutated on first access). Returns: the current value, running init if not yet set. Complexity: O(1).

  • Postcondition: tl.initialized == true
fn tls_set[T](tl: &mut ThreadLocal[T], value: T)

Write the calling thread's value. Params: tl - the thread-local; value - the new value. Complexity: O(1).

  • Postcondition: tl.initialized == true
fn tls_replace[T](tl: &mut ThreadLocal[T], value: T) -> T

Replace and return the previous value. Params: tl - the thread-local; value - the replacement. Returns: the previous value (or the initializer's value if unset). Complexity: O(1).

  • Postcondition: tl.initialized == true
fn tls_take[T](tl: &mut ThreadLocal[T]) -> Option[T]

Take the value, leaving the slot empty. Params: tl - the thread-local (cleared). Returns: Some(value) if set, None if uninitialized. Complexity: O(1).

  • Postcondition: tl.initialized == false
fn tls_clear[T](tl: &mut ThreadLocal[T])

Drop the calling thread's value and reset to uninitialized. Params: tl - the thread-local. Complexity: O(1).

  • Postcondition: tl.initialized == false
fn thread_local_key_new() -> Int

Allocate a raw TLS key. Returns: a fresh positive key value. Complexity: O(1).

  • Postcondition: result > 0
fn tls_key_get(key: Int) -> Int

Read the calling thread's value for a raw key. Params: key - the key to look up. Returns: the stored value, or 0 if the key is not the stored one. Complexity: O(1). Single-slot simulation: one raw key per program.

  • Postcondition: _raw_key != key => result == 0
fn tls_key_set(key: Int, value: Int)

Write the calling thread's value for a raw key. Params: key - the key; value - the value to store. Complexity: O(1). Single-slot simulation: one raw key per program.

  • Postcondition: _raw_key == key
  • Postcondition: _raw_value == value



park.xi

type ParkToken

ParkToken - a standalone one-shot park/unpark pair not tied to a thread.

Field Type
flag *Int
fn park_token_new() -> ParkToken

Create a new park token. Returns: a token with no pending notification. Complexity: O(1).

  • Postcondition: ptr.is_null(result.flag) == false
fn park_token_wait(tok: ParkToken)

Block until the token is notified. Params: tok - the token. Complexity: O(1) per poll; blocks until a notify.

  • Precondition: ptr.is_null(tok.flag) == false
fn park_token_notify(tok: ParkToken)

Release one waiter on the token. Params: tok - the token. Complexity: O(1).

  • Precondition: true
fn park()

Block the calling thread until it is unparked. Complexity: O(1) per poll; blocks until an unpark.

  • Postcondition: ptr.is_null(_park_flag) == false
fn park_timeout(ms: Int) -> Bool

Block up to ms milliseconds; true if unparked first. Params: ms - the timeout in milliseconds (clamped to >= 0). Returns: true if unparked before the timeout, false on timeout. Complexity: O(ms) polls, each sleeping up to 1 ms.

  • Postcondition: ptr.is_null(_park_flag) == false
fn unpark(t: SpawnThread)

Make the target thread eligible to resume. Params: t - the target thread. Complexity: O(1).

  • Postcondition: ptr.is_null(_park_flag) == false
fn unpark_all(threads: &Vec[SpawnThread])

Unpark every thread in the vector. Params: threads - the threads to wake. Complexity: O(n) where n is the number of threads.

  • Postcondition: ptr.is_null(_park_flag) == false



pool.xi

type PoolJob

Legacy per-job record (kept for source compatibility; the persistent fleet no longer stores per-job handles).

Field Type
handle *UInt8
buf *UInt8
type ThreadPool

Fixed-size persistent worker pool.

Field Type
workers Int
idle Int
busy Int
queued Vec[Int]
next_id Int
completed Int
closed Bool
running Vec[PoolJob]
handle *UInt8
fn thread_pool_new(workers: Int) -> ThreadPool

Create a pool with workers persistent workers. Params: workers - fixed number of workers (clamped to >= 1). Returns: a new pool with all workers idle and no pending jobs. Complexity: O(workers) OS thread creation.

  • Postcondition: result.workers >= 1
  • Postcondition: result.idle == result.workers
  • Postcondition: result.closed == false
fn tp_submit(p: &mut ThreadPool, job: fn() -> Unit) -> Bool

Enqueue a job; false if the pool is shutting down. Params: p - the pool; job - a named/top-level closure (runs on a persistent worker; capturing closures are not representable as bare code pointers -- see the module contract). Returns: true on acceptance, false if the pool is shut down. Complexity: O(1) amortized (blocks while the queue is full).

  • Postcondition: result == true => p.queued.len() >= 1
  • Postcondition: p.busy + p.idle == p.workers
fn tp_submit_with(p: &mut ThreadPool, job: fn(Int) -> Unit, arg: Int) -> Bool

Enqueue a job with one argument; false if the pool is shutting down. Params: p - the pool; job - the closure; arg - its single argument. Runs on a persistent worker with arg (no longer inline). Returns: true on acceptance, false if the pool is shut down. Complexity: O(1) amortized (blocks while the queue is full).

  • Postcondition: (p.closed == true) => (result == false)
  • Postcondition: (p.closed == false) => (result == true)
fn tp_join(p: &mut ThreadPool)

Block until all queued and running jobs complete. Params: p - the pool. REAL drain: waits for the runtime's outstanding counter to reach zero, then returns the assignment counters to busy == 0, idle == workers. Complexity: O(1) wait plus the workers' runtime.

  • Postcondition: p.queued.len() == 0
  • Postcondition: p.busy == 0
  • Postcondition: p.idle == p.workers
fn tp_shutdown(p: &mut ThreadPool)

Stop accepting jobs, drain the queue, and reap the workers. Params: p - the pool. Closes the pool (submit returns false afterwards), waits for completion, wakes every worker and joins the OS threads. Complexity: O(n) where n is the pending work.

  • Postcondition: p.closed == true
  • Postcondition: p.queued.len() == 0
fn tp_destroy(p: &mut ThreadPool)

Shut the pool down and free its runtime resources. Params: p - the pool (consumed). Do not call while another thread may still submit. Complexity: O(n) where n is the pending work.

  • Postcondition: p.closed == true
  • Postcondition: p.busy == 0
  • Postcondition: p.idle == p.workers
fn tp_size(p: &ThreadPool) -> Int

The number of persistent workers. Params: p - the pool. Returns: the fixed worker count. Complexity: O(1).

  • Postcondition: result >= 0
fn tp_idle(p: &ThreadPool) -> Int

The number of currently idle workers. Params: p - the pool. Returns: workers not currently assigned a job. Complexity: O(1).

  • Postcondition: result >= 0
fn tp_busy(p: &ThreadPool) -> Int

The number of currently assigned workers. Params: p - the pool. Returns: workers currently assigned a job (does not include queued work). Complexity: O(1).

  • Postcondition: result >= 0
fn tp_active(p: &ThreadPool) -> Int

The real number of queued + running jobs. Params: p - the pool. Returns: the runtime outstanding count (0 in degraded mode). Complexity: O(1) plus one lock.

  • Postcondition: result >= 0
fn tp_completed(p: &ThreadPool) -> Int

The real number of jobs completed by the workers. Params: p - the pool. Returns: the runtime completed counter (0 in degraded mode). Complexity: O(1) plus one lock.

  • Postcondition: result >= 0



spawn.xi

type SpawnThread

SpawnThread (the stub's Thread) - a handle to a spawned thread.

Field Type
id Int
handle *UInt8
buf *UInt8
fn spawn(f: fn() -> Unit) -> SpawnThread

Start a new thread running f (REAL since wave 145). Params: f - the function to run. Returns: a handle to the thread; join waits for it, detach releases it. Complexity: O(1) plus the cost of f on the worker.

  • Postcondition: result.id > 0
fn spawn_with(f: fn(Int) -> Unit, arg: Int) -> SpawnThread

Start a new thread running f(arg). Params: f - a named/top-level fn(Int) (capturing closures are not bare code pointers); arg - its single argument. Returns: a real OS-thread handle; join waits and frees the buffer. The arg travels in the runtime payload (REL-20261010-1834-engine-6: the arg channel now exists; spawn_with is no longer inline). Complexity: O(1) plus the cost of f on the worker.

  • Postcondition: result.id > 0
fn join(t: SpawnThread) -> Result[Int, Str]

Block until the thread exits; returns Ok(0). REAL since wave 145: waits on the OS thread, then frees the result buffer. Inline handles (no OS thread) join as a no-op Ok. Params: t - the thread handle (consumed). Complexity: O(1) syscall plus the worker's runtime.

  • Postcondition: true
fn detach(t: SpawnThread)

Let the thread run independently and free its OS handle. REAL since wave 145: the runtime releases the handle on exit; the 16-byte result buffer is retained for the process lifetime (documented). Inline handles are a no-op. Params: t - the thread handle (consumed). Complexity: O(1).

  • Precondition: t.id > 0
fn sleep_ms(ms: Int)

Suspend the calling thread for ms milliseconds. Params: ms - the sleep duration (clamped to >= 0). Complexity: O(1) syscall.

fn yield_now()

Voluntarily give up the CPU timeslice. Complexity: O(1) syscall.

  • Precondition: true
fn thread_id() -> Int

The id of the calling thread. Returns: the OS thread id of the current thread. Complexity: O(1).

  • Precondition: true
fn thread_count() -> Int

The number of running threads (hardware parallelism). Returns: the available hardware thread count (>= 1). Complexity: O(1).

  • Postcondition: result >= 1
fn is_main_thread() -> Bool

True if the calling thread is the main thread. Returns: whether the current thread id matches the first-seen id. Complexity: O(1).

fn spawn_scoped(f: fn() -> Unit) -> Result[Int, Str]

Spawn a thread scoped to the current stack frame (real spawn + join). Params: f - the function to run. Returns: Ok(0) after the thread has run and been joined. Complexity: O(1) plus the cost of f on the worker.

  • Postcondition: true



thread.xi

type Thread

OS thread handle plus its identifier.

Field Type
handle *UInt8
id Int

type JoinHandle

Handle to a spawned thread and its result slot.

Field Type
thread Thread
result_buf *UInt8

fn spawn[T](f: fn() -> T) -> JoinHandle[T]

Spawn a thread running f; join it to get the result.

  • Precondition: true
  • Postcondition: result.thread.handle != 0

fn spawn_with_name[T](name: Str, f: fn() -> T) -> JoinHandle[T]

Spawn a named thread (the name is advisory on some platforms).

  • Postcondition: result.thread.handle != 0

fn join[T](self: Self) -> Result[T, Str]

Wait for the thread and return its result, or Err with the message.

  • Precondition: self.thread.handle != 0
  • Postcondition: true

fn is_finished[T](self: Self) -> Bool

True when the thread has already terminated.

  • Precondition: self.result_buf != 0

fn thread[T](self: Self) -> Thread

The underlying thread handle (a copy; joining is not affected).

  • Postcondition: result.handle == self.thread.handle

fn detach[T](self: Self)

Detach the handle; the thread's result is discarded.

  • Precondition: self.thread.handle != 0
  • Precondition: self.result_buf != 0

fn current() -> Thread

Handle for the calling thread.

  • Precondition: true

fn id(self: Self) -> Int

Numeric thread id.

  • Postcondition: result == self.id

fn name(self: Self) -> Option[Str]

Thread name when one was set at spawn, else None.

  • Postcondition: result.is_none == true

fn sleep_ms(ms: Int)

Sleep for ms milliseconds; ms must be non-negative.

  • Precondition: ms >= 0

fn sleep(ms: Int)

Alias of sleep_ms (sleeps ms milliseconds); ms must be non-negative.

  • Precondition: ms >= 0

fn yield_now()

Give up the remainder of the current time slice.

  • Precondition: true

type Scope

Scoped threads (borrows from parent scope)

Field Type

fn scope[T](f: fn(&Scope) -> T) -> T

Run f with a scope that joins every thread spawned through it.

fn spawn[T](self: Self, f: fn() -> T) -> JoinHandle[T]

Spawn a thread joined when the enclosing scope exits.

  • Postcondition: result.thread.handle != 0

fn available_parallelism() -> Int

Number of usable CPUs (at least 1).

  • Precondition: true
  • Postcondition: result >= 1

fn hardware_threads() -> Int

Alias of available_parallelism.

  • Postcondition: result >= 1

fn current_thread_id() -> Int

Numeric id of the calling thread.

  • Precondition: true

fn thread_count() -> Int

Returns the number of available hardware threads. Delegates to available_parallelism(). Complexity: O(1). Thread-safe.

  • Postcondition: result >= 1

fn thread_sleep_us(us: Int)

Sleeps for us microseconds, rounding down to the nearest millisecond. Complexity: O(1) syscall. Thread-safe.

  • Precondition: us >= 0

fn thread_yield()

Yields the current thread's time slice. Alias for yield_now. Complexity: O(1) syscall. Thread-safe.

fn thread_parallel_for(start: Int, end: Int, f: fn(Int) -> Unit)

Executes f(i) for each i in [start, end). NOTE: This is a SEQUENTIAL implementation. True parallel execution requires spawning threads, which is not yet supported by this helper. Complexity: O(end - start) sequential invocations.

fn thread_name_current() -> Option[Str]

Returns the name of the current thread, or None if unnamed. Delegates to Thread.current().name. Complexity: O(1). Thread-safe.

  • Postcondition: result.is_none == true