Concurrency

Purpose

This chapter defines the common model shared by all Sec concurrency facilities. Later chapters define the exact APIs and syntax for tasks, spawn, await, threads, cancellation, scheduling, channels, events, mutexes, atomics, processes and IPC.

The common model answers questions such as:

• what kinds of execution contexts exist;
• when new execution begins;
• how ownership crosses execution boundaries;
• when values may be shared instead of moved;
• what synchronization means to the compiler;
• how completion publishes memory effects;
• how cancellation interacts with cleanup;
• how tasks differ from physical threads;
• how target profiles constrain concurrency facilities;
• how race and deadlock analyses consume canonical concurrency facts.

Core Principles

Sec concurrency follows several non-negotiable principles:

• execution creation is explicit;
• work is never silently detached;
• ownership and borrowing remain valid across concurrency boundaries;
• deterministic destruction still applies;
• shared mutable state is never introduced implicitly;
• garbage collection is not required;
• runtime ownership tracking is not required;
• ordinary data races are invalid;
• blocking and suspension remain distinct concepts;
• a target may reject unsupported concurrency, but may not silently redefine it.

These rules are deliberately independent of whether the runtime uses native threads, an event loop, a worker pool, an RTOS scheduler, fibers or statically allocated state machines.

Concurrency and Parallelism

Concurrency means that multiple execution entities may make progress independently. Parallelism means that multiple execution entities physically execute at the same time. Sec does not equate the two.

A target may run many logical tasks on one physical thread. Another target may map work across several worker threads. A task therefore does not imply one dedicated physical thread, while an explicit Sec thread does carry physical-thread semantics.

A scheduler may migrate a task between workers when the scheduling and transferability rules permit it. Migration must not change the logical identity, cancellation state, ownership or language-visible behavior of the task.

Execution Kinds

Sec distinguishes several execution kinds:

• Task — a logical Sec execution entity;
• Thread — an explicit physical target execution context;
• Process — a separate process execution domain;
• Interrupt context — target-defined interrupt execution;
• Foreign callback context — execution entering Sec through FFI.

These distinctions survive semantic analysis whenever they affect lifetime, scheduling, blocking, affinity, synchronization, transferability or target support. A backend must not turn a requested physical thread into an ordinary task simply because that would be easier to implement.

Explicit Execution Creation

Calling a function normally does not create asynchronous execution. New task or thread execution requires explicit creation syntax. Process creation is likewise an explicit operation owned by the process rules.

let worker := try spawn Work()

Creation may fail. A target with no required execution capability may reject the program at compile time, while a target that supports the execution kind may still encounter runtime resource exhaustion where the relevant creation rule permits it.

Spawn must also preserve ordinary argument evaluation, ownership transfer, failure and cleanup semantics. It is not a magic exception to normal Sec evaluation rules.

Tasks

Task[T] is the compiler-known owning lifecycle handle for a logical task whose function returns T. The handle is move-only regardless of whether T itself is copyable.

The canonical raw result of ordinary task creation is:

Result[Task[T], TaskSpawnError]

Awaiting a task consumes the owning task handle and always produces TaskOutcome[T]. The static type does not collapse to T merely because the compiler can prove that one outcome is likely or currently reachable.

type TaskOutcome[T] union {
    Completed(T)
    Cancelled
    Panicked(PanicInfo)
    Failed(TaskError)
}

If the task function itself returns Result[V, E], that Result remains the payload of Completed. An application error is not automatically promoted into task execution failure.

Task[Result[Image, IOError]]

// await type:
TaskOutcome[Result[Image, IOError]]

Threads

Thread[T] represents an explicit physical target execution context. Thread creation is distinct from task creation even when a particular runtime happens to schedule some tasks on native threads.

Physical stack behavior, thread affinity, thread-local storage and native scheduling properties belong to the thread model. A task running on a physical worker does not automatically acquire that worker's thread-local identity.

A target without physical-thread capability must reject explicit thread creation rather than silently converting it into task execution.

Processes

Processes form a separate execution and isolation boundary. Ordinary in-process references, raw pointers and process-local handles are not automatically transferable across that boundary merely because their machine representation can be copied.

