Data-race freedom, proved at compile time

Here is a program in the language of your choice:

Counter := Counter + 1;

Whether that line is correct depends on something not written anywhere near it: whether another thread might be doing the same thing at the same moment. Every mainstream language answers the question the same way — you keep track — and differs only in what it costs you when you get it wrong.

That last row is what this article is about, including the parts of it that are not as absolute as the row makes them look.

The example is examples/DataRaces.

make -C examples/DataRaces run

The rule, in one sentence

While tasks may be running, a touch whose access path is rooted at shared state must stand in a synchronized-marked statement.

Both halves carry weight.

Shared state means a program global, or a cell belonging to an enclosing activation — reached directly, or through any number of dereference steps from such a root. If a pointer lives in a shared cell, what it points at is shared too, because otherwise two tasks could reach one object through “private” pointers.

While tasks may be running means inside a task body, or inside a concurrent block’s own statement list. Nowhere else. And that is what makes the rule livable rather than merely strict:

total := 100;
ledger := 0;
WriteLn("  total starts at %lld", total);

Outside a concurrent block nothing is shared
  total starts at 100

No marks, and none wanted. Outside a concurrent block the structural join has already guaranteed that no task is alive, so there is nobody to race with. Most of a Mica program touches globals with no ceremony at all and is right to. The discipline applies exactly where sharing is possible, which is why it can afford to be absolute there.

Inside the region, every touch is marked

task Bump(rounds : int64);
var
    i : int64;
begin
    i := 0;

    while i < rounds do
    begin
        synchronized total := total + 1;
        i := i + 1;
    end;
end;

Inside it, every shared touch carries the mark
  total after 3000 marked increments: 3100

Delete the word synchronized and the program stops compiling:

analyzer error 5337: a task may touch the program's global variable 'total'
only in a 'synchronized'-marked statement: while tasks may be running, a global
is shared state on every core, so the access must be spelled 'synchronized' to
make that sharing visible — outside the shared region no mark is needed

Note what the mark does not say. It does not name a lock, a mutex, or an object. You marked a statement, and the compiler worked out which locks that statement needs — one lock word per activation, living in its scope head — and acquires them before the statement and releases them after.

Marking the statement rather than the data is the whole design, and the next two sections are why it can work at all.

Hole one: a call cannot launder a touch

This is where most “safe concurrency” schemes quietly stop. Move the shared touch into an ordinary procedure and it is no longer lexically inside the task:

procedure Record(amount : int64);
begin
    ledger := ledger + amount;
end;

task Post(rounds : int64, amount : int64);
begin
    ...
    Record(amount);
    ...
end;

Record knows nothing about tasks. It is a procedure that touches a global, written years earlier by someone with no concurrency in mind. A rule that only looked inside task bodies would accept this program and it would race.

Mica rejects it, and the message is the interesting part:

analyzer error 5337: a task may touch the program's global variable 'ledger'
(reached through the call to 'Record') only in a 'synchronized'-marked
statement: while tasks may be running, a global is shared state on every core,
so the access must be spelled 'synchronized' to make that sharing visible —
outside the shared region no mark is needed

Reached through the call to Record. The compiler computes, for every function, a summary of the shared state its body touches, unioned over everything it calls, to a fixpoint over recursion. A call whose summary is non-empty is a shared touch at the call site. So the mark goes in front of the call, and covers all of it:

synchronized Record(amount);

The mark covers a whole call
  ledger after 1000 marked calls: 2500

That analysis is exact rather than approximate, and the reason is a decision Mica made years before it had tasks: there are no function pointers in the language, no dynamic dispatch, and generics monomorphize. The call graph is closed and static. What a call might reach is knowable at compile time, always, without analysing a heap.

This is the load-bearing connection in the whole design. A language with first-class function pointers or virtual dispatch cannot compute this summary exactly, which is why languages that have them offer you a race detector instead of a race refusal.

Hole two: address cannot launder the root

The rule classifies by the root of the access path. So re-root it:

