Mica adopts DRF-SC: data-race-free programs are sequentially consistent.

Most systems languages state that as a bargain with a footnote attached. Reason correctly about sharing and the memory model behaves predictably; get it wrong and the behaviour is undefined. Mica’s design removes the footnote by moving the precondition into the build: the program that races is meant to be rejected at compile time, not left undefined at run time.

This page is about ordering — which operations establish it, and what it covers. The marking discipline that enforces the precondition, and the shapes the analyzer rejects, are on compile-time data-race freedom. Bit-identical numeric results across carrier counts and architectures are on determinism.

What the model says

For the sharing the analyzer covers, every execution of an accepted program is equivalent to some interleaving of its tasks’ operations, with each task in its own program order. There is no relaxed tier to opt into, and no ordering vocabulary anywhere in the language: no memory-order argument, no acquire, no release, no fence, no volatile. A Mica program does not select a memory ordering. Ordering is something the compiler and the runtime owe it.

The reasoning surface is therefore small: program order within a task, plus the edges below. There is nothing else to learn.

The happens-before edges

Every ordering guarantee a program can observe comes from one of these seams. On the single-carrier default they hold trivially — one carrier runs each task to its next suspension point, and marks compile to nothing at all. On a multicore build each seam is carried by an explicit acquire/release pair in the runtime, where the guarantee is actually paid for.

Ordering edge (HB = happens-before)Runtime seam that carries it
schedule HB the task body startingready-queue publish, then the carrier’s dequeue
A task finishing HB the block’s join completinglive-child decrement (release) paired with the drain’s load (acquire)
A child’s fail HB the parent’s on fail sectionfirst-wins error latch by compare-and-swap (release) paired with the block-end take (acquire)
A scope cancel HB cancellation being deliveredcancel-generation write (release) paired with the safepoint read (acquire)
A deadline firing HB ScopeTimedOut answering truefired-flag write (release) paired with the query’s read (acquire)
An unpark HB the resumed task’s next readthe park state machine’s handoff to a carrier
A lock release HB the next acquire of the same lockthe scope reader/writer lock’s own ordering
Leaving a synchronized mark HB the next mark naming the same ownerthe same scope lock, taken once per owner in chain order

Marks are mutually exclusive against every other mark that writes the same owner. That is the row most programs lean on, and it is the one the compiler plants without being asked.

What that buys, in code

program SynchronizedCounter;

imp
    WriteLn : std;

var
    count : int64;                      { the one shared global every task increments under the mark }

    { one worker: 'rounds' marked increments of the shared global, each holding the root's scope lock }
    task Bump(rounds : int64);
    var
        i : int64;
    begin
        i := 0;

        while i < rounds do
        begin
            synchronized count := count + 1;    { the critical section: read, add one, write, all under the lock }
            i := i + 1;
        end;
    end;

begin
    { the concurrent block spans the three workers' whole lifetime; the join at 'end' guarantees all three
      have finished and counted themselves in before the root reads the total }
    concurrent
        schedule Bump(1000);
        schedule Bump(1000);
        schedule Bump(1000);
    end;

    WriteLn("count %lld", count);        { free: the join guarantees no task is alive to touch 'count' now }
end.

Two rows of the table are doing the work. The mark row makes each read-modify-write indivisible against every other mark on the same owner, so no increment is lost. The join row makes the final read safe and unmarked: the block does not complete until every scheduled task has, so by the time the root reads count no task is alive that could touch it. The total is exact on the single-carrier default and on a multicore build at any carrier count: the output is a sum, not an interleaving.

This program is part of the merge-gated corpus — 1,389 programs, 8,436 declared runs as of 2026-07-22 — and its expectation is replayed on the single-carrier default and on multicore builds at more than one carrier count.

See also