Mutexes and Locks

Purpose

Ownership transfer is usually the simplest way to avoid shared mutable state, but some programs genuinely need several execution contexts to coordinate access to one mutable object. Mutex[T] provides that shared synchronization boundary without exposing the protected value outside the lock discipline.

The mutex model provides:

• one protected owned value;
• one synchronization identity;
• exclusive acquisition;
• deterministic release through guard destruction;
• acquire/release memory synchronization;
• compiler-visible guard lifetime and execution binding;
• timeout and context-aware waiting without a generic LockError;
• static diagnostics for reentrancy, unsafe guard transfer and suspension hazards.

Mutex synchronization is part of Sec semantics. The compiler must not infer that an arbitrary function is a mutex operation merely because its backend happens to call a native lock primitive.

Core Model

Mutex[T]
    owns one protected T
    owns one synchronization identity

successful acquisition
    produces exactly one MutexGuard[T]

MutexGuard[T]
    owns release responsibility
    provides exclusive protected access
    releases on deterministic destruction

Ordinary contention is normal control flow, not a Sec error. A waiting lock operation may need to wait, time out or observe a cancellation condition, but the fact that another execution currently owns the mutex is not itself exceptional.

Mutex and Guard Types

The source-visible compiler-known type shapes are:

@noCopy
type Mutex[T]

@noCopy
type MutexGuard[T]

Both types have exactly one generic parameter. Mutex[T] is non-copyable even when T itself is trivially copyable, because copying a mutex would duplicate synchronization identity. MutexGuard[T] is also non-copyable because one acquisition must have exactly one release owner.

A guard may move between bindings and function calls within the same execution entity. It is therefore move-only rather than immovable.

fn InspectGuard(guard: MutexGuard[ApplicationState]) void {
    Log(guard.Connections)
}

let guard := State.Lock()
InspectGuard(<-guard)

Construction

A mutex is constructed from exactly one initial protected value:

let state := Mutex(
    ApplicationState {
        Running: false
        Connections: 0
    }
)

Type inference may infer Mutex[ApplicationState]. Explicit typing is also valid. Construction consumes or initializes the protected value according to ordinary Sec constructor and move rules.

Sec does not permit an uninitialized mutex whose protected storage can later be accessed. A usable mutex begins life with one valid protected T.

Static Mutexes

A mutex is the canonical way to protect mutable static state that must be shared between concurrent execution contexts.

static let State: Mutex[ApplicationState] := Mutex(
    ApplicationState {
        Running: false
        Connections: 0
    }
)

The mutex binding normally remains immutable. Protected mutation happens through a mutable guard, so static let mut is not required merely because the protected value will change.

Acquisition API

The exact Sec 0.1 public acquisition surface is:

impl Mutex[T] {
    fn Lock() MutexGuard[T]
    fn TryLock() Option[MutexGuard[T]]
    fn Lock(timeout: duration) Option[MutexGuard[T]]
    fn Lock(context: ref Context) Result[MutexGuard[T], ContextError]
}

Public mutex methods use Sec's CamelCase convention. Lock and TryLock are canonical; older lowercase spellings are not part of the public API.

Sec 0.1 intentionally has:

• no portable LockError;
• no Lock(timeout, context) overload;
• no public Unlock() method;
• no public guard Value or Get() accessor.

Lock()

let state := State.Lock()

Lock() waits until exclusive acquisition commits unless current-execution cancellation wins first. Ordinary contention is not represented as Result or Option; successful return means exactly one guard has been acquired.

When the current execution entity supports cooperative cancellation, waiting in Lock() is a cancellation point. If cancellation commits before acquisition, Lock() does not return. Terminal cancellation cleanup begins. If acquisition commits first, the guard exists and ordinary cleanup releases it before terminal cancellation completes.

TryLock()

TryLock() performs exactly one non-waiting acquisition attempt:

match State.TryLock() {
    Some(mut state) => {
        state.Connections += 1
    }

    None => {
        DoSomethingElse()
    }
}

Some(guard) means acquisition committed immediately. None means the mutex was not immediately available. None is not an error and does not mean cancellation.

Because TryLock() performs no wait, it is not a cancellation point merely by being a mutex operation.

Timeout Lock

The timeout overload uses the canonical temporal duration type:

fn Lock(timeout: duration) Option[MutexGuard[T]]

match State.Lock(5<s>) {
    Some(mut state) => {
        state.Running = true
    }

    None => {
        HandleTimeout()
    }
}

Some(guard) means acquisition committed before the timeout. None means timeout committed first. Timeout is ordinary alternate control flow, not ContextError.

Current-execution cancellation remains independently active while waiting. If terminal cancellation wins first, the operation does not return None. Exactly one event must win: acquisition, timeout or current-execution cancellation.

