Skip to main content

core.runtime

Status legend. See stdlib status badge system.

The runtime module is the single place where the language meets the operating system. Everything with a sys.* call underneath — scheduling, futures, threads, timers, memory arenas, TLS, retry loops — lives here. The same module ships in five profiles (full, single_thread, no_async, no_heap, embedded); each profile swaps in a compatible implementation of the interfaces below. See runtime tiers → profiles for when to pick which profile.

Everything documented here matches the .vr sources in core/runtime/. Items marked (protocol) are typed interfaces that multiple profiles implement; items marked (record) are concrete types.

Submodule status overview​

The table below mirrors the per-submodule audit findings at core-tests/runtime/<sub>/audit.md. Click each row's audit link for the full open-defects list + deferred-action ranking.

ModuleStatusNotes
runtime.envpartial—
runtime.cbgrcomplete (interp)canonical re-export of the memory-safety surface
runtime.syncregression-onlyre-exports the synchronization APIs; mutex guard lifetime remains incomplete
runtime.syscallcomplete (interp)thin canonical re-export
runtime.timecomplete (interp)canonical re-export; qualified names bind correctly
runtime.tlscomplete (interp)live thread-local round-trips
runtime.textpartialone Unicode case-category pair classified wrongly
runtime.async_opspartialelapsed time measured across a sleep is unreliable
runtime.ctx_bridgepartialparallel writes to one context slot are not coherent
runtime.poolpartialsubmit and join run; retrieving a value through a handle is being filled in
runtime.threadpartialspawn and join run under the interpreter
runtime.configpartialtwo display paths pending
runtime.stack_allocregression-onlyallocators available; methods on a const-generic implement block do not resolve
runtime.recoverypartiala foreign Drop implementation on a scope guard is not run
runtime.spawnpartiala constructor chain can leak an unresolved stub
runtime.task_queuecomplete (interp)—
runtime.supervisorcomplete (interp)native borrowed root-supervisor access can fail; see below
runtime.modpartialaccessor receiver resolution through a renamed mount

Backend coverage must be validated separately. Successful interpreter checks do not establish native returned-reference or resource-lifetime correctness.

Known limitations: repeated root-supervisor access works under the interpreter. In native execution, lazy initialization produces the expected value once, but using the borrowed result through the accessor chain used by root_supervisor() can fail. Successful initialization alone does not establish safe access to the returned reference.

Mutex guard lifetime also remains incomplete: an interpreter check can report the mutex unlocked while the guard is still in scope. General native owned-resource destruction and lock-guard cleanup are not yet reliable. See mutex limitations and resource lifetime.

Module map​