Process transfer may require IPC, serialization, shared memory, handle duplication or another explicit process adapter. Detailed process semantics are defined later in the process and IPC chapters.

Ownership Confinement

Exclusive ownership is the preferred default for mutable concurrent state. A value owned by exactly one execution entity needs no synchronization merely because other execution entities exist.

Moving ownership to another execution entity transfers destruction responsibility as well. The source becomes unavailable when the ownership transfer commits.

let data := Data.Create()
let worker := try spawn Consume(<-data)

The compiler must not clone a move-only value to make this compile, and it must not silently heap-promote an invalid borrow so that it survives the boundary.

Boundary Transferability

Assignability is not enough to prove that a value may cross every concurrency boundary. Transferability depends on the destination execution kind and the state of the value at the transfer point.

Validation may need to account for:

• ownership and partial-move state;
• active borrows and lifetimes;
• task migration or thread affinity;
• storage and allocation domains;
• destruction-context restrictions;
• closure captures;
• FFI handle and callback contracts;
• process serialization or adapter requirements;
• ISR-specific restrictions.

Transferability is therefore semantic. It must never be inferred simply from whether the bits of a value can be copied.

Shared Immutable Access

Immutable sharing may be valid across concurrent execution contexts, but only when lifetime, storage, publication and transferability rules all permit it.

A shared ref T is not automatically thread-safe merely because the reference value is copyable. The referent may live in task-local storage, on a movable stack, in thread-affine memory or in another location whose lifetime or execution constraints forbid concurrent use.

Shared Mutable State

Shared mutable state requires an explicit concurrency-safe synchronization or ownership mechanism. Ordinary overlapping mutable borrows are not transformed into a concurrency primitive.

Valid strategies may include:

• Mutex[T] for exclusive shared-state access;
• atomic types for supported atomic invariants;
• message passing that transfers ownership instead of sharing it;
• another specialized synchronization abstraction with defined semantics;
• a platform-specific mechanism exposed through a verified Sec abstraction.

Synchronization

Synchronization primitives are semantic operations. They are not recognized from method names or implementation accidents. A primitive must define what it means for ownership, blocking, cancellation, memory visibility and boundary transfer.

A user function named lock is not automatically a lock operation. A foreign function is not automatically synchronization merely because its native implementation happens to use a mutex internally.

Volatile access is not synchronization.

Mutexes

Mutex[T] is the primary exclusive shared-state primitive for ordinary Sec code when mutual exclusion is required. The mutex owns the protected value. Access is provided through an exclusive MutexGuard[T] capability.

The guard is move-only, and its destruction releases the acquisition according to the mutex rules. A live guard is not an ordinary freely transferable owned value. Its lifetime may restrict execution-boundary transfer and suspension.

Sec 0.1 mutexes are non-reentrant. Detailed lock, timeout, cancellation, fairness and priority-inversion behavior is covered in chapter 63.

Atomics

Atomic operations are explicit synchronization operations for supported atomic types. They are useful when the invariant can be represented by the supported atomic object and memory-order semantics.

Atomics are not an automatic substitute for a mutex protecting a multi-location invariant. Atomicity, volatility and ownership exclusivity are separate concepts.

Atomic operations retain their selected memory-order semantics through semantic analysis, Semantic IR and lowering. Concrete target support is resolved through the selected CompilationPlan.

Message Passing and Channels

Message passing is a first-class concurrency strategy. A channel operation must preserve the ownership semantics of the transmitted value rather than hiding copies behind buffering or runtime queues.

A consuming send transfers ownership only at the operation's defined commit point. Failed or cancelled operations must preserve or consume the source exactly as the channel contract specifies. Buffering must not imply hidden cloning of move-only values.

Receive establishes ownership of a received owned value. Borrowed-message designs require their own explicit lifetime semantics and must not be inferred from ordinary owned-value channels.

Static State

Static lifetime does not imply concurrency safety. Immutable static data may be read concurrently when publication and type semantics permit it, but mutable static state still requires synchronization or another safe ownership mechanism.

static let mut State: ApplicationState

// Long lifetime does not make concurrent mutation safe.