Time-unit expressions such as 5<s> or 250<ms> are converted to duration by the ordinary unit/temporal rules; the mutex API does not maintain a private list of time-unit spellings.

Context-Aware Lock

A caller may bind waiting to an explicit cancellation/deadline context:

fn Lock(context: ref Context) Result[MutexGuard[T], ContextError]

match State.Lock(ctx) {
    Ok(mut state) => {
        state.Running = true
    }

    Err(ContextError.Cancelled) => {
        HandleCancelledOperation()
    }

    Err(ContextError.DeadlineExceeded) => {
        HandleDeadline()
    }
}

Context cancellation is an operation-local typed result. It does not itself terminally cancel the current task or thread. Current-execution cancellation is separate terminal control flow and, if it wins first, does not get rewritten into Err(ContextError.Cancelled).

The returned guard does not retain the supplied Context. An already cancelled or expired context is observed before a wait outcome commits, so the runtime cannot return a context error and later leak an acquisition.

Acquisition Commit

Waiting mutex operations have one atomic semantic commit boundary. Before commit, no guard exists and the caller owns no acquisition. After commit, exactly one guard exists and owns the acquisition.

before commit
    no guard
    no release responsibility

acquisition commits
    exactly one MutexGuard[T]
    caller owns release responsibility

alternate outcome commits first
    no guard exists

Timeout and cancellation must never partially acquire the mutex. Runtime races between wakeup, timeout and cancellation are implementation details that must collapse to one source-visible winning outcome.

Guard Access

A guard is an access capability, not a copy of T. The complete protected object stays owned by the mutex while the guard is live.

Guards may be borrowed for helper functions:

fn InspectState(state: ref MutexGuard[ApplicationState]) void {
    Log(state.Connections)
}

fn UpdateState(state: ref mut MutexGuard[ApplicationState]) void {
    state.Connections += 1
}

Borrowing a guard does not create another acquisition or another release owner.

Direct Member Forwarding

Member access on MutexGuard[T] forwards directly to the protected T. There is no required wrapper accessor.

let mut state := State.Lock()

state.Running = true
state.Connections += 1
state.Refresh()

The static type of state remains MutexGuard[ApplicationState]. Forwarding is compiler-known member lookup, not an implicit conversion from guard to T.

Lookup order is:

1. guard-specific members, if Sec defines any;
2. ordinary accessible members of the protected T.

Visibility, property rules, generic inference, overload resolution and error typing remain those of the original protected member.

Guard Mutability

An immutable guard binding permits read-only protected access:

let state := State.Lock()
Log(state.Connections)

Mutation requires a mutable guard binding:

let mut state := State.Lock()
state.Connections += 1

The acquisition itself remains exclusive in both cases. Binding mutability controls how this source binding may use the protected value; it does not alter mutex identity or make the mutex reentrant.

Protected References

A reference obtained through guard forwarding cannot outlive the guard. A reference obtained through a borrowed guard is additionally bounded by that guard borrow.

fn Invalid() ref string {
    let state := State.Lock()
    return ref state.Name
}

This is invalid because the reference would survive after guard destruction releases the mutex. Diagnostics should identify both the acquisition and the escaping reference.

Moving Protected Values

The complete protected T cannot be moved out through a guard. A consuming method that would consume complete T is therefore invalid through forwarding.

Copying a copyable protected subvalue is permitted under ordinary Sec rules. Moving an owned subvalue is permitted only when normal partial-move rules allow it and the protected object is restored to a valid releasable state before guard destruction.

Deterministic Unlock

The mutex is released when the final owning MutexGuard[T] is destroyed. This follows ordinary deterministic cleanup paths including normal return, early return, break, continue, error propagation and supported cancellation or unwind cleanup.

fn Update() Result[void, UpdateError] {
    let mut state := State.Lock()
    state.Running = true

    if state.Connections == 0 {
        return Err(UpdateError.NoConnections)
        // guard cleanup releases State before return completes
    }

    return Ok()
}

No defer is required for ordinary mutex release, and Sec 0.1 intentionally exposes no public guard.Unlock(). The guard's destruction is the release operation.

Execution-Entity Binding

A guard is bound to the execution entity that acquired it. This is a logical execution identity, not merely an operating-system thread ID, because a task may migrate between physical workers.

A live guard may:

• move between bindings within the same execution entity;
• move into helper functions executed by that same entity;
• be borrowed by helper functions in that same entity.

A live guard may not:

• move or borrow into another task or thread;
• cross spawn by move, borrow or capture;
• be detached;
• be stored in shared concurrent storage.

let guard := State.Lock()
let worker := try spawn UseState(<-guard) // invalid

Suspension Boundaries

Sec 0.1 does not permit a live guard to cross:

• await;
• a suspending or blocking join;
• select;
• another compiler-classified suspension boundary.