p := address total;      { shared cell -> a private pointer }
value p := value p + 1;  { the path's root is now the local p }

Refused, at the address:

analyzer error 5341: a bare 'address' of 'total' cannot be taken here: the cell
is shared while tasks may run, and the raw pointer would outlive the lock that
guards each marked touch — bind an 'borrowed pointer' to it inside a
'synchronized' statement for a mark-scoped view, or copy the value out under a
mark

And the message names the legal spelling. An alias is a borrow scoped to the statement that bound it, so binding one inside a mark bounds every use of it to the mark’s extent:

task View(rounds : int64);
var
    view : borrowed pointer int64;
begin
    ...
    synchronized
    begin
        view := address total;
        value view := value view + 5;
    end;
    ...
end;

An alias views shared state for exactly one mark
  total after 200 marked views: 7100

Lock coverage follows syntactically: the view cannot exist outside the mark, so there is no moment at which it points at unguarded state. Using it later is its own refusal (5342).

A mark may not suspend

synchronized
begin
    total := total + 1;
    Yield();
end;

analyzer error 5322: a 'synchronized' statement must not suspend, but 'Yield' is
a suspension point: 'synchronized' promises the statement runs without
preemption, and that promise is what lets the same source stay correct when
tasks run on more than one core — move the suspending call out of the marked
statement

This is checked transitively too — by the same walk that computes the shared touches. It buys three things at once: a critical section is never left half-done for a sibling to observe, cancellation can never route a task out of one, and no task ever stops making progress while holding a lock.

That last one matters more than it looks, and it is the fourth leg of the reason an accepted program cannot deadlock on the locks the compiler plants. The other three: every lock a mark may need belongs to an ancestor of the running task, and ancestors form a chain, so a total order exists; the full transitive lock set is known at mark entry, from the same closed call graph; and locks are acquired all-at-entry in chain order, with a nested mark folding into the outer acquisition as a reentrant no-op. Shallow to deep, one order, no holder ever stalls — no cycle can form.

Deadlock freedom here is a theorem with four conditions, not a promise. Each condition is met because of a specific language decision, and it is worth knowing which, because the theorem is only as good as they are.

Parent cells, and the idiom that avoids them

A global is not the only shared root. A task reaching an enclosing activation’s local touches a cell its parent owns:

procedure Serve(rounds : int64);
var
    served : int64;

    task Count(n : int64);
    begin
        ...
        synchronized served := served + 1;
        ...
    end;

analyzer error 5321: a task may touch a parent activation's variable 'rounds'
only in a 'synchronized'-marked statement: the parent's frame is shared with the
running tasks, so the access must be spelled 'synchronized' to mark that sharing
— unshared locals and functions need no mark

That error is not from served — it is what you get for reading rounds, the parent’s parameter, in the loop test. Which is exactly the nudge the rule should give you. Pass it instead:

schedule Count(rounds);

Now the loop is entirely private, and only the cell that genuinely must be shared is marked. Reaching up is possible; taking a snapshot is better, and the compiler makes the difference visible instead of leaving it to taste.

The escape hatch: copy out, compute free, copy back

Marking every touch would be a poor deal if it meant holding a lock through a long computation. It does not, because Mica’s value model gives you the way out:

task Grind(rounds : int64);
var
    snapshot : int64;
begin
    synchronized snapshot := total;      { copy out, under the mark }

    while i < rounds do
    begin
        snapshot := snapshot + 3;        { own frame: free, no lock held }
        i := i + 1;
    end;

    synchronized total := snapshot;      { copy back, under the mark }
end;

Two locked statements instead of a thousand, and the loop between them is ordinary uncontended code. This is the same shape as the partitioned total, and it is the one to reach for first.

What this does not do

The claim is precise, so its edges are worth stating precisely.

It prevents data races, not lost updates. The hatch above is race-free and, run by two tasks at once, would still let one task’s answer overwrite the other’s. That is a logic bug, and no type system is going to find it. Mica removes the class where memory itself becomes undefined; it does not remove the need to think about what your algorithm means.

It is conservative, deliberately. Classification is by the access path’s root, decided syntactically, with no alias analysis. An owning pointer taken out of a shared cell stays shared until you copy from it, so you will sometimes write a mark you can see is unnecessary. That cost is visible and local; the alternative is a whole-program analysis whose failures would not be.

A plain blocking C call under a mark still stalls. The suspension rule catches Mica’s own suspension points and the parking imports. An ordinary blocking foreign call is not one of them, so a mark around it holds its locks for the duration. Not a cycle — the theorem still stands — but a freeze in practice.

Lock granularity is per activation, not per variable. The root’s lock guards all the globals. Two tasks marking touches of two unrelated globals serialize against each other. That is a performance property, never a correctness one, and reads do run concurrently: whether a mark reads or writes each owner is a static fact, so the scope-head lock is a reader-writer lock and readers of a hot global do not exclude one another.

None of it applies outside the shared region, by design. If you find a way to keep a reference to shared state alive past a concurrent block’s end, you are outside what the rule covers — which is why the join is total and why there is no detached task.

What the compiler proved

You wrote no locks, and the program cannot deadlock on the ones you got. You called an ordinary procedure that touches a global, and the compiler knew, and told you where. You could not take a raw pointer to shared state, and the borrow that replaced it could not outlive its lock. And every total this program printed — 3100, 2500, 500, 6100, 7100 — is identical on one carrier and on four.

The word for a race here is not “detected”. It is “unwritten”.

Next

That completes the concurrency path: tasks and the task tree, generators and streams, carriers, multicore and busy loops, and this one. The capability catalog states the same guarantees in normative form, one page each.