A protected form may instead use a synchronization-owning type:

static let State: Mutex[ApplicationState]

Structured Concurrency

Structured concurrency ties child-work lifetime to an owning lifecycle obligation. A lexical scope must not silently abandon unresolved owning child handles.

Awaiting or joining a child discharges lifecycle responsibility according to the specialized task or thread rules. Returning or moving a child handle transfers that responsibility. Explicit detach is the escape hatch from the ordinary structured relationship.

This model preserves deterministic cleanup without requiring garbage collection to eventually discover abandoned work.

Detachment

Detachment is always explicit. It consumes or transfers the owning lifecycle capability according to the relevant execution-kind rule.

Detached work cannot retain a borrow whose source scope may end first. Thread-affine or storage-affine state also remains subject to transferability rules. Detachment does not retroactively make a failed spawn successful; creation must first complete.

Cancellation

Cancellation is cooperative termination control. A request for cancellation and actual cancellation completion are different events.

Cancellation follows a defined control-flow path and must preserve defer execution, destruction of still-owned values and borrow validity. It does not fabricate a normal return value and remains distinct from panic, typed application errors and execution failure.

Detailed current-task/current-thread observation, Context propagation, deadlines, shielding and cancellation checkpoints are covered in chapter 59.

Blocking and Suspension

Sec distinguishes physical blocking from logical task suspension. A suspended task may release its worker so that other tasks continue, while a blocking native call may prevent the physical worker itself from making progress.

An operation may therefore be:

• nonblocking;
• task-suspending;
• physically blocking;
• indefinitely blocking;
• cancellation-aware;
• non-cancellable;
• conditionally blocking according to its resolved contract.

These properties matter to scheduler selection, deadlock analysis, interrupt legality, target validation and capabilities such as live mutex guards.

Await, Join and Completion

Await and join are semantic completion-synchronization operations. They are not mere loops that poll a status flag.

Successful completion synchronization publishes the completed execution's required memory effects to the waiting context. A status read alone does not automatically provide the same guarantee.

Await and join may also differ in ownership: task await consumes the owning task handle, while task join preserves the handle according to the task rules.

Memory Visibility

Sec's concurrency memory model defines the ordering and visibility relationships between execution contexts. Ownership transfer and memory synchronization are related, but they are not identical.

Synchronization constructs establish publication or happens-before relationships according to their own contracts. Examples include task/thread completion, mutex release/acquisition, atomic memory orders and channel operations.

The compiler must preserve required ordering across optimization and lowering. It must not invent synchronization simply because one target instruction is stronger than required, and it must not weaken required synchronization because one current target happens to appear safe without it.

Data Races

Ordinary unsynchronized data races are invalid Sec behavior. This applies across all execution contexts that may overlap, not only tasks and threads.

Potentially overlapping contexts may include:

• multiple tasks;
• multiple threads;
• repeated instances from one spawn site;
• foreign callbacks;
• interrupt handlers;
• platform execution contexts.

Race analysis uses canonical storage identity and Place/provenance facts rather than comparing only source variable names. Ownership exclusivity can prove that sharing does not occur, but borrow exclusivity must not be mistaken for cross-context synchronization.

Deadlocks

A deadlock is a cyclic blocking or progress dependency that prevents required progress. It is distinct from a data race, starvation and livelock.

Deadlock analysis is not limited to mutexes. Completion waits, resource acquisition, foreign waits, callbacks, events, platform synchronization and interrupt interactions may all contribute to a dependency cycle when their canonical semantics require it.

The compiler must distinguish a proven deadlock from a potential or unknown one when precision is insufficient. Missing information must not be fabricated into proof.

Resource Amplification

Concurrent execution consumes real target resources. Recursive spawn, repeated detach, spawn cycles and unbounded creation loops may amplify task, thread, stack, queue or scheduler requirements.

Hosted targets may permit runtime spawn failure when resources are exhausted. Static or embedded targets may instead require a compile-time bound or proof before accepting a creation pattern. The compiler must use the selected target's resources, never the resources of the machine on which the compiler itself runs.

Closures and Captures

A closure used by newly created execution crosses an execution boundary. Its captures therefore have to satisfy both closure rules and concurrency transferability.

