Compile-time data-race freedom

Sharing is not something you remember to do. It is something you have to write down.

Most systems languages state data-race freedom as a precondition: reason carefully about sharing, and in exchange the memory model behaves predictably. Break it and you inherit undefined behaviour. Go detects races dynamically, at the cost of a slower build in CI and only for the interleavings a test happened to exercise. C and C++ leave it entirely to the programmer.

Mica moves the obligation into the build. Every touch of shared state must be spelled synchronized, and the compiler rejects the ones that are not — not as a lint, but as a hard error that stops compilation. What a reviewer has to check shrinks accordingly: unmarked code is not shared code.

What it looks like

Concurrency is a visible block with a structural join. schedule starts a task; the block does not complete until its tasks do.

task Client(tag : int64);
begin
    sock := Socket(AF_INET, SOCK_STREAM, 0) on fail use -1;
    synchronized remote := serverAddress;
    rc := Connect(sock, address remote, 16) on fail use -1;

    if n = 4 then
        synchronized echoedCount := echoedCount + 1;
end;

begin
    concurrent
        schedule Client(65);
        schedule Client(66);
        Serve(listener);
    end;
end.

synchronized marks any touch of a cell owned by an ancestor activation. That is the entire surface the programmer sees — one keyword, at the point of access.

What the compiler rejects

Tasks are uncoloured and stackful, arranged on an activation tree. The analyzer performs a transitive effect walk over that tree, stamps every mark with its lock chain, and rejects unmarked shared access. Four things are hard compile errors today, each verified against the shipping compiler:

The diagnostics name the variable, explain why it is shared, and suggest the fix. Two rows matter most in practice. Laundering an access through a helper function does not hide it from the analyzer. And the address rule is not scoped to the concurrent block: taking the address of a cell that tasks can reach is refused wherever you write it — before the block, inside a called procedure, into a record field, or as a returned value — because a raw pointer outlives any mark, and its later dereferences would touch shared state with no lock held.

The one legal way to point at shared state is an alias pointer bound inside a synchronized statement, where the borrow’s scoping bounds every use to the mark’s extent.

Deadlock freedom follows from construction rather than from analysis: owners form a chain — a task’s ancestors — and locks are always acquired in chain order, shallow to deep. A cycle is not reachable.

Reader/writer modes are derived per mark by the same effect walk. There is no separate read-lock syntax to get wrong, because there is no syntax at all.

One source, one or many carriers

The single-carrier default compiles marks to nothing. No fence, no atomic, no lock word anywhere — the scheduler is the lock, and the analyzer keeps that honest by rejecting any suspension point inside a marked statement. That is the embedded stance, and the mark itself costs exactly zero.

Building with multiple carriers plants the scope-lock protocol and links a different runtime archive. The source never changes — not a keyword, not a build flag inside the program. Carrier count is a compile-time decision, so a deployed binary has one known, fixed degree of parallelism rather than one that varies with the machine it lands on.

A single-carrier multicore build produces byte-identical output to the sequential build, which is checked continuously as a corpus-equivalence sweep rather than asserted. The binaries themselves differ — the multicore build plants the carrier configuration and links the multicore runtime archive.

See also

• Determinism
• Heap lifetime proof