Atomics and Memory Order

Purpose

Concurrent code needs two distinct guarantees. First, access to one shared value may need to be indivisible so readers never observe a torn update. Second, operations may need ordering semantics so ordinary memory written in one execution context becomes safely visible in another.

Atomic[T] provides the indivisible storage operation. MemoryOrder states the synchronization strength required by that operation. The surrounding concurrency memory model then defines publication, synchronizes-with and happens-before.

Sec keeps these concepts explicit so a target backend may choose an appropriate native instruction, intrinsic or verified platform primitive without changing the source-level semantics.

Atomic[T]

Atomic[T] is a compiler-known nominal generic type family. It owns one atomic storage identity containing one value of T.

Atomic[T]

Its physical representation, alignment and target-specific implementation are not exposed as ordinary source fields. User code cannot reach an internal T storage member directly.

Atomicity applies to the complete contained value. A target implementation must not tear one atomic value into separately observable pieces.

Atomic-Compatible Types

Sec 0.1 intentionally defines a conservative atomic-compatible type set. The following categories are semantically eligible:

• bool;
• primitive signed integer types;
• primitive unsigned integer types;
• RawPtr[T];
• integer-backed enums;
• named types whose underlying type is atomic-compatible and whose contracts permit the requested operation.

int and uint are eligible even though their concrete width is selected by the target. The language does not hard-code a maximum machine width into atomic eligibility.

Excluded Types

The following categories are not atomic-compatible in Sec 0.1:

• float, float32 and float64;
• decimal and decimal128;
• string;
• ordinary structs and unions;
• arrays, slices and collections;
• Result[T, E] and Option[T];
• Task[T] and Thread[T];
• arbitrary composite types that merely happen to match a machine atomic width.

This is a language-design boundary, not a statement that every target is physically incapable of atomic operations over those representations. A backend must not silently legalize an excluded Atomic[T] merely because the hardware has a convenient instruction.

Construction

An atomic value is initialized from one ordinary value of T:

let ready: Atomic[bool] := Atomic(false)
let count: Atomic[uint64] := Atomic(0)

Static atomic storage is also valid:

static let Requests: Atomic[uint64] := Atomic(0)

The binding that owns an atomic object normally remains immutable. Mutation of the contained value happens through atomic methods, not by replacing a source-visible storage field.

Requests.FetchAdd(1)

MemoryOrder

The exact Sec 0.1 memory-order type is:

enum MemoryOrder {
    Relaxed
    Acquire
    Release
    AcqRel
    SeqCst
}

The variants mean:

• Relaxed — atomicity and per-object coherence only;
• Acquire — acquire ordering for an operation that reads atomic state;
• Release — release ordering for an operation that publishes through a modification;
• AcqRel — combined acquire and release semantics for read-modify-write operations;
• SeqCst — the appropriate acquire/release behavior plus participation in the global sequentially consistent order.

MemoryOrder is a real source-visible core enum as well as a compiler-known semantic type. Tooling must expose the same canonical declaration.

Default Memory Order

Ordinary atomic methods default to MemoryOrder.SeqCst when the order argument is omitted.

let value := Counter.Load()
Counter.Store(10)
Counter.FetchAdd(1)

are equivalent in ordering strength to:

let value := Counter.Load(MemoryOrder.SeqCst)
Counter.Store(10, MemoryOrder.SeqCst)
Counter.FetchAdd(1, MemoryOrder.SeqCst)

This default gives the simplest portable reasoning model. Weaker orderings are an explicit optimization and should be chosen only when the synchronization argument is understood.

The formatter must not insert explicit MemoryOrder.SeqCst arguments when the source omitted them.

Common Atomic API

Every atomic-compatible Atomic[T] provides the common surface:

impl Atomic[T] {
    fn Load() T
    fn Load(order: MemoryOrder) T

    fn Store(value: T) void
    fn Store(value: T, order: MemoryOrder) void

    fn Swap(value: T) T
    fn Swap(value: T, order: MemoryOrder) T

    fn CompareExchange(
        expected: T,
        desired: T
    ) CompareExchangeResult[T]

    fn CompareExchange(
        expected: T,
        desired: T,
        successOrder: MemoryOrder,
        failureOrder: MemoryOrder
    ) CompareExchangeResult[T]
}

Public names are canonical CamelCase. Spellings such as load, compareExchange or fetchAdd are not the Sec 0.1 public API.

Load

Load atomically reads one complete value of T.

let ready := Ready.Load(MemoryOrder.Acquire)

Valid explicit load orders are:

• MemoryOrder.Relaxed;
• MemoryOrder.Acquire;
• MemoryOrder.SeqCst.

Release and AcqRel are invalid for a pure load because a load does not publish a modification.

Store

Store atomically replaces the contained value and returns void.

