Async Reactive Context

An async context is a separate reactive surface for computations whose values are produced by async/future-returning functions. It is not an overload of the synchronous or thread-safe context; it is a distinct graph with its own handles, because futures introduce in-flight state, cancellation, stale completion, and dependency tracking across suspension points that the synchronous graph does not have.

This chapter fixes the cross-language contract. An async context is compute, not protocol — only resolved slot values cross IPC/FFI as ordinary cell payloads, exactly like the synchronous graph.

Why a separate surface

A synchronous reactive context tracks dependencies through a thread-local stack touched on every read, and a slot’s value is either present or unset. An async computation can be in-flight (suspended at an .await) when its inputs change, can complete after those inputs are gone, and can be canceled mid-flight. Those states require:

• an explicit per-slot state machine (not just present/absent),
• revision tracking so a stale completion is discarded,
• dependency edges registered before the read is awaited, and
• a cancellation contract that is safe under waiter drop, supersession, and context disposal.

A binding gates this surface behind a separate feature flag so downstream users do not accidentally accept the larger semantic surface.

Handles

An async context exposes its own copyable, id-only handles, distinct from the synchronous handles:

Handles are id-only and copyable; they are usable only with the owning async context.

AsyncSource and AsyncComputed are the canonical public value kinds in every binding. Published pre-v2 spellings such as AsyncCellHandle and AsyncSlotHandle may remain only as deprecated aliases of those exact types. Constructing through an old spelling must still return the canonical type.

API surface

Sources are the synchronous input layer: source, get, and set are synchronous. Only computed evaluation and effects are async. The constructor and read/write vocabulary is deliberately the same as the local and thread-safe contexts; only the async handle types and get_async are execution-model-specific.

The public state projection is AsyncComputedState. The formal theorem/module name remains AsyncSlotState, because it describes the storage state machine, not a public value-handle kind. Bindings with a published AsyncSlotState API keep it as a deprecated alias of AsyncComputedState; formal references are not renamed mechanically.

Async computed state machine (formal AsyncSlotState)

Each async slot tracks its state through a finite state machine:

            first get_async /         future Ok,          dependency
   Empty ──────────────────► Computing ──────► Resolved ──────► Computing
     ▲         (spawn)        │    │                              │
     │                         │    │ future Err                   │
     │                         │    ▼                              │
     │                         │  Error ──────────────────────────┘
     │                         │   retry get_async
     │                         ▼
     │      dependency invalidation      revision mismatch on
     └──── during in-flight compute ──► (stale) Computing ──► complete discards;
      hard clear                                                new future spawned

Revision tracking is load-bearing: a computation records the slot revision at start; at publish time the graph accepts the value only if the revision is still current. This is what makes stale completion safe.

Transitions:

• Empty → Computing — first get_async or invalidation with no cached value.
• Computing → Resolved — future completes Ok and the recorded revision still matches.
• Computing → Error — future completes Err and the recorded revision still matches.
• Computing → Computing (stale) — invalidation advances the slot revision during an in-flight computation. The completing future finds its revision no longer matches and discards the result; a new future is spawned for the updated revision.
• Resolved → Computing — invalidation marks the cached value stale and spawns a new computation.
• Error → Computing — get_async retry after an error. This transition is mandatory, not optional: a slot in Error holds no cached result, so the next read re-spawns for the current revision. A binding that replays the stored error to every later reader is non-conforming — it makes a transient failure (a timed-out fetch, a disconnected peer) permanent for the lifetime of the slot, with no read path that can recover it. invalidate on an Error slot is therefore a no-op rather than a repair: the retry is owned by the read, not by a dependency change. The executable form is LazilyFormal.AsyncSlotState.step … SlotEvent.retry, which maps error → computing and is a no-op from every other state.

Cancellation contract

A conforming async context MUST honor all five of:

1. Waiter cancellation is safe. Dropping one get_async future does not cancel the shared in-flight computation while other waiters still need it. Each waiter holds a shared handle; dropping a receiver does not abort the in-flight task.

2. Stale completion is discarded, not published. When invalidation advances the slot revision during an in-flight computation, the completing future finds its recorded revision no longer matches and discards the result. Waiting callers are retried against the new revision or attached to the newly spawned future.

3. Explicit cancellation. A hard clear, invalidation, or context disposal may mark the in-flight revision as canceled; if an abort handle is available, the task is aborted. User futures MUST be cancellation-safe, because aborting drops them at an .await boundary.

4. Context disposal. Dropping the async context cancels all in-flight computations via their abort handles and awaits completion of all active cleanup futures before returning.

5. Effect cleanup is triggered by rerun or dispose, and completes before the next body. An effect’s cleanup future MUST run only when the effect reruns or is disposed — the trigger fixed by reactive-graph.md § Conformance (“cleanup runs before each rerun and on dispose”) — and when it runs on a rerun it MUST complete before the next body starts. Disposal removes pending reruns before awaiting cleanup.

   A binding MUST NOT run cleanup at the end of the flush that ran the body. This clause previously stated only the ordering (“cleanup completes before the next body starts”) and left the trigger to reactive-graph.md, which turned out to be enough rope: lazily-py’s async effect awaited cleanup at flush end whenever no rerun was queued, and satisfied the ordering vacuously because there was no next body to be ordered against. Found 2026-07-19 by disarm_disposes_nothing, which asserts cleanup_order: [] at a step where nothing was disposed or invalidated, and observed a cleanup.

   The reason the trigger matters rather than just the ordering: the canonical effect acquires a resource in the body and releases it in the cleanup. Running cleanup at flush end releases the resource while the effect is still live and will rerun later — an effect that subscribes and returns an unsubscribe would unsubscribe itself immediately. lazily-go and lazily-dart both retain the cleanup between runs and execute it at the start of the next one; that is the family behavior.

