Concurrency and safety

Structured concurrency

A function that runs concurrent work declares exec in its row; there is no ambient executor. Inside scope(exec), spawn opens a child task, and the scope cannot return while a child is still running. A mutable reference cannot cross into a spawned task, so a value the parent keeps is cloned and handed over with take.

scope(exec) group {
    let ta = group.spawn { net.get_safe(a) }
    let tb = group.spawn { net.get_safe(b) }
    return match (ta.await, tb.await) {
        case (.ok(let ba), .ok(let bb)) => (ba, bb)
        case (.err(let e), _)           => raise e
        case (_, .err(let e))           => raise e
    }
}

There is no syntax for a task that outlives its scope, so a detached spawn is not something an author can write by accident. If a failure makes the scope raise, its siblings are cancelled at their next checkpoint.

Tasks carry errors as values

A spawn produces a linear Task(T), consumed by exactly one of await, detach, or cancel_and_await. Dropping the handle is a compile error. A task body's row may carry capabilities and cancellation but not err: E: once a value crosses the task boundary there is no shared call stack to carry the error contract, so a fallible body returns Outcome(T, E) and the join matches on it.

public function detach(t: take Task) -> ()
public function cancel_and_await(t: take Task) -> () with {cancellation}

Cancellation is an effect. It is handled with handle cancellation -> cleanup { ... } or absorbed by the enclosing scope. ? does not propagate it, so there is no await?.

Coherence regions

Inside scope(coherence), the effects of the body, allocations, mutations, capability calls, are not visible to an outside observer until the closing brace. The guarantee is that no caller sees the partial state. It is not a transaction: if an operation raises partway through, the partial state remains. A mutable parameter's refinements are re-checked at the region's exit.

scope(coherence) build {
    for entry in entries {
        index.insert(entry.key, entry.value)?
    }
    index.shrink_to_fit()?
}

The two forms nest in either order. Putting scope(exec) inside scope(coherence) builds a result in parallel while its intermediate states stay hidden until every task has finished.

Type-state and linearity