Ready.Store(true, MemoryOrder.Release)

Valid explicit store orders are:

• MemoryOrder.Relaxed;
• MemoryOrder.Release;
• MemoryOrder.SeqCst.

Acquire and AcqRel are invalid for a pure store because the operation does not read atomic state.

Swap

Swap is one read-modify-write operation. It atomically reads the previous value, stores the supplied value and returns the previous value.

let previous := State.Swap(newState, MemoryOrder.AcqRel)

All five Sec 0.1 memory orders are valid for Swap because it both reads and modifies the atomic object.

CompareExchange

Sec 0.1 provides strong compare-exchange. The exact result type is:

enum CompareExchangeResult[T] {
    Exchanged
    NotExchanged(T)
}

Exchanged means the observed value matched expected and desired was stored. NotExchanged(observed) carries the value observed by that same atomic operation when the exchange did not occur.

match State.CompareExchange(expected, desired) {
    CompareExchangeResult[WorkerState].Exchanged => {
        // desired is now stored
    }

    CompareExchangeResult[WorkerState].NotExchanged(observed) => {
        // observed is the value seen by this CompareExchange
    }
}

The simple overload uses SeqCst for both success and failure. The explicit overload accepts separate success and failure orders.

Valid failure orders are only:

• Relaxed;
• Acquire;
• SeqCst.

Release and AcqRel are invalid failure orders because a failed compare-exchange performs no modification. Sec does not add a separate rule requiring the failure order to be weaker than the success order.

Fetch Operations

Atomic signed and unsigned integer types additionally provide read-modify-write fetch operations:

impl Atomic[T] {
    fn FetchAdd(value: T) T
    fn FetchAdd(value: T, order: MemoryOrder) T

    fn FetchSub(value: T) T
    fn FetchSub(value: T, order: MemoryOrder) T

    fn FetchAnd(value: T) T
    fn FetchAnd(value: T, order: MemoryOrder) T

    fn FetchOr(value: T) T
    fn FetchOr(value: T, order: MemoryOrder) T

    fn FetchXor(value: T) T
    fn FetchXor(value: T, order: MemoryOrder) T
}

Each operation returns the value stored immediately before its modification. Fetch arithmetic follows the ordinary arithmetic semantics of T. Atomic arithmetic must not introduce C-style undefined signed overflow or silently switch to wrapping behavior merely because the machine instruction wraps.

These fetch methods are not automatically available for bool, enums or RawPtr[T] just because those types are valid atomic payloads.

Operation / Order Matrix

The compiler and LSP must enforce this exact Sec 0.1 matrix:

Invalid combinations are source-level semantic errors. A target backend cannot make an invalid order valid merely because the hardware has an instruction that could be emitted.

Relaxed

MemoryOrder.Relaxed guarantees atomicity and coherent modification order for the atomic object itself. It does not add acquire ordering for following ordinary memory and does not add release ordering for preceding ordinary memory.

Requests.FetchAdd(1, MemoryOrder.Relaxed)

This is appropriate for a counter when no other memory is being published through the increment. It is not, by itself, a publication mechanism for unrelated data.

Acquire and Release

Release publishes ordinary effects sequenced before a modifying atomic operation. Acquire constrains operations sequenced after an atomic read and may observe the publication when the read participates in the required communication relation.

// Producer
Data.Value = 10
Ready.Store(true, MemoryOrder.Release)

// Consumer
if Ready.Load(MemoryOrder.Acquire) {
    Use(Data)
}

The publication is not created merely because the words Release and Acquire appear somewhere in the program. The acquire must observe the qualifying released value, or a value carried through a valid release sequence.

AcqRel

MemoryOrder.AcqRel combines acquire and release semantics in one read-modify-write operation.

let previous := State.Swap(next, MemoryOrder.AcqRel)

It is valid for successful RMW operations and invalid for a pure Load, a pure Store and the failure path of CompareExchange.

SeqCst

MemoryOrder.SeqCst provides the acquire/release behavior appropriate to the operation and also participates in one global order of sequentially consistent atomic operations and sequentially consistent fences.

This is the default order for ordinary atomic methods because it provides the simplest portable reasoning model. The compiler may lower it with a stronger target primitive when necessary, but it may never silently weaken the requested ordering.

Happens-Before

Ownership and borrowing determine who may access a value. The concurrency memory model determines when memory effects are safely visible across overlapping execution contexts. A valid program must satisfy both models.

Sec defines happens-before from program-order edges and canonical synchronizes-with edges. It is transitive.

A happens-before B
B happens-before C

therefore:
A happens-before C

Valid release/acquire communication is one way to create a cross-context synchronizes-with edge. Mutex release/acquisition, task/thread completion, channel commit and other owning concurrency rules may create additional edges.