There is no pinned-guard mechanism in Sec 0.1 and no separate AsyncMutex merely to bypass this restriction.

let state := State.Lock()
let outcome := await worker // invalid while state is live

Narrow the guard scope so it is destroyed before the suspension boundary.

Non-Reentrancy

Mutex[T] is non-reentrant. The same execution entity may not acquire the same mutex again while it still owns a live guard for that mutex.

let first := State.Lock()
let second := State.Lock() // invalid when the compiler proves same mutex identity

A statically provable repeated acquisition is a semantic error. Diagnostics should identify both acquisition sites. Checked profiles may additionally provide runtime self-lock detection when the identity cannot be proven statically.

The mutex type itself does not require full dynamic deadlock detection. General deadlock analysis belongs to Sec's concurrency analysis layer.

Memory Synchronization

Successful mutex acquisition provides acquire synchronization. Guard destruction and release provide release synchronization.

execution A                         execution B
-----------                         -----------
lock State                          lock State
write protected data                read protected data
release State  --------sync------> acquire State

A release of one mutex synchronizes with a matching later successful acquisition of the same mutex identity. Writes before release become visible after that synchronizing acquisition.

Two different mutexes do not synchronize merely because they protect values of the same type.

Mutex Identity and Movement

Mutex[T] is @noCopy, but an owned mutex may move when ordinary ownership and synchronization-identity rules permit it. Before publication or locking, moving a mutex can be valid.

Once another execution context depends on the mutex identity, movement must preserve that identity. A live guard, waiter or identity-dependent reference forbids a move that would invalidate the synchronization object.

A struct may own a mutex. Each struct instance owns its own mutex identity, and copying the enclosing struct is invalid when that would copy the contained mutex.

type Server struct {
    State: Mutex[ServerState]
}

Destruction

Destroying Mutex[T] destroys the protected T exactly once. The mutex itself may not be destroyed while a live guard, waiter, valid reference or published execution context can still use it.

Where ownership and lifetime information is sufficient, the compiler proves these destruction requirements statically. Forced unsafe termination is outside ordinary safe cleanup guarantees.

No Implicit Poisoning

Sec 0.1 does not use implicit mutex poisoning. Panic, task failure or cancellation does not automatically make a mutex permanently unusable.

When deterministic cleanup runs, the live guard releases the acquisition. If protected application state can become logically inconsistent, recovery belongs to that application's typed state/error design rather than to a universal poisoned-mutex bit.

Fairness and Priority

Sec 0.1 does not guarantee strict FIFO mutex fairness. A target/runtime may use FIFO, priority-aware, scheduler-defined or platform-native waiting.

Priority inheritance, priority ceiling and scheduler-specific priority behavior are target/profile properties. They may affect implementation and timing, but they must not change source ownership, guard lifetime or non-reentrancy semantics.

Interrupt Contexts

Ordinary Mutex[T] is not assumed ISR-safe. Blocking Lock overloads are invalid in execution contexts whose contract forbids blocking unless the selected CompilationPlan proves a compatible implementation with identical source semantics.

TryLock() may be usable in additional contexts only when the selected target explicitly permits it. Local interrupt masking is not automatically equivalent to a portable mutex across cores or execution domains.

Foreign Mutexes

A native or foreign mutex is not automatically a Sec Mutex[T]. A safe adapter must define the complete semantic contract: ownership, acquisition, release, execution binding, cancellation behavior, memory ordering, destruction and context validity.

Native platform error codes do not automatically become a portable LockError. Sec 0.1 deliberately has no such generic mutex error type.

Context Surface Used by Mutex Waiting

The detailed cancellation model is covered in chapter 59, but context-aware mutex acquisition depends on the following compiler-known surface.

enum ContextError error {
    Cancelled
    DeadlineExceeded
}

@noCopy
type Context

@noCopy
type ContextSource

type Instant

impl Context {
    static fn Background() Context
    fn WithCancel() ContextSource
    fn WithTimeout(timeout: duration) ContextSource
    fn WithDeadline(deadline: Instant) ContextSource

    IsCancelled bool
    Error Option[ContextError]
    Deadline Option[Instant]
}

impl ContextSource {
    Context ref Context
    fn Cancel() void
}

Context has no public Cancel(). Cancellation authority belongs to ContextSource. The source owns its derived child context and exposes it only as ref Context.

Destroying a ContextSource ends the branch lifetime; it is not defined as an implicit cancellation event.

Static Analysis

Semantic analysis must track at least:

• mutex identity and concrete protected type;
• guard ownership, moves and borrows;
• guard lifetime and acquiring execution entity;
• the selected acquisition overload;
• timeout duration or context identity where applicable;
• forwarded access and references derived from protected state;
• release and synchronization edges;
• reentrancy and suspension-boundary violations;
• target capability requirements.