get_async re-resolve contract

get_async MUST treat the slot state as authoritative and re-resolve rather than assert, because the slot can change between its lock acquisitions and a notifier can close under it. It runs an outer loop that, each pass, re-reads the slot via the get() fast path and then re-locks to attach to or spawn a computation. Two concurrency windows are benign (not data inconsistencies — the published value is always correct):

1. Resolved-since-get(): the slot can transition Computing → Resolved between the fast-path get() (which releases the lock) and the re-lock. Observing Resolved at the re-lock is expected; the cached value is read directly. It is not an unreachable state.
2. Notifier dropped: the per-computation waiters can all close without a final Resolved signal when an in-flight compute is superseded by a newer revision (the stale Computing → Computing transition early-returns) or the slot is invalidated. A “the world changed” error means re-resolve from current slot state — return the now-published value, attach to the new in-flight compute, or respawn. It MUST NOT panic.

Dependency tracking

Async compute and effect callbacks do not use a thread-local tracking stack (a thread-local does not survive executor thread migration or suspension/resume across .await). Instead each callback receives a compute context:

Edges register immediately, so source invalidation while the future is suspended can cancel or supersede the in-flight computation before it publishes stale data. On rerun, stale dependencies are removed and new ones registered; the dependency set is carried by the compute context, not a thread-local.

Async effects

An async effect runs an effect body returning an optional async cleanup:

• Serialized reruns: reruns are serialized per effect — a rerun does not start until the previous cleanup future completes.
• Cleanup trigger and ordering: cleanup runs on rerun or dispose and at no other time — not at the end of the flush that ran the body. When it runs on a rerun, the previous run’s cleanup completes before the next body starts; disposal awaits the current cleanup before removing the node. The cleanup is therefore retained between runs rather than executed eagerly. See § “Conformance” item 5 for why the trigger is normative and not merely the ordering.
• Auto-tracking: the body receives a compute context and tracks dependencies through get_async / get.
• Scheduled, not inline: dependency invalidation schedules an async rerun after the current invalidation pass; the rerun runs on the runtime executor, not inline within send/batch.
• Disposal: removes pending scheduled reruns, awaits the current cleanup future, and unsubscribes dependency edges.

Batch support

batch(run) is a synchronous boundary. Cell updates queue invalidation roots; at batch exit, queued roots trigger propagation. Async slots and effects are scheduled for rerun but do not execute inside the batch callback — async reruns execute after the batch returns, on the runtime executor. Mutation semantics stay synchronous at the graph boundary: invalidations schedule async reruns only after the outermost batch exits.

In-flight deduplication & fast path

• One in-flight computation per revision: each async slot has one published cache and at most one in-flight computation for the current revision. Concurrent get_async callers await the same in-flight result instead of spawning duplicate futures.
• Synchronous fast path: get() returns the cached value synchronously when the slot is Resolved, avoiding async overhead. get_async() calls get() first; only unresolved or dirty slots enter the async spawn path.

Async state machine

A flat State Machine over the async context keeps send and state synchronous (sources are the synchronous input layer) while reactive observers use the async APIs: on_transition returns an async effect handle and state_is returns an async signal handle. Because resolution is asynchronous, eager recomputation settles on the runtime rather than synchronously within send.

Conformance

An async context conforms when:

1. The slot state machine (Empty/Computing/Resolved/Error) and its transitions, including the stale Computing → Computing discard, are implemented exactly.
2. Revision tracking discards every stale completion; a stale value is never published.
3. All five cancellation properties hold, and disposal awaits cleanup.
4. get_async re-resolves through both benign-race windows without panicking.
5. Dependencies are tracked through the compute context (not a thread-local) and registered before the awaited read.
6. Async effect reruns are serialized, cleanup-before-body ordered, and executor-scheduled rather than inline.
7. Batching is synchronous at the mutation boundary; async reruns fire only after the outermost batch exits.

Implementation status

The async surface is required of any binding whose platform exposes an async/future runtime (async/await, promises, coroutines, a suspending executor) — see Wire Protocol § Concurrency layers are required. A binding on a platform with no notion of suspendable async computation declares the async capability as none and advertises it, never silently. A binding that ships the async context MUST honor the full cancellation and re-resolve contract above. API-shape checks for the canonical async-v2 names are informational only: they do not admit a peer to transport, CRDT, queue, or sync feature groups. Network-suite membership continues to follow the binding’s advertised production capabilities, channels, codecs, and variants. Concurrency-window coverage is pinned by targeted deterministic tests rather than exhaustive interleaving exploration, because the async resolve loop runs on a real async executor whose primitives a synchronization-model checker cannot shim.