SubmoduleContents
runtime.envExecutionEnv (θ+) — memory / capabilities / recovery / concurrency.
runtime.configRuntimeConfig protocol and profile-specific implementations.
runtime.supervisorSupervision tree — Supervisor, SupervisorHandle, ChildSpec, restart strategies.
runtime.recoveryRetry policies, circuit breakers, backoff and jitter.
runtime.poolThread-pool primitive (ThreadPool, TaskHandle).
runtime.threadOS threads (Thread, ThreadBuilder, JoinHandle<T>, stack traces).
runtime.timeMonotonic / wall clocks, sleep, Instant, Duration.
runtime.tlsThread-local storage primitive.
runtime.stack_allocStack-only allocator for no_heap.
runtime.syscallPlatform sys.* intrinsic imports.
runtime.syncSynchronisation wiring (re-exports from core.sync).
runtime.cbgrCBGR-runtime glue: generation / epoch trackers.
runtime.ctx_bridgeBridges between slot-based context access and the language's using [...] clause.
runtime.async_opsImplementation of await / select at the op-code level.
runtime.spawnLow-level spawn primitive (the language's spawn compiles to this).

Execution environment — runtime.env​

The centrepiece. ExecutionEnv (θ+) is a 2,560-byte structure holding the four pillars of execution state. Full layout, fork rules, and hot-path costs are documented in architecture → execution environment.

The user-facing API is deliberately small — most Verum code never touches runtime.env directly, because the language's &T, using [...], provide, defer, and spawn constructs read and write it implicitly.

/// Get the current task's environment (usually you don't need this).
public fn current_env() -> Maybe<&ExecutionEnv>;

/// Run a closure inside a freshly forked environment.
public fn with_forked_env<T, F: fn() -> T>(f: F) -> T;

/// CBGR safety tier (four variants, see architecture docs).
public type ExecutionTier is
    | Tier0_Full       // full CBGR: ≤ 15 ns design target; 1.2–1.7 ns (gen+epoch)
    | Tier1_Epoch      // gen + epoch: 1.2–1.7 ns
    | Tier2_Gen        // gen only: < Tier1_Epoch
    | Tier3_Unchecked; // no checks: 0 ns (unsafe)

Runtime configuration — runtime.config​

public type RuntimeConfig is protocol {
    type Allocator; type Executor; type IoDriver;
    fn init() -> Result<Self, RuntimeInitError>;
    fn shutdown(&mut self);
    fn allocator_ref(&self) -> &Self.Allocator;
    fn executor_handle(&self) -> &Self.Executor;
    fn io_driver_ref(&self) -> &Self.IoDriver;
};

The canonical implementation for the full profile is DefaultRuntimeConfig, which reads from the [runtime] section of verum.toml and falls back to sensible defaults (worker_threads = num_cpus, max_blocking_threads = 512, stack_size = 2 MiB, cbgr_tier = Tier0_Full).

Starting a runtime — Runtime​

core.async.executor.Runtime is the top-level handle returned by RuntimeBuilder. One is created in fn main() (implicitly by the language runtime) or explicitly by Runtime.new() in tests.

public type Runtime is { /* private */ };

implement Runtime {
    public fn builder() -> RuntimeBuilder;
    public fn new() -> Runtime;                        // default config
    public fn spawn<F: Future>(&self, f: F) -> JoinHandle<F.Output>;
    public fn block_on<F: Future>(&self, f: F) -> F.Output;
    public fn shutdown(self, timeout: Duration) -> Result<(), ShutdownError>;
}

/// Enter the async world from a synchronous function.
public fn block_on<F: Future>(future: F) -> F.Output;

RuntimeBuilder is the fluent configuration surface:

public type RuntimeBuilder is { /* private */ };

implement RuntimeBuilder {
    public fn new() -> Self;
    public fn worker_threads(self, n: Int) -> Self;
    public fn thread_stack_size(self, bytes: Int) -> Self;
    public fn enable_io(mut self) -> RuntimeBuilder;
    public fn enable_time(mut self) -> RuntimeBuilder;
    public fn thread_name(self, prefix: Text) -> Self;
    public fn max_blocking_threads(self, n: Int) -> Self;
    public fn build(self) -> AsyncRuntime;
}

Supervision — runtime.supervisor​

Erlang/OTP-style supervision over async tasks. A supervisor owns a set of children; each child has a ChildSpec that declares how the supervisor reacts when the child fails.

Key types​

public type SupervisorId is (UInt64);
public type ChildId      is (UInt64);

public type SupervisionStrategy is
    | OneForOne          // restart only the failing child
    | OneForAll          // restart every child on any failure
    | RestForOne;        // restart the failing child and its successors

// NOT `RestartStrategy` — that name belongs to a different type in
// `runtime.env`. The supervisor's is prefixed.
public type SupervisorRestartStrategy is
    | Permanent          // always restart
    | Transient          // restart on abnormal exit only
    | Temporary;         // never restart

public type FailureReason is
    | NormalExit
    | ErrorExit(Text)
    | Panic(Text)
    | Timeout
    | Cancelled
    | Manual             // operator-initiated restart
    | SupervisorShutdown;

public type ChildStatus is
    | Running | Starting | Restarting | Terminated | Failed | Stopped;

// A tracker, not a pair of settings: the counters are atomic and live
// in the type, so a supervisor reads the window without a lock.
public type RestartIntensity is {
    max_restarts:    UInt16,
    window_ms:       UInt64,
    restart_count:   AtomicU16,
    window_start_ms: AtomicU64,
    last_restart_ms: AtomicU64,
};

// No `start` factory, no `modules` list, no `ty`, no `significant` —
// a child is named and scheduled, and the work is handed to
// `SupervisorHandle.supervise` rather than stored in the spec.
public type ChildSpec is {
    name:                Text,
    restart:             SupervisorRestartStrategy,
    shutdown_timeout_ms: UInt32,
    max_restarts:        UInt16,
    restart_window_secs: UInt32,
    priority:            UInt8,        // higher starts earlier, stops later
};

public type ShutdownStrategy is
    | Graceful { timeout_ms: UInt32 }   // cancel, wait, then force
    | Brutal   { timeout_ms: UInt32 }   // force after a minimal timeout
    | Infinite;                         // wait forever

ChildSpec.new(name) gives Transient / 5000 ms / 10 restarts per 60 s / priority 100; ChildSpec.permanent(name) differs only in the restart strategy. ShutdownStrategy.graceful() is 5000 ms and ShutdownStrategy.brutal() is 100 ms.

Creating a supervisor​

// The window lives here as two plain numbers; `RestartIntensity` is the
// runtime tracker the supervisor builds from them. There is no
// `AutoShutdownStrategy`, and the name is a `Text`, not a `Maybe<Text>`.
public type SupervisorConfig is {
    strategy:                  SupervisionStrategy,
    max_restarts:              UInt16,
    restart_window_secs:       UInt32,
    escalation:                EscalationPolicy,
    shutdown:                  ShutdownStrategy,
    enable_circuit_breaker:    Bool,
    circuit_breaker_threshold: UInt16,
    name:                      Text,
};

implement SupervisorConfig {
    public fn one_for_one(name: Text) -> Self;      // and the other two
}

implement SupervisorHandle {
    public fn new(config: SupervisorConfig) -> Self;
    public fn root(config: SupervisorConfig) -> Self;
    public fn id(&self) -> SupervisorId;
    public fn name(&self) -> Text;
    public fn status(&self) -> SupervisorStatus;
    public fn set_parent(&self, parent: SupervisorHandle);

    public async fn supervise<F, T>(...) -> Result<ChildId, SupervisorError>;
    public async fn restart(&self, child_id: ChildId)
        -> Result<(), SupervisorError>;
    public async fn terminate(&self, child_id: ChildId)
        -> Result<(), SupervisorError>;
    public async fn shutdown(&self) -> Result<(), SupervisorError>;
}

public type SupervisorStatus is {
    id: SupervisorId, name: Text, strategy: SupervisionStrategy,
    child_count: Int, running_count: Int,
    total_restarts: UInt64, last_restart_ns: UInt64, is_running: Bool,
};

public type SupervisorError is
    | TooManyRestarts { count: Int, window_secs: UInt32 }
    | ChildNotFound(ChildId)
    | ShuttingDown
    | SpawnFailed(Text)
    | ChannelClosed
    | InvalidSpec(Text)
    | NoParentSupervisor
    | Other(Text);

shutdown() takes no argument — the strategy comes from the config the supervisor was built with. There is no start, start_child, which_children or count_children: a supervisor is constructed with new/root, work is attached with supervise, and the census is status().

Built-in shortcuts​

public fn root_supervisor() -> &SupervisorHandle;

public async fn spawn_supervised<F, T>(future: F) -> Result<ChildId, SupervisorError>
    where F: Future<Output = T> + Send + 'static, T: Send + 'static;

public async fn spawn_permanent<F, T>(future: F, name: Text) -> Result<ChildId, SupervisorError>;
public async fn spawn_temporary<F, T>(future: F, name: Text) -> Result<ChildId, SupervisorError>;

Escalation​

When a supervisor exceeds RestartIntensity, it escalates to its parent supervisor according to EscalationPolicy:

public type EscalationPolicy is
    | RestartSubtree         // restart every child of this supervisor
    | EscalateToParent       // the @default arm
    | Terminate              // stop the whole tree
    | LogAndIgnore;          // for non-critical children

public type EscalationReason is
    | RestartLimitExceeded {
          child_id: ChildId, child_name: Text,
          max_restarts: UInt16, window_secs: UInt32,
          last_failure: FailureReason,
      }
    | SubSupervisorEscalation {
          supervisor_id: SupervisorId, reason: Heap<EscalationReason>,
      }
    | InternalFault { error: Text }
    | AllStrategiesExhausted;

There is no CustomHandler arm and no EscalationAction type — the policy is a closed set of four, and EscalationReason.description() renders any of them for a log line. SubSupervisorEscalation nests through Heap<EscalationReason>, which is how a deep tree reports the original cause upward.

Recovery — runtime.recovery​

Retry loops, circuit breakers, backoff and jitter. Available on every profile (including no_async — the synchronous form uses the same types).

Retry​

Every name in this module carries a Recovery prefix — BackoffStrategy and RetryPolicy unprefixed are not declared. Delays are milliseconds, not Duration, and there is no Fibonacci arm.

public type RecoveryBackoffStrategy is
    | Fixed       { delay_ms: UInt64 }
    | Linear      { base_ms: UInt64, increment_ms: UInt64, max_ms: UInt64 }
    | Exponential { base_ms: UInt64, max_ms: UInt64, multiplier: Int }
    | None;                                       // immediate retry

implement RecoveryBackoffStrategy {
    fn calculate_delay_ms(&self, attempt: Int) -> UInt64;
    fn exponential(base_ms: UInt64, max_ms: UInt64) -> Self;   // multiplier 2
}

// A sum type, not a function type.
public type RetryPredicate is
    | AllErrors
    | TransientOnly                    // timeouts, connection reset
    | Custom(fn(&Text) -> Bool);

public type JitterConfig is
    | None
    | Proportional(UInt8)              // percentage 0-100 of the delay
    | Fixed(UInt64)                    // plus or minus this many ms
    | Full;                            // 0 .. delay

implement JitterConfig {
    fn apply(&self, delay_ms: UInt64) -> UInt64;
}

// The config and the policy are two types: the policy carries the
// running state.
public type RuntimeRetryConfig is {
    max_attempts: Int,
    backoff:      RecoveryBackoffStrategy,
    jitter:       JitterConfig,
    retry_on:     RetryPredicate,
};

public type RecoveryRetryPolicy is {
    config:          RuntimeRetryConfig,
    current_attempt: Int,               // 1-indexed
    total_retries:   Int,
    last_error:      Maybe<Text>,
};

Circuit breaker​

// Three bare variants — the deadline and the trial count are state on
// the breaker, not payload on the state.
public type RecoveryCircuitState is
    | Closed                 // normal
    | Open                   // rejecting
    | HalfOpen;              // testing recovery

public type RecoveryCircuitBreakerConfig is {
    failure_threshold:  UInt16,
    required_successes: UInt16,
    timeout_ms:         UInt32,        // Open -> HalfOpen after this
    error_predicate:    ErrorPredicate,
};

public type RecoveryCircuitBreaker is { /* atomic state */ };
public type CircuitBreakerStats is { /* counters */ };
public type CircuitBreakerError<E> is
    | Open                     // the breaker rejected the call; no inner error
    | Failed(E);               // the call ran and failed, carrying E

The inline variants​

InlineCircuitBreaker and InlineRetryPolicy are stored by value to avoid a heap allocation on the hot path; RecoveryCircuitBreaker and RecoveryRetryPolicy above are for long-lived state shared across tasks. RuntimeRecoveryStrategy selects between them.

Threads — runtime.thread​

OS-level threads. Available only on profiles that have threading (full, no_async). Suspended on single_thread, no_heap, embedded.

public type ThreadId is { /* opaque */ };
public type Thread   is ();

// `ThreadJoinHandle`, not `JoinHandle` — the bare name is not declared
// here.
public type ThreadJoinHandle<T> is { /* opaque */ };

public type ThreadBuilder is { /* fluent */ };

implement ThreadBuilder {
    public fn new() -> ThreadBuilder;
    public fn name(self, name: Text) -> ThreadBuilder;
    public fn stack_size(self, size: Int) -> ThreadBuilder;
    public fn spawn<T: Send>(self, f: fn() -> T)
        -> Result<ThreadJoinHandle<T>, ThreadError>;
}

implement Thread {
    public fn spawn<T: Send>(f: fn() -> T) -> ThreadJoinHandle<T>;
    public fn builder() -> ThreadBuilder;
    public fn current_id() -> ThreadId;
    public fn yield_now();
    public fn sleep(duration: Duration);
    public fn sleep_ms(ms: Int);
    public fn available_parallelism() -> Int;
    public fn park();
    public fn unpark(thread_id: ThreadId);
}

// Four variants. There is no StackTooSmall, OutOfMemory, NameTooLong or
// ProfileUnsupported, and SpawnFailed carries no payload.
public type ThreadError is
    | SpawnFailed | JoinFailed | Panicked | InvalidName;

// `ThreadStackFrame`, and every resolvable field is a `Maybe` because
// symbolication is deferred and may fail.
public type ThreadStackFrame is {
    ip:     UInt64,
    symbol: Maybe<Text>,
    file:   Maybe<Text>,
    line:   Maybe<Int>,
    column: Maybe<Int>,
};

public type StackTrace is { frames: List<ThreadStackFrame> };

StackTrace records no thread id — StackTrace.capture() is written to walk the calling thread's own frames, up to 64 of them.

caution
capture() does not walk anything yet

Checked. The walk starts from @frame_address(0), and type inference has no arm for that name, so it types as Unit — the frame pointer the loop tests and advances is not a pointer.

The evidence is in the shipped bytecode rather than in a compiler run, because a single-file verum check over core/ and the stdlib bake do not agree and the bake is what ships:

strings runtime.vbca | grep -c capture         38
strings runtime.vbca | grep -c frame_address    0

The function is there. The intrinsic its walk depends on is not, under any name, anywhere in the archive.

The gap is the same shape as the cubical @builtin_* family described on verification/cubical-hott — a name the compiler parses and does not type. It differs in one way worth knowing: there the failure is silent, here it is a visible E400 that does not mention @frame_address, so a reader sees found 'Unit' and has nowhere to look for where the Unit came from.

Nothing about StackTrace's own shape is affected: the record, its fields and ThreadStackFrame are all real.

This box stops being true when frame_address appears in the archive alongside capture.

Thread pool — runtime.pool​

A fixed-size thread pool for CPU-bound tasks that do not need the full async scheduler. The task shape is deliberately minimal — fn(Int) -> Int — matching the native verum_pool_* runtime ABI; richer task shapes ride the async executor instead.

public type ThreadPool is { handle: Int };
public type PoolTaskHandle is { handle: Int, awaited: Bool };

implement ThreadPool {
    /// num_workers <= 0 defaults to 4.
    public fn new(num_workers: Int) -> ThreadPool;
    public fn submit(&self, func: fn(Int) -> Int, arg: Int) -> PoolTaskHandle;
    /// Static: submit to the lazily-initialized global pool.
    public fn global_submit(func: fn(Int) -> Int, arg: Int) -> PoolTaskHandle;
    /// RAII: Drop releases the pool; explicit destroy for early release.
    public fn destroy(&self);
}

implement PoolTaskHandle {
    /// Block until the task completes and return its result.
    /// Use `join` for this synchronous handle; `.await` is async-expression syntax.
    /// Drop drains an un-joined handle.
    public fn join(&mut self) -> Int;
}

Tier semantics. Tier-1 (AOT) runs tasks on real native worker threads (verum_pool_*). Tier-0 (interpreter) executes each task EAGERLY at the submit point on the interpreter thread and parks the result in a slot-recycling handle table — observable join() results are identical for any result-observing program; only the interleaving differs, which the language does not promise. See core-tests/runtime/pool/ for the execution and result-observation controls.

Time — runtime.time​

runtime.time is a THIN RE-EXPORT of the canonical, wired declarations in core.intrinsics.runtime.time — one source of truth for both tiers (RUNTIME-DUPLICATE-TREE-1 discipline). Instant / Duration and the calendar surface live in core.time, not here.

public mount core.intrinsics.runtime.time.{
    monotonic_nanos,   // fn() -> Int — monotone, both tiers
    realtime_secs,     // fn() -> Int — Unix seconds
    realtime_nanos,    // fn() -> Int — Unix nanoseconds
    num_cpus,          // fn() -> Int — logical CPU count
    sleep_ms,          // fn(Int)
    sleep_ns,          // fn(Int)
};

Consumer mounts preserve the qualified target of each re-export. core-tests/runtime/time/ checks monotonic_nanos and num_cpus through this shim so they reach their intended runtime implementations.

Thread-local storage — runtime.tls​

runtime.tls is a thin re-export of core.intrinsics.runtime.tls — the raw slot API over a DEDICATED user_tls_slots store (opcodes 0x59-0x5D; the context system populates separate high slots and cannot collide).

public mount core.intrinsics.runtime.tls.{
    tls_get_base,      // fn() -> *mut Byte
    tls_slot_get,      // fn(UInt8) -> *const Byte
    tls_slot_set,      // fn(UInt8, *const Byte)
    tls_slot_clear,    // fn(UInt8)
    tls_slot_has,      // fn(UInt8) -> Bool
    tls_frame_push,    // fn() -> *const Byte   — balanced pair:
    tls_frame_pop,     // fn()                  — pops the TOP frame
    tls_read_ptr, tls_write_ptr,      // <T> raw offset access
    tls_read_i32, tls_write_i32,
    tls_read_usize, tls_write_usize,
};

Note the frame discipline: tls_frame_pop() takes NO argument — it is a balanced-stack pop, not a token-addressed restore.

Stack / arena / pool allocators — runtime.stack_alloc​

Deterministic-latency allocators over fixed [Byte; SIZE] buffers. PRIMARY use is the no_heap / embedded profiles (EmbeddedRuntime's allocator). The module is not cfg-gated; its self-contained implementations are also available on the full runtime (request arenas, connection pools). The real API surface:

public type StackAllocator<const SIZE: Int> is { /* buffer + bump top + watermark */ };
public type StackSavepoint is { top: Int, alloc_count: Int };
public type ArenaAllocator<const CHUNK_SIZE: Int, const MAX_CHUNKS: Int> is { /* chunked */ };
public type PoolAllocator<const BLOCK_SIZE: Int, const BLOCK_COUNT: Int> is { /* freelist */ };
// Presets: TinyStackAllocator (1 KiB) / Small (4) / Medium (16) / Large (64)

implement<const SIZE: Int> StackAllocator<SIZE> {
    public fn new() -> Self;
    public fn alloc(&mut self, layout: Layout) -> Result<*mut Byte, AllocError>;
    public fn dealloc(&mut self, ptr: *mut Byte, layout: Layout);   // LIFO only
    public fn save(&self) -> StackSavepoint;
    public fn restore(&mut self, savepoint: StackSavepoint);
    public fn capacity(&self) -> Int;
    public fn used(&self) -> Int;
    public fn remaining(&self) -> Int;
    public fn watermark(&self) -> Int;
    public fn alloc_count(&self) -> Int;
    public fn reset(&mut self);       // keeps the lifetime watermark
    public fn reset_all(&mut self);   // clears the watermark too
}

Known gap: methods of implement<const N> blocks are currently unresolvable on archive-loaded types (CONST-GENERIC-IMPL-METHODS-1) — the conformance suites are written and pinned on that task.

public type Arena is { /* stack-backed */ };

implement Arena {
    public fn new(buffer: &mut [Byte]) -> Self;
    public fn allocate(&mut self, layout: Layout) -> Result<&mut [Byte], AllocError>;
    public fn reset(&mut self);
    public fn bytes_used(&self) -> Int;
}

A no_heap-profile program that tries to call Heap.new(v) is a compile error, not a runtime failure.

Process / session — core.concurrency​

Two small modules outside runtime proper but closely related:

  • core.concurrency.process — child-process spawn (Command, Child, ExitStatus, stdin/stdout/stderr pipes).
  • core.concurrency.session — terminal session utilities (PTY allocation, signal propagation, job control).

These are documented under stdlib → concurrency.

See also​