Data-race analysis can use the mutex identity and protected-access path as proof of exclusive synchronized access. Deadlock analysis can consume lock acquisition and ownership facts together with other waits and progress dependencies.

Semantic IR must preserve these facts explicitly. Lowering must not rediscover mutex meaning from a method name such as Lock or from a native runtime call.

Diagnostics and Tooling

Representative diagnostic shapes include:

Mutex requires exactly one type argument

mutex State is already locked by the current execution entity

MutexGuard[ApplicationState] is bound to the current execution entity
and cannot cross spawn

mutex guard state remains active across await

cannot return reference to mutex-protected value beyond guard lifetime

cannot move the complete protected ApplicationState out of
MutexGuard[ApplicationState]

LSP hover for Mutex[T] should expose its @noCopy classification, protected type, exact acquisition overloads and non-reentrant behavior. Hover for a guard should expose deterministic release, execution binding and direct forwarding.

Completion on a guard includes accessible forwarded members from T, but must not invent Unlock, Value or Get.

Current Implementation Status

The mutex language surface is normative, while compiler integration is currently partial. The governance ledger records the following normative surface:

• Mutex[T] and MutexGuard[T] are compiler-known @noCopy generic types;
• the public acquisition surface is Lock(), TryLock(), Lock(duration) and Lock(ref Context);
• guard forwarding and non-reentrancy are normative;
• live guards may not cross spawn or suspension boundaries;
• there is no portable LockError or public Unlock/Value/Get API.

Remaining implementation work includes:

• synchronizing canonical CamelCase method registration and older lowercase call sites/tests;
• complete @noCopy semantics for mutexes and guards;
• exact timeout/context overload resolution;
• deterministic guard destruction and release lowering;
• execution-entity-bound guard escape analysis;
• live-guard diagnostics across await, join, select and spawn;
• same-execution repeated-lock detection;
• complete forwarding for fields, properties, methods and lifetime-aware references;
• acquire/release integration with the concurrency memory model;
• target/platform lock capability through the selected CompilationPlan.

Mutex Semantic IR and final lowering are still listed as planned work. This manual chapter describes the normative Sec 0.1 contract rather than only the subset already accepted by the current frontend.

Best Practices

• Prefer ownership transfer or message passing when shared mutable state is unnecessary.
• Let Mutex[T] own the state it protects rather than storing an unrelated lock beside mutable data.
• Keep guard lifetimes short and visibly scoped.
• Destroy the guard before await, suspending join, select or another suspension boundary.
• Use TryLock() when waiting is not acceptable.
• Use Lock(duration) when timeout is ordinary alternate control flow.
• Use Lock(ref Context) when an operation should follow an explicit cancellation/deadline branch.
• Do not attempt to acquire the same mutex recursively.
• Do not transfer a guard through spawn, detach or shared storage.
• Use a mutable guard binding only when the protected value must actually be mutated.
• Do not return references derived from protected state beyond the guard lifetime.
• Do not call consuming methods that would move the complete protected value out of the mutex.
• Do not add manual defer solely to unlock a normal guard.
• Do not assume FIFO fairness, priority inheritance or ISR safety unless the selected profile says so.
• Use atomics instead when the invariant genuinely fits one supported atomic value and explicit memory-order semantics.

Summary

• Mutex[T] owns exactly one protected T and one synchronization identity.
• MutexGuard[T] represents exactly one successful exclusive acquisition.
• Both mutexes and guards are @noCopy.
• Mutex construction requires one valid initial protected value.
• Static mutexes are the canonical mechanism for synchronized mutable static state.
• The exact acquisition surface is Lock(), TryLock(), Lock(duration) and Lock(ref Context).
• Ordinary contention is not a Sec error and Sec 0.1 has no portable LockError.
• TryLock() returns Option[MutexGuard[T]] and never waits.
• Timeout lock returns None when timeout wins.
• Context-aware lock returns typed ContextError when the supplied context branch wins.
• Current-execution cancellation remains separate terminal control flow.
• Waiting acquisition has one atomic semantic commit boundary.
• Guards forward accessible fields, properties and non-consuming methods directly to protected T.
• There is no public Unlock, Value or Get guard member.
• Guard destruction deterministically releases the mutex.
• Guards are execution-entity-bound and may not cross spawn or suspension boundaries.
• Mutex[T] is non-reentrant.
• Successful acquisition is acquire synchronization; guard release is release synchronization.
• The complete protected value cannot be moved out through a guard.
• Protected references cannot outlive the guard.
• Sec 0.1 does not use implicit mutex poisoning or guarantee strict FIFO fairness.
• Ordinary mutexes are not assumed ISR-safe.
• The normative model is complete, while current compiler integration remains partial.