Transferability, Data Races and Deadlocks

Purpose

Sec deliberately keeps the common concurrency hazards visible in the type and analysis model. The language does not use one broad marker equivalent to “this type is safe everywhere”. Instead, the compiler derives facts from the concrete value, the execution boundary, the operation being performed and the effective execution policy.

This allows the compiler to answer questions such as:

• may this value be moved into a new task?
• may this value cross into another thread?
• does this process payload have a defined cross-process representation?
• may this operation be used from an interrupt context?
• may two execution contexts access this storage at the same time?
• does a synchronization edge order these accesses?
• can this set of waits form a deadlock cycle?

Three Safety Questions

It is useful to keep three questions separate:

Passing one question does not imply the others. A value may be transferable but still require synchronization after transfer. A program may be race-free and still deadlock. A lock-free algorithm may avoid mutex deadlocks while still being logically incorrect for other reasons.

Transferability

Transferability is a compiler-derived property. It is not one user-implemented interface and it is not equivalent to copyability. The answer depends on the destination boundary and on the semantics of the value being transferred.

The compiler derives transferability from the complete semantic value graph. A struct is not task-transferable merely because its outer declaration looks simple; every relevant field and nested ownership relationship must satisfy the required boundary contract.

Compiler Transfer Facts

The compiler uses separate semantic facts for the major execution boundaries. These are compiler facts, not source interfaces that user types manually implement.

These facts intentionally remain distinct. A type can be task-transferable without being process-transferable. A process-transferable value may require serialization or capability transfer rather than preserving its in-process representation. ISR transferability may depend on operation direction and interrupt policy rather than on one blanket type classification.

Recursive Derivation

Transferability is derived recursively through the value graph. The compiler considers relevant fields, payloads, captures, ownership state, references, resources and nested generic arguments.

type WorkItem struct {
    Id: uint64
    Payload: Buffer
}

// WorkItem is transferable across a boundary only when the complete
// concrete value graph satisfies that boundary's transfer contract.

Generic types are evaluated after substitution. There is no rule saying that Container[T] is always transferable merely because the generic container declaration itself is valid.

Copy, Move and Transfer

Copyability, move semantics and transferability answer different questions.

• A copy duplicates a value while leaving the source available.
• A move transfers ownership and makes the source unavailable.
• A boundary transfer additionally requires the value to be legal in the destination execution domain.

A move-only value can still be transferable if the destination boundary supports a valid ownership transfer. Conversely, a trivially copyable machine value can still be invalid to transfer when its semantic meaning is local to one execution domain.

Process transfer makes this especially clear. A raw process-local address may be trivially copyable as bits, but that does not make it meaningful in another process.

References and Borrows

A reference is non-owning and cannot outlive its owner. Crossing an execution boundary therefore requires proof that the referenced storage remains valid for the complete use and that the destination access is permitted by the sharing model.

Detached execution is stricter because the detached execution entity may outlive the scope that created it. A scope-owned borrow cannot simply be captured and carried into detached work unless the compiler can prove a lifetime and sharing contract that makes the reference valid for the entire detached lifetime.

Closures and Captures

A spawned closure is checked through its captures as well as its callable type. Each captured value keeps its own ownership and transfer requirements.

let worker := capture(config) fn() void {
    Run(config)
}

let task := try spawn worker

Whether this is legal depends on the concrete capture. Copyable values may be copied when permitted. Move-only captures may transfer ownership. Borrowed captures require lifetime and sharing proof. A closure that captures an execution-bound guard remains invalid to transfer even though the callable syntax itself is valid.

Guards and Execution-Bound Values

Some values are intentionally bound to the execution entity that created them. MutexGuard[T] is the most important example.

A live MutexGuard[T] is move-only and bound to the acquiring execution entity. It may not cross spawn, detach or a suspension boundary such as await, suspending join or select. References derived from the protected value may not outlive the guard.

let guard := state.Lock()

// invalid while guard remains live:
let task := try spawn ProcessGuard(<- guard)

This rule prevents a lock acquisition from silently migrating to another execution entity or surviving across a suspension where the original lock ownership contract would no longer be valid.

Boundary-Specific Rules

Different boundaries have different semantics. The compiler therefore evaluates the exact operation rather than applying one universal transfer rule.