Volatile access is not synchronization. Ordinary function calls do not create cross-context synchronization merely by being function calls.

Modification Order

Every atomic storage identity has its own total modification order. Sec does not define one global modification order for all atomic objects.

These operations add a modification:

• Store;
• Swap;
• FetchAdd and FetchSub;
• FetchAnd, FetchOr and FetchXor;
• successful CompareExchange.

These do not add a modification:

• Load;
• failed CompareExchange;
• atomic.Fence.

A read-modify-write operation reads and modifies one coherent state as one indivisible operation.

Release Sequences

A release sequence belongs to one atomic object. It starts with a release modification and may continue through a contiguous chain of later read-modify-write modifications on the same atomic storage identity.

// Producer
Data.Value = 42
Counter.Store(1, MemoryOrder.Release)

// Another execution context
Counter.FetchAdd(1, MemoryOrder.Relaxed)

// Consumer
let observed := Counter.Load(MemoryOrder.Acquire)

The relaxed FetchAdd may extend the release sequence. If the acquire load observes the value produced by that qualifying RMW chain, it can synchronize with the release head and thereby observe the producer's prior write.

A plain later Store is not RMW and breaks the preceding release sequence. A failed CompareExchange also cannot extend it because failure performs no modification.

Fences

Sec 0.1 provides the explicit fence operation:

atomic.Fence(order: MemoryOrder) void

The order is mandatory. Valid fence orders are:

• Acquire;
• Release;
• AcqRel;
• SeqCst.

MemoryOrder.Relaxed is invalid for a fence.

A fence does not itself load or store an Atomic[T]. Two fences do not synchronize merely because both exist. Fence synchronization requires the qualifying atomic communication defined by the concurrency memory model.

Data.Value = 42
atomic.Fence(MemoryOrder.Release)
Ready.Store(true, MemoryOrder.Relaxed)

// another execution context
if Ready.Load(MemoryOrder.Acquire) {
    Use(Data)
}

Ownership and Shared Access

Atomic[T] follows ordinary Sec ownership rules and owns exactly one atomic storage identity. Atomic interior mutation is a compiler-known exception to ordinary mutable-borrow syntax: valid shared references may invoke atomic methods.

fn Increment(counter: ref Atomic[uint64]) void {
    counter.FetchAdd(1)
}

This exception applies only to the atomic object's compiler-known interior mutation. It does not authorize unsynchronized mutation of nearby ordinary fields.

Atomic[T] must not expose an ordinary ref T or ref mut T to the contained value. Concurrent access must go through the atomic API or another explicitly defined operation preserving the same contract.

Atomic and Non-Atomic Access

The same shared storage location must not be concurrently accessed through a mixture of atomic and ordinary non-atomic operations.

A stronger order on the atomic side does not repair this. When the compiler can prove invalid mixing statically, it must reject the program. Unsafe code may make proof more difficult, but it does not turn a data race into valid Sec behavior.

Multi-Field Invariants

Separate atomic fields remain separate storage identities. They do not give a reader a transactionally consistent snapshot across all fields.

type Statistics struct {
    Requests: Atomic[uint64]
    Failures: Atomic[uint64]
}

Each field is individually atomic. The enclosing Statistics value is not one atomic object, and ordinary non-atomic fields in the same struct do not become safe for concurrent mutation.

If correctness depends on one invariant spanning several values, prefer Mutex[T] or another higher-level synchronization mechanism.

Named Types and Enums

A compatible named integer type can preserve its identity through atomic operations:

type RequestCount uint64

let count: Atomic[RequestCount] := Atomic(RequestCount(0))
let previous: RequestCount := count.Swap(RequestCount(10))

Fetch arithmetic is available only when the named type's ordinary contracts remain enforceable. A ranged named type must not be atomically incremented into an invalid value merely because the target has a wrapping machine instruction.

Integer-backed enums may use the common atomic surface:

enum WorkerState uint8 {
    Idle
    Running
    Stopping
}

let state: Atomic[WorkerState] := Atomic(WorkerState.Idle)

Enums receive Load, Store, Swap and CompareExchange. They do not receive integer fetch arithmetic or bitwise fetch operations in Sec 0.1.

RawPtr Atomics

RawPtr[T] is atomic-compatible in Sec 0.1.

The guaranteed pointer surface is:

• Load;
• Store;
• Swap;
• CompareExchange.

Atomic pointer operations do not create pointee ownership, extend pointee lifetime or solve memory reclamation. Pointer arithmetic fetch operations are not part of the Sec 0.1 API, and compare-exchange does not imply ABA safety.

Target Capability

The immutable CompilationPlan is the authoritative source of concrete target capability. Capability may depend on:

• the concrete T;
• size and alignment;
• operation kind;
• requested memory order;
• execution context;
• interrupt-safety requirements;
• target architecture;
• runtime and profile policy.

A conforming target may use a native instruction, compiler intrinsic or another verified platform primitive. A hidden blocking global-mutex fallback is not automatically permitted.

If an emulation strategy blocks, it is invalid in a context that forbids blocking. If no conforming implementation exists for the selected plan, compilation must fail with a focused target-capability diagnostic rather than silently degrading to non-atomic access.

Interrupt Contexts

Atomic eligibility does not automatically imply ISR suitability. An ISR may use an atomic operation only when the active CompilationPlan proves that the concrete lowering is valid in that interrupt context.

A blocking emulation cannot satisfy an ISR-safe atomic requirement. Interrupt masking may be a valid target technique only when the platform contract proves that the masking establishes the required exclusion and ordering.

Local interrupt masking must not be assumed to synchronize with another CPU core, DMA engine or unrelated execution domain.

Diagnostics and Tooling

Tooling must present the source-visible atomic model rather than backend intrinsics. In particular:

• hover for MemoryOrder exposes the exact five variants;
• hover for CompareExchangeResult[T] exposes Exchanged and NotExchanged(T);
• completion on Atomic[T] offers only methods semantically applicable to the concrete T;
• completion uses canonical CamelCase method names;
• diagnostics distinguish an invalid Sec operation from a valid Sec operation unavailable for the selected CompilationPlan.

Useful diagnostics include:

error: MemoryOrder.Release is not valid for Atomic.Load
help: use Relaxed, Acquire or SeqCst

error: Atomic[float64] is not atomic-compatible in Sec 0.1

error: this target cannot implement Atomic[uint64].CompareExchange
       with the requested ordering in this execution context

Current Implementation Status

The Sec 0.1 atomic language model is normative, but implementation is currently partial.

The canonical implementation ledger records the remaining work as including:

• source-register the exact core MemoryOrder enum;
• source-register the generic CompareExchangeResult[T] enum;
• expose the exact compiler-known Atomic[T] API through Sema and LSP;
• synchronize member lookup to the canonical CamelCase names;
• implement exact per-T method applicability;
• implement the exact operation/order matrix;
• preserve successful and failed CompareExchange paths distinctly;
• implement atomic.Fence through parsing, Sema, IR and lowering;
• separate semantic eligibility from target capability;
• add target-aware diagnostics and complete tooling support.

Semantic IR atomic facts, final atomic lowering and CompilationPlan atomic-capability modeling are still planned work. The manual describes the normative language surface, not only the currently integrated subset.

Best Practices

• Use SeqCst unless you have a concrete reason to weaken ordering.
• Use Relaxed for independent counters and flags only when no unrelated memory is being published through the operation.
• Use release/acquire as a publication pair when one context publishes ordinary memory for another.
• Do not use atomics as decoration around a multi-field invariant that really needs a mutex.
• Do not mix atomic and ordinary concurrent access to the same storage location.
• Do not assume volatile access provides synchronization.
• Treat compare-exchange mismatch as ordinary control flow and use the observed value returned by the operation.
• Do not assume an atomic pointer solves lifetime, ownership, ABA or memory reclamation.
• Keep target capability separate from source-language type eligibility.
• Re-check ISR suitability separately even when an atomic operation is valid in ordinary thread/task code.
• Use fences only when the synchronization pattern genuinely requires them; a fence by itself is not communication.

Summary

• Atomic[T] owns one indivisible atomic storage identity.
• Sec 0.1 atomics intentionally support a conservative scalar type set.
• Atomic compatibility is a language rule; concrete operation support is a CompilationPlan capability.
• MemoryOrder is exactly Relaxed, Acquire, Release, AcqRel and SeqCst.
• Ordinary atomic operations default to SeqCst.
• Load, Store, Swap and CompareExchange form the common atomic surface.
• Integer atomics additionally provide fetch arithmetic and bitwise RMW operations.
• CompareExchangeResult[T] is Exchanged | NotExchanged(T); mismatch is not an error.
• Failed compare-exchange is a read only and accepts only Relaxed, Acquire or SeqCst failure ordering.
• Sec does not require compare-exchange failure ordering to be weaker than success ordering.
• Every atomic object has its own total modification order.
• RMW operations are indivisible reads plus modifications and may extend a valid release sequence.
• A plain Store breaks an earlier release sequence; a failed CompareExchange does not extend one.
• atomic.Fence requires an explicit non-Relaxed order and does not synchronize by existing alone.
• Atomics do not create ownership and do not make multiple fields transactional.
• Mixing atomic and ordinary concurrent access to one location is invalid.
• Target and ISR capability must be proven independently from source-level atomic eligibility.
• The normative atomic model is complete, while current compiler/tooling integration remains partial.