Copyable capture does not automatically imply safe sharing of storage referenced inside the value. Moving a move-only capture transfers ownership when the spawn transfer commits. Reference captures require proof of lifetime, address stability, aliasing and destination execution validity.

Detached closures require capture lifetimes independent of the source scope. A thread-affine capture must not enter a migratable task unless scheduling rules prove the task is pinned or otherwise safe.

Task-Local and Thread-Local State

Thread-local state belongs to a physical thread. Task-local runtime state belongs to the logical task. These are separate domains.

If a task migrates between workers, the task's logical state follows the task, while the identity of thread-local storage does not. A reference into thread-local storage therefore carries physical-thread affinity and cannot be retained across migration without an appropriate proof.

FFI and Foreign Concurrency

Foreign code may block, create threads, retain pointers, invoke callbacks from unknown contexts, share memory or use foreign synchronization. The compiler cannot infer safe concurrency from a raw pointer, ABI name or native function name.

A safe Sec wrapper must establish the relevant ownership, retention, synchronization, thread-affinity, callback-context and blocking contracts. Unknown retention remains unknown; unknown callback context must not be treated as the current task or thread.

Interrupt Interaction

Interrupt execution participates in the concurrency model whenever it may overlap or preempt ordinary execution. Shared memory between ISR and ordinary code participates in race analysis, and synchronization/waits participate in deadlock reasoning when the interrupt rules permit those operations.

Ordinary Mutex[T] must not be assumed interrupt-safe. Atomics or dedicated interrupt-safe primitives are valid only where their owning rules and the active target profile permit them.

Unsafe Concurrency

unsafe does not disable concurrency semantics. Ownership, deterministic destruction, lifecycle obligations and target capability rules still apply.

Raw pointers can remove some compiler proof of alias safety, but they do not redefine the language so that races become valid. If safe proof is lost, responsibility moves to the programmer; a concurrency operation already proven invalid by the compiler does not become valid merely because it is placed inside unsafe.

Targets and Runtime Independence

Concurrency validation and lowering use the immutable selected CompilationPlan. Host-machine properties do not leak into target semantics.

Hosted, RTOS and BareMetal are profile families, not fixed scheduler designs. Hosted does not guarantee every concurrency facility. RTOS does not imply hosted-style native threads. Bare metal does not imply that tasks or synchronization are impossible.

Sec also does not require one universal concurrency runtime. A conforming target may use an event loop, cooperative executor, worker pool, fibers, RTOS primitives, native threads or static state machines, provided source semantics remain unchanged.

Errors and Outcomes

Application errors remain separate from execution lifecycle outcomes.

• TaskSpawnError describes failure to create a task.
• TaskOutcome[T].Completed(T) describes normal task completion.
• TaskOutcome[T].Cancelled describes cancellation.
• TaskOutcome[T].Panicked(PanicInfo) describes panic.
• TaskOutcome[T].Failed(TaskError) describes failure of an already-created task execution.

If T is itself a Result[V, E], then Completed(Err(error)) is still normal task completion. Generic Result handling must not flatten or reinterpret the concurrency outcome model.

Cleanup and Destruction

Concurrency does not suspend deterministic destruction. When ownership moves to another execution entity, destruction responsibility moves with it. Values retained by the source remain the source's responsibility.

Cancellation must run required cleanup. Normal completion must perform required destruction before completion is published. Scope exit must not silently abandon an unresolved owning task or thread lifecycle obligation.

Compiler Analysis

Sec's concurrency model is designed to provide canonical facts to semantic analysis, data-race analysis, deadlock analysis, Semantic IR and lowering rather than letting every subsystem invent its own interpretation.

The compiler preserves facts such as:

• execution kind and identity;
• ownership state of handles and transferred values;
• live borrows relevant to boundaries;
• transferability and affinity restrictions;
• synchronization resource identities;
• blocking and suspension effects;
• cancellation and completion semantics;
• memory-order and publication edges;
• target/profile requirements.

The LSP, compiler and sec analyse should consume the same canonical facts. Interactive analysis may refine findings progressively, but mandatory safety rules do not disappear in the editor.