• Task: may share an address space with its creator, but ownership, borrow lifetime, migration and detach policy still matter.
• Thread: crosses a native-thread execution boundary and must satisfy thread transfer and shared-memory rules.
• Process: crosses an isolation boundary; direct references and process-local pointer meaning do not transfer.
• ISR: obeys interrupt-specific direction, bounded-execution, blocking and target constraints.

Process transfer may use an explicit transfer representation or capability adapter. The source and destination states must follow the process-transfer transaction rules; an unsuccessful transfer must not silently destroy the source resource.

Shared Mutable State

Transferability says whether a value may cross a boundary. It does not by itself make concurrent mutation safe. Once several execution contexts can reach the same semantic storage, the concurrency memory model applies.

Sec prefers ownership transfer and message passing when shared mutable state is not required. When state is shared, use an owning synchronization abstraction such as Mutex[T], a suitable atomic value, a channel protocol, IPC synchronization or another construct whose rulebook defines the necessary synchronization edges.

What Is a Data Race?

A data race requires conflicting accesses to the same semantic memory location from execution contexts that may overlap, where at least one access writes and the accesses are not ordered by the required synchronization model.

The analysis therefore needs to establish:

1. whether the accesses can execute concurrently;
2. whether they refer to the same or overlapping storage identity;
3. whether at least one access can modify that storage;
4. whether an atomic or synchronization rule orders or permits the accesses.

Ordinary sequential source order inside one function does not automatically order an access performed by another concurrently running task, thread, process-shared mapping or interrupt handler.

Storage Identity and Places

Race analysis works on semantic storage locations and Places rather than only source variable names. Two syntactically different expressions may refer to the same storage. Conversely, proven-disjoint fields may represent independent locations.

state.Left
state.Right

When the compiler proves these fields are disjoint, accesses may be analyzed independently. Dynamic indexes and aliasing references remain conservative when disjointness cannot be proven.

Hardware aliases, shared-memory mappings, FFI pointers and other external storage identities require the corresponding platform or FFI facts. Analysis must not guess that differently named storage is independent.

Happens-Before

Sec uses happens-before reasoning to determine when memory effects are safely ordered across execution contexts. Happens-before is built from program-order edges and canonical synchronization edges and is transitive.

A happens-before B
B happens-before C

therefore:
A happens-before C

Synchronization edges can come from mutex release/acquisition, valid atomic release/acquire communication, task or thread completion, committed channel transfer, defined IPC synchronization and other constructs whose canonical rules explicitly create such an edge.

Mutex Protection

Mutex[T] owns one protected value and successful acquisition produces one exclusive MutexGuard[T]. While the guard is live, protected access is tied to that acquisition. Guard destruction releases the mutex and contributes the synchronization edge defined by the concurrency memory model.

Race analysis can therefore use mutex identity and the protected access path as evidence that accesses are mutually exclusive. The proof depends on using the same logical mutex/resource identity; two unrelated locks do not automatically protect the same state.

Atomic Access

Atomic[T] provides indivisible access to one atomic storage identity. Atomic operations avoid torn non-atomic access to that identity and participate in the memory-order model defined by their MemoryOrder.

Atomics do not make surrounding ordinary fields atomic and do not automatically make a multi-field invariant safe. A data structure that requires several fields to change together usually needs a mutex or another higher-level synchronization protocol.

Mixing atomic and non-atomic access to the same storage must follow the atomic rules. The presence of some atomic operations elsewhere in the program is not a blanket race exemption.

Volatile and Unsafe

Volatile hardware access and concurrency synchronization solve different problems. Volatile preserves observable external accesses. It does not establish happens-before between concurrent execution contexts.

Likewise, unsafe permits specific operations that the compiler cannot verify through the normal safe surface. It does not disable the concurrency memory model and does not make a proven data race valid.

Publication

Publication is the act of making a value or state visible to another execution context. Correct publication requires both ownership/transfer validity and the memory ordering required for the receiving context to observe initialized state safely.

Moving ownership through a channel or completing a task can provide both lifecycle and ordering semantics because those constructs define a completion or transfer boundary. Publishing a raw pointer into ordinary shared memory does not automatically provide equivalent synchronization.

Race Analysis Results

The dedicated race analysis uses result categories that preserve the distinction between proof and lack of proof:

Unknown does not mean safe. It also does not mean a race has been proven. Strict contexts may require positive proof, while advisory analysis may report the unknown state with the missing evidence.

What Is a Deadlock?

A deadlock exists when execution entities form a cycle of progress dependencies such that each waits for another dependency in the cycle and none can make the progress required to release the others.

Mutexes are the classic example, but Sec deadlock analysis is not limited to mutex acquisition. Completion waits, channel operations, IPC synchronization, callbacks, foreign blocking behavior and interrupt reentry can all contribute dependencies.

Wait-For Graph

Deadlock analysis models relevant waits and resources as a wait-for graph. Edges may represent acquisition, ownership, completion or another progress dependency.

Task A --waits for--> Mutex B
Mutex B --held by--> Task B
Task B --waits for--> Mutex A
Mutex A --held by--> Task A

A cycle is important evidence, but the analysis must also account for conditional edges, capacities, non-blocking alternatives, timeout/cancellation behavior, reentrancy rules and whether the involved paths can actually coexist.

Lock Ordering

Conflicting lock order is a common source of deadlock.

// path A
let first := accountMutex.Lock()
let second := ledgerMutex.Lock()

// path B
let first := ledgerMutex.Lock()
let second := accountMutex.Lock()

When both paths can overlap, the opposite acquisition order can create a cycle. A consistent order removes that specific cycle and also gives the analyzer stronger evidence.

Sec mutexes are non-reentrant. A proven attempt by one execution entity to acquire the same mutex again while already holding it is therefore invalid rather than being treated as an implementation-defined recursive lock.

Completion and Join Dependencies

Waiting for another execution entity to finish creates a progress dependency. A deadlock can therefore involve task or thread completion even when only one explicit mutex is present.

// Conceptual cycle:
// parent holds State mutex
// parent waits for child completion
// child needs State mutex to complete

Guard rules prohibit carrying a live MutexGuard[T] across suspension boundaries precisely because holding exclusive state while suspending creates severe progress and reasoning hazards.

Channels and IPC

Message passing reduces shared-memory pressure but does not eliminate progress dependencies. Blocking send/receive, rendezvous channels, bounded capacity, select, IPC mutexes, semaphores and process completion may all participate in a wait graph.

In-process Channel[T] and cross-process typed IPC are different transports with different transfer rules. The compiler must preserve that distinction rather than treating every message operation as the same synchronization resource.

IPC analysis also preserves process-level resource and capability identity so a deadlock cycle may cross process boundaries when the participating operations are statically visible.

Callbacks, FFI and ISRs

Open callbacks and foreign code make concurrency analysis harder because the compiler may not know which locks are acquired, whether a call blocks or which execution context invokes a callback. Sec keeps these effects explicit or conservative rather than inventing safe behavior from a function name.

Interrupt handlers add asynchronous reentry. ISR analysis consumes race and deadlock facts together with interrupt priority, preemption and target metadata. A resource that is safe between ordinary tasks may still be invalid when an interrupt can preempt the holder and attempt an incompatible operation.

Deadlock Analysis Results

Deadlock analysis distinguishes stronger and weaker evidence:

A potential deadlock is deliberately not promoted to a language error merely because the analyzer cannot exclude every runtime schedule. Strict environments may impose a stronger project policy, while ordinary analysis can present the evidence and source paths as an advisory finding.

Cancellation Is Not Proof

Timeouts and cancellation may provide an alternate progress path, but the compiler must not automatically treat their existence as proof that deadlock is impossible. Cancellation may itself depend on another task, scheduler event or resource.

Analysis therefore models whether the cancellation path is guaranteed, optional, target-dependent or itself blocked. A timeout that might occur is different from a proof that one must occur before the cycle becomes permanent.

Proof States

The dedicated race and deadlock analyses expose domain-specific findings, while the common compiler-analysis framework also uses the broader conceptual states Valid, Invalid and Unproven.

Tooling must preserve this distinction. “Not proven safe” is not the same statement as “proven unsafe”. Conversely, Unproven must never be silently displayed as a green safety proof.

Analysis Depth

Concurrency safety analyses participate in the common analysis-depth model described in chapter 69. Interactive analysis favors responsiveness, Standard is the normal compiler analysis level, and Deep may spend more budget refining aliases, call targets, wait graphs and cross-context paths.

