Nikaia
Menu
v0.0.1343pre-alpha GitHub

ADR-281: Shared Mutable State Is SharedMut[T], Its Shape Is Chosen Per Value, It Opens Through Four Doors, and What Leaves It Is Stamped

Status: Accepted Date: October 3, 2026 History: the records this one replaces are archived in docs/history/adr; read them only for how the decision was reached Answers: whether Locked[T] keeps two implementations or gets one Mutex floor, and what the shared mutable type is called; what a lock is in the machine; how a block that changes locked data says so; how a hull is made; what a door over several locks is called and whether it hands a value back per lock (#245); the two refusals that come with the doors (#175); what access may do and how update changes a large value; the lost update written over two lines; the re-entrancy switch; I/O under a lock that neither pauses nor takes a lock, which ADR-288 D21 leaves to this record; and update’s compare-and-swap row (#184) Displaces: Part II 12.2’s per-setting split of the lock (D5-D7); Part II 12.3’s “often a compile-time error”, Part II 12.2’s “safety net” sentence and ADR-005 D6’s last sentence (D28); Part I 6.2’s definition of Locked[T] by the nesting (D3); Part II 12.2’s sync-lambda derivation and ADR-297 D3’s “for free” (D10); ADR-312’s annotation as the constructor (D2); Part I 6.3’s sentence about appending through access (D11); ADR-021 D5’s cache-key enumeration, which gains a dimension (D37); and ADR-037 D7, which gains a third answer, word (D8) Related: ADR-037 D2, D6, D7 (one user thread at no; the atomic count as the floor; the per-value inference D7 here rides on), ADR-312 D6-D8 (a lock may go into a task of our own and not into code nothing describes — the crossing verdict, which this record does not restate; the count, plain at one user thread; a handle is duplicated, never moved), ADR-288 D21 (a door’s block is sync and touches no lock; NK2202 against NK2203) and its sync fixpoint, which D29 mirrors, ADR-094 D3 (mut on a parameter is in-place change), ADR-292 D3 and D7 (touches; a default that cannot be declined is imposed), ADR-288 D15 (sync = "from(f)"), ADR-303 D7 (the foreign-thread rule D32 extends), ADR-010 D1 (the polarity D31 and D34 each depart from, for their stated reason), ADR-025 D6 (iterates, the precedent for a column on a type), ADR-313 D5 (why the doors and the shared types need no use), ADR-258 (the four weights). Evidence: mutex-floor.md, lock-free.md.

1. Question

How does a program share a value that changes — what is the type called, what is it in the machine, how is it read and changed, and what may run while it is open?

The answer decides whether Part II 12.2’s counter — the program user_parallelism = yes exists to serve — can be written.

2. How others do it

Language / tool Its answer What it costs there
Rust two wrappers, Arc<Mutex<T>>; RefCell panics on a re-entrant borrow, a Mutex hangs on one, and a panic under a Mutex poisons it the composition everybody complains about; two behaviours for what a reader thinks is one thing (D4)
Clojure atom, Haskell MVar / TVar, Scala Ref one name for the capability, no composition; the cell is made by a call, and a change takes a pure function none of them can spell it as a count around a lock; the pure change is what allows compare-and-swap with retry
C++ std::lock several locks at once, by try-and-back-off a different mechanism from sorting two by address
Perl taint mode data from outside is marked; one word removes the mark somebody removes it early to make the types fit, and three functions later nobody remembers

What does not transfer: Rust’s split into two wrappers, because the combination is this language’s common case; a mark that can be removed. What does: one name made by a call, and a change written as a block the implementation may run more than once.

3. Options, weighed

The options rejected, one row each; the number that decided, where there was one, is in §5.

Question Option rejected Why it lost See
what is under the lock one Mutex floor at both settings pays 11.3 ns an acquisition at no, where it unlocks nothing; a conflict-refusing flag needs the same atomic and its refusing branch is dead under D28 D4
  one shape per build setting decides a property of a value somewhere other than where the value is; a library cannot know its own type across its boundary —
  two shapes that behave differently a per-value choice the reader cannot see must not change what a program does D9
the name Shared[Locked[T]] as the spelling, or as a second one Rust’s wart; the same bytes below, two types above D3
  a name that is the mechanism closes the door to a lock-free implementation that D8 walked through D1
the first hull the annotation as the constructor constructs only where a position says so, and the list of positions had four holes — a literal, a return, an argument, a field D2
the doors one door that carries every rule three of four shapes of change need none of them D10
  access changing through its parameter, with mutability arriving from the callee unspelled the first place a change would not be written on the line —
  a second lambda form for a mutable parameter mut on a parameter already exists (ADR-094 D3), and one lambda form is what ADR-277 protects D12
  update as a pure function, value in and value out a large value is moved out and back, and a panic leaves an empty slot —
several locks a ledger entry a signature binds from a receiver, and there is none D17
  a keyword, or a method on one lock a reserved word buys nothing the call form lacks; a method implies an order, which is the bug D17
the lost update a dataflow pass over one body, or across calls stops at the function boundary, or at time — a value kept in a struct between requests —
  a version carried and checked at run time reports the collision when it happens; a counter per lock and sixteen bytes per value —
  a stamp with a word that removes it Perl’s taint again —
what may run inside a precise which lock analysis whether a program compiles would depend on aliasing an unrelated line can change D30
  a copy of the crossing walk for foreign calls re-derives four subtleties, and gets the empty field list of fs::Mapped wrong D32
  a type’s touches read fail-closed what is built on it is a refusal, and refusing on doubt refuses correct programs D34
the runtime check always on; on the command line; named debug a default that cannot be declined is imposed; a command-line switch makes a shipped build irreproducible; it is a guarantee, not a development aid D36

Where two weights pulled apart, the reader’s (D2, D4 of ADR-258) is chosen only where the program’s (D1, D3) cost nothing: the mutex shape pays its owner check (D9) so that one written type has one behaviour, and that check falls only on values that actually cross.

4. Decision

The type

D1 — Shared mutable state is SharedMut[T]: one name for the capability, and it survives to the emitter.

SharedMut[T] means a value several parts own at once and any of them may change. It does not mean a count around a lock; what is under it is the compiler’s, chosen per value (D5-D8). The short name is for the common case and is a deliberate departure from spelling words out.

It is one name up to the emitter and becomes two hulls only there, so no internal spelling appears in a diagnostic, a printed type or a ledger entry. Naming the capability rather than the mechanism keeps the lock-free implementation possible — which D8 uses.

D2 — A hull you can observe, you write: Shared(x), SharedMut(x) and Locked(x) are calls.

A hull you cannot observe, the compiler writes. A hull you can observe, you write.

A T?’s Some(…) stays the compiler’s (ADR-278); these three change when a value is cleaned up, which a program can see. A call is an expression, so a hull is made wherever an expression stands — a literal, a return, an argument, a field — and SharedMut(0) gives the number its type as any argument does. The call is typed by the compiler, not the ledger: a ledger signature binds from a receiver (ADR-288) and a constructor has none.

D3 — Shared[Locked[T]] is refused, and Locked[T] is the lock on its own, for individually locked fields.

NK1123 refuses the long spelling, and a hull of a hull, with the replacement in the message. Locked[T] keeps its own use — one lock per field inside a shared structure rather than one around the whole — and is opened by the same doors. Part I 6.2 defines it by that use, not by the nesting.

What is under it

D4 — Two shapes stay, and the difference between them is made unobservable rather than bought away.

A cheap shape (a borrow flag) and a robust one (an operating-system mutex) both stay. What a program could see between them — re-entering one lock panics under one and hangs under the other — is made impossible at compile time (D28), not paid for with a floor on every acquisition in every program. Poisoning is not unified: at no a panic is a process abort (Part III A.2), so nobody survives for whom poisoning would be done.

D5 — The safe shape is the floor, and the cheap one is an optimisation on top of it.

Where it is not proved that nothing crosses a thread with a value, its lock is the mutex. ADR-037 D6’s polarity, for its reason: wrong towards the mutex costs nanoseconds, wrong towards the flag costs correctness.

D6 — At user_parallelism = no every lock is the cheap shape.

Nothing a user writes can cross a thread there: one user thread (ADR-037 D2), and the runtime’s I/O thread carries no closure and cannot reach a user lock. The mutex would buy nothing and cost what the switch exists to save — and the cheap shape says so when a lock is re-entered, where the mutex hangs.

D7 — At user_parallelism = yes the shape is decided per value, by the analysis that decides the count.

A lock is reachable from two places only through a shared handle, so the answer contracts::sharing gives the handle is the answer for the lock inside it — one analysis, two decisions, and every one of its reasons to decline carries over unchanged.

D8 — A word-sized value that crosses is the word, and its update is a compare-and-swap.

A third answer of the same analysis, beside plain (the cheap lock) and atomic (the mutex): word, an atomic count around an atomic 64-bit word whose update is D13’s retry loop and whose set(…; after:) is one compare-and-swap. A class of handles gets it where all of these hold:

It never replaces the cheap shape, and at no nothing gets it.

D9 — The shapes behave alike, and the mutex shape pays for it with an owner check.

Rc and Arc differ in cost and nothing else, which is what makes a per-value choice invisible. A borrow flag and a mutex do not, so the mutex shape carries an owner check and re-entering a lock says the same thing whichever shape a value got. One behaviour, two prices. Whether that check is emitted at all is D36’s switch.

The doors

D10 — Four doors, and while the lock is open in get or set no user code runs.

door for the block may wait
kasse.get() taking a copy out —
kasse.set(value) replacing; the value is computed outside yes, outside
kasse.update fn(mut v) { v += 100 } changing it, under the lock no
kasse.access fn(state) { … } reading it in place no

set needs no block: its argument is evaluated before the call, so the lock is open for one store, and get is one load. While the lock is open in get and set, no user code runs at all — no derivation through a sync lambda is needed, since set has no lambda.

get and access are reads; set and update are writes. Under ADR-292 D3 two reads of one resource are unordered, so two gets or two accesses on one lock may run in either order, and the writing forms keep theirs.

D11 — access reads in place, and may not change what it is handed.

It hands the block the value where it lies and returns what the block computed. It stays because nothing else reads part of a large value without copying it: get copies, and asking a ten-thousand-entry list for its length should not.

D12 — update has one form: the block takes mut v, changes it, and returns nothing.

kasse.update fn(mut v) { v += 100 }
protokoll.update fn(mut log) { log.push(entry) }

mut is ADR-094 D3’s word, unchanged: the value is changed in place, and the caller’s value — here the lock’s — is what changes. A block that hands a value back is NK1141; one that changes v without the word is NK1138, asked at a door. So exactly one lambda in this language is handed something it may change, and it carries the word every changed parameter carries; Part I 5.3’s one lambda form is untouched.

D13 — What v is, is the compiler’s, by type: a copy where the value is a word, the address otherwise.

the value v is the door does
in D8’s word class a copy on the stack load the word, run the block on the copy, compare-and-swap it in; on a collision load again and run again
anything else the address in the lock take the lock, run the block once, release

Nothing is moved out of the lock in either row and no slot is ever empty. The program writes one form and learns nothing about word sizes or user_parallelism from it.

D14 — An update block may run more than once, and a program cannot tell.

The three things that would let a program notice are already refused at every door: the block is sync, so it does not wait; it touches no lock, so it does no I/O and takes nothing else (ADR-288 D21); and it captures its surroundings as views (Part I 5.3), so it changes nothing outside v. The retry is used only where the copy is free; a block on an address runs once, because a change to the address cannot be taken back.

D15 — A panic in the block leaves a word untouched and poisons an address.

On a copy nothing was swapped in. On the address the value stays as the block left it, and D4 applies: an abort at no, poisoning at yes, where the next door on that lock refuses.

D16 — get is the one door that copies, and --sharing says where it copies something large and which row each value got.

--sharing names a get on a type that does not copy cheaply — big.get() copies the whole String out of the lock each time; access reads it in place — reports a word as word (its update is a compare-and-swap and there is no lock), and says why a word-sized value that crosses kept its lock: a door over several locks, or the floor.

D17 — A door over several locks is a call the compiler types.

Not a ledger entry: a signature binds from a receiver and the locks are arguments of different types. Not a construct: the grammar already takes access_all(a, b) fn(x, y) { … } as a call with a trailing lambda, and a keyword would cost a reserved word for nothing. Not a method on one lock: a.update_with(b) reads as first A, then B, which is the bug. The checker types the locks and hands the block one parameter per lock; the ledger carries the sync column, sync = "from(f)", from an entry with no signature.

D18 — access_all reads; update_all takes one mut per lock, returns nothing, and keeps the lock.

update_all(konto_a, konto_b) fn(mut von, mut nach) {
    von -= 30
    nach += 30
}

D12 widened, not a second rule: nothing sees either lock between the two writes. Two words cannot be swapped by one compare-and-swap on every target, so the pair takes the locks, in D19’s order — and a value such a door names keeps the mutex rather than becoming a word, because a retry cannot be held. The word shape is not a door over several locks, so a program that reached one with it would not compile rather than race. Two locks at a time; NK1124 refuses a door handed something that is not a lock, one lock where two are wanted, or a block that does not name one value per lock.

D19 — The order is by address, decided at run time, and the names are bare.

std sorts the locks by address, so access_all(a, b) in one task and access_all(b, a) in another take them alike, and no cycle can form. Two locks need not hold the same type or have got the same shape. The names stand beside println, without a use — ADR-313 D5 gives the reason.

What leaves a lock

D20 — Assigning to a SharedMut directly is NK2204, and the message names the door with the value in it.

kasse = 42 is refused with write kasse.set(42): the repair is mechanical, and “use a door” would leave the reader to pick one of four. It fires where the target is a name.

D21 — What cannot be quoted back is not quoted.

An expression has no span (ADR-081 D2), so a help line rebuilds a literal, a name and a negation and writes an ellipsis for anything else. A help line that quoted the wrong thing would be worse than one that quotes nothing.

D22 — What a lock hands out is Seen[T], and the emitter erases it.

kasse.get() is a Seen[i64]; so is what access and access_all compute. Seen[T] is a type in the checker and in the ledger’s type language (Part III 13.5), and not in the language below: no counter, no marker, no check at run time, no bytes.

D23 — The stamp sticks, and passes through whatever cannot write it back.

stand + 100, stand > 100, stand.abs() are stamped. A call whose argument is stamped is allowed where the callee’s touches names no lock — it cannot put the value into one — and its result is stamped: f"…", println, fs::write, a response body. A callee whose touches names a lock, or is absent (touches everything, ADR-292), takes a Seen only where its signature says Seen.

D24 — Seen is written at two places and inferred everywhere else.

A struct field that keeps a value read from a lock, because that is where the value outlives the moment it was read; and a parameter of a function that touches a lock, where a stamped value is passed in. Locals, expressions, arguments to lock-free functions and results are inferred.

D25 — A stamped value does not go back into a lock blind: three refusals, and no way around them.

There is no .value, no overwrite, and no word that turns a Seen[T] into a T. b.set(a.get()) is refused too; the form is update_all(a, b) fn(mut x, mut y) { y = x }, which also reads a consistent pair.

D26 — set(neu; after: seen) is the one door for a stamped value, and it is a definition.

kasse.set(neu; after: stand)
// is, by definition,
kasse.update fn(mut v) { if v == stand { v = neu } else { throw Overtaken } }

The witness covers the stored value and the condition alike, so neither NK2205 shape applies. T must compare; the witness is a view; Overtaken is an error like any other and carries nothing, because reading the current value would be a second acquisition. It takes the lock once; on a word it is one compare-and-swap, and on a large value it compares the whole value, which the message says. The lowering’s own name, set_after, written by hand is NK2208: there is one door to the comparison, and so none around the stamp.

D27 — The stamp’s verdict is the same at yes and at no.

A two-line update at no with no pause between the lines would be safe, and is refused all the same: the refusal is about the shape, not the clock (ADR-005 Group B).

What may run while a lock is open

D28 — Taking a lock while a lock is held is refused, always.

Part II 12.3’s “often a compile-time error” becomes always (NK2203): one door opened while another is open, directly, through a chain of calls, or by a scope opened inside the block. With that no program exists in which the two shapes of D4 behave differently.

D29 — “Touches a lock” is a second derived property of a function, propagated over sync’s call graph with the opposite lattice.

One traversal, two lattices: sync is a greatest fixpoint (everyone starts sync), this is a least one (nobody starts touching a lock). An unresolvable call takes the sync claim away and sets this property, so fail-closed lands on the same side for both. A trailing lambda’s body and a scope’s tasks belong to the calling function, because they run during the call; a spawn’s body does not. No from(f) form is needed: the check reads the caller’s own body, where an immediate lambda is visible. Inside update, access, access_all and update_all, a call to anything that carries the property is NK2203. The ledger’s column is locks.

D30 — The property is coarse, and never answers an ordering question.

It says a lock, not which. The precise version needs alias analysis, and then whether a program compiles would depend on whether two handles are provably distinct. It is a different column from ADR-292 D3’s touches, which names a lock per container and is what D10’s ordering rests on.

D31 — For this column, an absent entry means “touches a lock”.

The one inverted key: an absent sync means not sync, and for locks the restrictive answer is the other way round. Reading absence as permission is the polarity ADR-010 D1 forbids. Part III 13.5 states it as a sentence of its own.

D32 — A call into foreign code is judged by what its arguments can reach, by the crossing walk generalised, never copied.

This language has no global mutable data, so foreign code touches only what it reaches. Where no lock is reachable from the arguments, transitively through fields, the call is allowed; otherwise it is NK2503, naming the call, the argument and the field. The walk is contracts::send’s, because it already answers undecided for an empty field list (fs::Mapped), carries a depth limit and a cycle rule — judgements a copy would re-derive wrongly. It extends ADR-303 D7’s first rule to locks.

D33 — A function handed to foreign code may not touch a lock, and the answer comes from its body, never its type.

It closes the callback detour: foreign code, called from inside an open lock, calling back into Nikaia and taking a lock. A function type answers undecided — a lambda is its captures — so this rides on D29’s body walk. A spawned lambda is handed to our own runtime and runs later, so it is outside this rule. D32 and D33 are the two halves of one boundary.

D34 — A type records what reading a value of it touches, in touches.

fs::Mapped says touches = ["file read"]: mapped[i] calls nothing a program wrote, so the fact lives on the type, as iterates does (ADR-025 D6). It is written by hand and never inferred. Silence is not a claim: a type with no touches is not refused on, because what is built on it is a refusal (Part III C.4).

D35 — Reading such a value inside a door is NK2201.

Both shapes of read, a method and an index. The message names the page fault, says why NK2202 (a pause) and NK2203 (a lock) are silent, and hands over the way out: read what the block needs before the door. Part II 12.2’s no I/O while holding locked data has a code for each of its three cases.

The runtime check

D36 — The runtime re-entrancy check is a build option, reentrancy-check in [build], yes or no, yes by default.

Under D28 it cannot fire in a correct compiler; it is self-control of D28, not error handling, and without it a compiler hole shows as a silent hang. For every program that obeys D28 both builds behave identically. It is a guarantee that can be declined (ADR-292 D7), not a debug aid. It lives in the manifest, with no command-line override, because a shipped build that could be changed from the command line is not reproducible; and in [build] rather than the runtime settings, because it changes what the compiler emits. A third spelling is refused, not guessed at. Part I 1.2 names the build options rather than counting them.

D37 — It is a dimension of the build cache and of the compiled std’s own tree.

A switch is a cache-key dimension (ADR-037 D4), which adds one to ADR-021 D5’s enumeration. And because the check lives in nikaia-std, the word decides what that crate contains: without a tree of its own, a second project would link the first one’s answer (ADR-021 D7).

D38 — Declining it reaches the crossing shape alone.

The mutex shape carries a mark this compiler wrote, and that is what the switch declines. The cheap shape is a RefCell, whose borrow flag notices a re-entrant borrow whatever anyone asks: the language below’s, not this option’s.

5. Consequences

The numbers that decided:

6. What this does not decide

This site is open source. Improve this page.