Following Chapters

This chapter provides the shared model. The detailed concurrency surface is split into:

• 55 Tasks — Task ownership, status, observers and lifecycle;
• 56 Spawn — explicit execution creation and transfer;
• 57 Await and Task Outcomes — completion and outcome handling;
• 58 Threads and Thread-Local Storage — physical execution and affinity;
• 59 Cancellation and Context — cooperative cancellation and deadlines;
• 60 Scheduling, Blocking and Structured Concurrency;
• 61 Channels and Select — message passing and multi-wait selection;
• 62 Events — event-style synchronization;
• 63 Mutexes and Locks — protected shared state;
• 64 Atomics and Memory Order;
• 65 Processes and Command;
• 66 Inter-Process Communication;
• 67 Transferability, Data Races and Deadlocks.

Current Implementation Status

The revision-2 concurrency model is normative, while compiler implementation is still partial. Existing frontend work already recognizes several compiler-known task, thread and synchronization concepts, but not every rule described by the full model has complete semantic, IR, lowering or runtime support yet.

Current governance specifically records that:

• Task[T], TaskOutcome[T] and several lifecycle operations already have frontend coverage;
• the full concurrency umbrella model is integrated but marked partial;
• task spawn typing in the current frontend still contains older direct-Task[T] behavior that must converge on the normative fallible spawn model;
• transferability analysis across task, thread, process, ISR and foreign boundaries remains planned work;
• data-race and deadlock analysis have dedicated governance and are not duplicated here;
• Semantic IR and lowering still need complete concurrency lifecycle and transfer operations.

The manual therefore describes the normative Sec 0.1 model. A currently incomplete backend path must not be read as changing the language semantics.

Best Practices

• Prefer ownership transfer over shared mutable state when either design is reasonable.
• Use tasks for logical concurrent work and threads only when physical-thread semantics are actually required.
• Treat spawn as fallible and keep the lifecycle handle visible.
• Resolve, transfer or explicitly detach every owning execution handle.
• Do not assume copyable means transferable or thread-safe.
• Do not keep ordinary mutable borrows alive across concurrent use.
• Use recognized synchronization primitives rather than ad-hoc flag protocols.
• Never treat volatile MMIO access as thread synchronization.
• Keep application Result errors separate from task lifecycle outcomes.
• Distinguish task suspension from physical thread blocking.
• Be cautious with FFI callbacks and foreign retention until explicit contracts prove the concurrency behavior.
• Design detached work so every retained value outlives the detached execution.
• Remember that the selected target profile may provide fewer concurrency capabilities than the development machine.

Summary

• Concurrency is a language-level semantic model in Sec.
• Concurrency and physical parallelism are different concepts.
• Tasks, threads, processes, interrupts and foreign callbacks remain distinct execution kinds.
• New execution is explicit and is never silently spawned or detached.
• Task[T] is a move-only owning lifecycle handle.
• Task creation is fallible and ordinary task spawn has raw type Result[Task[T], TaskSpawnError].
• Awaiting Task[T] always yields TaskOutcome[T].
• Application Result values remain inside normal task completion.
• Exclusive ownership is the preferred default for mutable concurrent state.
• Boundary transferability is separate from ordinary assignability and bitwise copyability.
• Shared mutable state requires explicit synchronization or another concurrency-safe ownership mechanism.
• Volatile access is not synchronization.
• Mutex guards and other execution-bound capabilities may restrict suspension and transfer.
• Channels preserve ownership commit and failure semantics.
• Structured concurrency requires lifecycle obligations to be resolved rather than abandoned.
• Detachment is always explicit.
• Cancellation is cooperative and preserves cleanup.
• Blocking a physical execution context and suspending a logical task are different effects.
• Await and join establish completion synchronization rather than merely reading status.
• Ordinary unsynchronized data races are invalid Sec behavior.
• Deadlock analysis includes generalized wait dependencies, not only mutex ordering.
• Unsafe code does not disable concurrency semantics.
• The selected CompilationPlan controls available target capabilities.
• Sec does not require one universal concurrency runtime.
• Concurrency preserves deterministic destruction and ordinary ownership responsibility.