A deeper analysis may turn an earlier unknown or potential finding into a stronger proof. It must not change the language semantics themselves; it only changes how much evidence the compiler can derive within the available budget.

Diagnostics

Concurrency diagnostics should explain the proof, not merely announce a category. A useful diagnostic identifies the relevant boundary, storage or resource identity, both sides of a conflicting access, or the complete wait cycle where possible.

Representative diagnostic shapes include:

value session is not ThreadTransferable because field socket
owns a thread-affine resource

shared write to state.Counter may race with read in worker task

first conflicting access is here
synchronization edge is missing between these execution contexts

potential deadlock: inconsistent mutex acquisition order
  task path A: AccountState -> Ledger
  task path B: Ledger -> AccountState

MutexGuard[State] is bound to the current execution entity
and cannot cross await

When analysis remains unknown, diagnostics should identify the missing evidence when practical: an open callback target, foreign synchronization, unresolved alias, unknown interrupt relation or target-dependent capability.

Current Implementation Status

The concurrency-safety model is normative across the relevant rulebooks, but compiler implementation is not complete. Several transferability restrictions are already enforced through ownership, spawn, process, mutex and IPC rules. In particular, execution-bound guards and process-transfer restrictions already influence semantic validation.

The dedicated whole-program data-race and deadlock analyses remain planned work in the current implementation ledger. Their analysis books define the intended result models, summaries, happens-before reasoning, wait-for graphs, callbacks, FFI and ISR integration, but the complete analysis pipelines are not yet active compiler features.

This page therefore documents the Sec 0.1 safety contract and the analysis model that compiler, LSP and sec analyse are expected to converge on. A missing current analyzer must not be interpreted as permission for a data race or invalid transfer.

Best Practices

• Prefer ownership transfer or message passing when state does not need concurrent shared mutation.
• Do not assume copyability implies transferability.
• Do not assume task transferability implies thread, process or ISR transferability.
• Keep borrowed captures local unless the compiler can prove their complete destination lifetime.
• Never carry MutexGuard[T] across spawn, detach or suspension boundaries.
• Use one synchronization identity consistently for the state it protects.
• Use atomics only when the invariant genuinely fits the atomic storage and memory-order model.
• Do not use volatile or unsafe as substitutes for synchronization.
• Establish a consistent lock order when code needs several mutexes.
• Avoid waiting for child completion while holding resources the child may need.
• Treat callbacks, FFI and ISRs as real concurrency edges when their execution behavior is open or asynchronous.
• Use named channels, mutexes and IPC resources in diagnostics and design so resource identity remains clear.
• Treat Unknown or Unproven as missing proof, not as proof of safety.
• Use deeper analysis when an important safety property remains unresolved under the normal analysis budget.

Summary

• Concurrency safety combines transferability, memory-order/race safety and progress/deadlock safety.
• Transferability is value-, boundary- and execution-policy-specific.
• Sec derives separate facts such as TaskTransferable, ThreadTransferable, ProcessTransferable, ISRTransferable and ThreadSafeShared.
• Transferability is derived recursively through the concrete value graph.
• Copy, move and boundary transfer are different semantic operations.
• Transfer does not extend reference lifetimes or make borrowed data automatically shareable.
• MutexGuard[T] is execution-bound and may not cross spawn or suspension boundaries.
• A data race requires conflicting unordered accesses to overlapping semantic storage from concurrent contexts.
• Happens-before is built from program order and canonical synchronization edges.
• Mutexes and atomics provide different synchronization models and do not automatically protect unrelated state.
• Volatile and unsafe do not make data races valid.
• Race analysis distinguishes ProvenRace, ProvenRaceFree and Unknown.
• Deadlock analysis reasons over a wait-for graph, not only mutex acquisition.
• Task/thread completion, channels, IPC, callbacks, FFI and ISRs may participate in progress dependencies.
• Deadlock analysis distinguishes ProvenDeadlock, PotentialDeadlock and Unknown.
• Timeout or cancellation is not automatically proof that a deadlock cannot occur.
• The common analysis framework preserves Valid, Invalid and Unproven as distinct proof states.
• Dedicated full data-race and deadlock analysis remains planned implementation work even though the language safety model is defined.