Skip to main content

Concurrency Spec (v0.1)

Status: normative for core/task::* ABI shape and deterministic replay behavior.

Goals

  • Keep kernel purity unchanged (no threads in kernel semantics).
  • Express concurrency only as capability effects.
  • Preserve deterministic replay and auditability.

Operation Surface

  • core/task::spawn
  • core/task::await
  • core/task::cancel
  • core/task::status
  • core/task::scope

All operations are deny-by-default under capability policy.

Payload and Result Schemas

Canonical task data contracts: - Task handle:

{:task-id <symbol|str>}
  • Successful task completion:
{:task-id <symbol|str> :state :done :result <term> :error nil}
  • Failed task completion:
{:task-id <symbol|str> :state :failed :result nil :error <term>}
  • Cancelled task:
{:task-id <symbol|str> :state :cancelled :result nil :error nil}

core/task::spawn

Request payload:

{:scope <str|symbol|nil> :label <str|symbol|nil> :payload <term>}

Optional executable payload forms inside :payload:

{:task/eval <coreform-expr-term>}
{:task/eval <coreform-expr-term> :task/arg <term>}
{:task/eval <coreform-expr-term> :task/args [<term> ...]}

Semantics: - The runner evaluates :task/eval in a fresh prelude environment. - If :task/arg/:task/args are present, the evaluated value must be callable and is applied left-to-right. - If evaluation yields an effect program, it is executed under the same capability policy as the parent run. - Final non-datum results are rejected as core/task/program-error.

Result payload:

{:task-id <symbol|str> :state :running|:done|:failed|:cancelled}

core/task::await

Request payload:

{:task-id <symbol|str>}

Result payload:

{:task-id <symbol|str> :state :done|:failed|:cancelled :result <term|nil> :error <term|nil>}

core/task::cancel

Request payload:

{:task-id <symbol|str>}

Result payload:

{:task-id <symbol|str> :state :cancelled|:done|:failed}

core/task::status

Request payload:

{:task-id <symbol|str>}

Result payload:

{:task-id <symbol|str> :state :running|:done|:failed|:cancelled}

core/task::scope

Request payload:

{:scope <str|symbol|nil>}

Result payload:

{:scope <str|symbol|nil> :state :entered}

Determinism Rules

  • Task identifiers must be deterministic within a run (monotonic logical IDs are recommended).
  • Runner-visible schedule decisions must be recorded in effect logs.
  • Replay must fail on:
    • missing/extra task events
    • task-id mismatch
    • state transition mismatch
    • response hash mismatch

Replay Contract

  • spawn/await/cancel/status/scope responses are replayed from log, never recomputed from wall-clock scheduling.
  • Any host runtime that cannot satisfy deterministic replay for these ops must return sealed core/caps/backend-unavailable with actionable configuration guidance.

Policy Hooks

Capability policy should support: - max_tasks - max_workers - max_queue - per-op timeout and cancellation controls

Task worker defaults: - task.default_workers defaults to host parallelism (available_parallelism, minimum 1) when unspecified. - explicit task.default_workers remains authoritative when set.

Absent non-task policy entries default to deny.

Production SLO Contract

Throughput/latency SLO enforcement for task scheduler and GPU/compute bridge paths is defined in: - docs/spec/CONCURRENCY_GPU_SLO_v0.1.md.

Stress Evidence Lifecycle

  • Read-only stress check: scripts/check_task_concurrency_stress.sh
  • Explicit report/history producer: scripts/update_task_concurrency_stress_report.sh
  • Renderer with caller-owned destinations: scripts/render_task_concurrency_stress_report.sh
  • Optional E0 report: .genesis/perf/task_concurrency_stress_report.json
  • Optional one-row-per-invocation history: .genesis/perf/task_concurrency_stress_history.jsonl

The check executes the real cancellation, channel-close, and bounded parallel-reduce replay matrix but writes only private temporary outputs. GENESIS_TASK_STRESS_HISTORY is input-only for the check and cannot redirect retained output. The producer preserves the same failure-rate, per-test, and suite-budget enforcement while appending exactly one report row.