Status: Superseded by ADR-281 — its D1 is D4 there, D2-D7 are D28-D33, D8 is D36-D37, D9 is D1 and D3, and D10 is D10, D20 and D25
Related: ADR-005 D6 (the sentence D2 displaces, and the
Send check D6 extends), ADR-037 D3 (this answers its second
half, which ADR-037 D7 left open), ADR-027
(the propagation D3 reuses), ADR-010 D1 (the polarity D5 turns
around for one column), ADR-029 D3 (the bound D3 does not need,
and why), ADR-033 D8 (the precedent for D8’s switch, and the switch its
count left out), ADR-021 D5 (whose cache-key enumeration D8 adds
a dimension to), ADR-033 D2 (the touch vocabulary D4 must not be
mistaken for),
ADR-038 D7 (the foreign-thread rule D6 extends),
ADR-028 (whose division of labour decides where D3’s answers come
from), ADR-006 D2 (whose “for free” composition D10 replaces with
a stronger sentence). Evidence: docs/mutex-floor.md,
docs/history/rc-or-arc.md.
This record was opened to decide one thing — whether Locked[T] keeps two
implementations, one per user_parallelism, or gets a single Mutex floor — and
it closes as something else. It is a build order for a type no Nikaia program
can write today. Saying that plainly is part of the record, because the
question as posed assumed a type that exists.
The probe that settled it:
let kasse: Shared[Locked[i32]] = Shared::new(Locked::new(0))Four errors — cannot find type 'Shared' in this scope, cannot find type
'Locked' in this scope, and twice use of undeclared type. nikaia-std carries
three type entries in its ledger (cli::Args, fs::Mapped, io::Lines) and
neither of these is among them; the emitter has no lowering for either; the
checker does not know the names.
What is built is the reasoning above them. contracts::send lists Shared
among the container names its crossing walk recognises, and contracts::sharing
infers which count each Shared position gets (ADR-037 D7, D8).
So the analysis of these types is built and the types are not — which is also
why no measurement of a floor could say anything about behaviour: there was
nothing to behave.
The measurement did settle three things, and none of them was the question.
Blocking is not pausing, and the specification had already chosen: the panic hook
must be sync and Part I 7.2 permits it to block, which makes a lock
acquisition not a suspension point. access stays sync through
ADR-029 D3’s from(f), which turns on one ledger line and never on
the primitive. And the floor’s price is 11.3 ns an uncontended acquisition, no
syscall, a smaller value than the alternative, with contention unreachable at
user_parallelism = no.
The two implementations differ in two things a program can see: re-entering the same lock panics under one and hangs under the other, and a panic inside the guard poisons under one and not the other. That is the real objection to keeping both, and it is answered by making the programs that could observe it impossible (D2) rather than by buying the difference away for 11.3 ns on every acquisition in every program.
Checks belong in compile time. Where one does not fit in the compiler this record says so; it does not cover the gap with nanoseconds.
Two arguments that were made for the floor and do not hold:
Crossing — and this argument was dismissed on a false premise, corrected
here. A floor was argued to make Shared[Locked[T]] movable across threads at
all, and that was answered: at user_parallelism = yes the lock is already a
real OS lock, so everything already travels there, leaving only the narrow case
of handing a value to a foreign Rust library at no.
The answer was wrong, and so the dismissal was. The verdict does not look at
the implementation this build uses. For a type whose implementation follows the
switch it takes the worse of the two settings (ADR-037 D6) — so
nothing travels at yes either, and a floor would in fact make the type
crossable. What it buys is therefore not a narrow foreign-library case. It is
Part II 12.2’s counter, at the setting that exists for it. §3 states that as the
open half of this record rather than as a settled cost.
The 11.3 ns is still 11.3 ns, and it is still paid at the setting where it unlocks nothing. What changed is the other side of the comparison.
Poisoning. Making a panic poison at both settings was argued to follow from
D1’s motive. It does not: at no a panic is a process abort (Part III, appendix
A.2), so nobody survives for whom poisoning would be done. The difference in
panic behaviour between the settings exists for a reason unrelated to locks, and
no normative sentence changes for it.
Keeping both representations also keeps NK2501/NK2502 a candidate: the lock
stays non-crossable at no, so the two codes keep the occupant they would
otherwise never have had.
And that has a consequence this decision did not record, which §3 now states
as an open question rather than leaving it to be discovered. A lock that may
not cross cannot be handed to a task, so Part II 12.2’s counter — the program
user_parallelism = yes exists to serve — cannot be written. D1 is not wrong
about the 11.3 ns; it is incomplete about what the 11.3 ns was buying.
Part II 12.3 already calls manual nesting an anti-pattern and “often a compile-time error”. “Often” becomes “always.” With that, no program exists in which the two representations of D1 can behave differently, because the one behaviour that distinguishes them cannot occur.
This displaces two sentences that say the opposite, and they are the reason this is a decision and not a sharpening:
sync calls — but well-formed code never triggers them.”
That sentence asserts the case is not refused statically. It is now.sync does not rule out reentrant access on
the same lock through a chain of sync calls.” True of sync alone, and the
displaced claim: something else rules it out now.sync and with the opposite lattice.Inside any of D10’s blocking doors, calling anything whose property is set is refused. That catches chains and self-calls, which is what D2 needs to be complete rather than local.
It is one traversal and two lattices, not a second pass. The call graph
contracts::sync builds already answers three questions it would be expensive
to get right twice: a method call is resolved by the type checker and not by a
second resolver in this file (ADR-028); a trailing lambda’s body
belongs to the function that writes it, because it runs during the call; and
spawn’s body does not, because it runs later and elsewhere (Part I 5.4).
The difference is the direction:
| starts from | rule | |
|---|---|---|
sync |
everyone is sync |
greatest fixpoint — take the claim from whoever reaches a non-holder |
| touches a lock | nobody touches one | least fixpoint — give the property to whoever reaches a holder |
That is why mutual recursion between pure functions keeps sync
(ADR-027 D1) and correctly gets nothing here, for the mirrored
reason. Fail-closed lands on the same side in both: an unresolvable call takes
the sync claim away and sets this property, so one polarity decision serves
both.
A scope’s tasks propagate upward; a spawned task does not. A scope waits for
its tasks, so they run during the call and their bodies belong to the surrounding
function, for the same reason a trailing lambda’s body does. The consequence is
intended: opening a scope inside an open lock is refused, because the task waits
for the lock and the holder waits for the end of the scope, and that is a real
deadlock rather than a precaution. A task started with spawn runs later and
elsewhere, so taking a lock in one is the ordinary case.
This column needs no from(f), and the reason bounds it.
ADR-029 D3 gives sync a fourth state because a ledger entry for
map must answer a question whose answer is in the caller’s lambda. Here the
check runs on the caller’s own body, where the walk already sees that lambda —
so what sync had to summarise in an entry, this reads directly. The premise is
stated so that it is visible if it is wrong: it holds exactly while the lambda is
immediate. A lambda the callee stores — so that it may run while a lock is
open somewhere this walk cannot see — is D7’s case. A lambda the callee
spawns is neither: it runs later and elsewhere, so the sentence above about
spawn is the whole of it.
It says “a lock”, not “which lock”. The precise version needs alias analysis, and the cost of that is not compile time: whether a program compiles would depend on whether two handles are provably distinct, so an unrelated line elsewhere could make unchanged code stop compiling. That is a worse failure than a refusal a programmer can read.
So this is a different column from ADR-033 D2’s touches,
which names a lock per container because Part I 8.1.1 promises “which file,
which socket, which lock”. touches answers whether two operations are ordered;
this answers whether a call may appear inside an open lock. Part II 12.2’s rule
that two accesses to the same lock keep their order rests on the first, and must
never be re-derived from this one, which cannot tell two locks apart.
If the coarse rule hurts in real programs, touches is the home for the precise
version. Not now.
sync, written out where a reader would apply sync’s rule.Part III 13.5 states, as a rule about that file, “An absent sync therefore
means not sync” — safe there, because absent lands on the restrictive answer.
For this column absent would land on permission, and an entry nobody wrote would
be a hole through which every rule in this record falls. Reading the absence of
an answer as a yes is the polarity ADR-010 D1 forbids.
This is a sentence of its own in 13.5, beside the general rule, not a footnote.
Foreign code can only touch what it reaches, and this language has no global mutable data. So if no lock is reachable from the arguments — transitively, through structs — the call is allowed, silently. Otherwise it is refused. This extends ADR-038 D7’s first rule to locks and displaces nothing there.
Generalising rather than copying is the decision, not an implementation
preference, and one case shows why. fs::Mapped has a ledger entry with an
empty field list, because its fields are Rust. Read structurally that is
“nothing reachable”, and “allowed silently” would have had a hole at exactly that
shape. contracts::send’s walk already gets it right — an empty field list
answers undecided, which is the fail-closed arm, because a type with no fields
recorded is not a type with no fields. The walk carries three more such
judgements: a depth limit against a type that holds itself through a container, a
cycle rule, and the arm D7 is about. A copy re-derives four subtleties and one of
them is re-derived wrongly.
(Corrected on first use. This decision was first written as “a function handed
outward”, which read as forbidding what D3 calls ordinary: a spawned
lambda is handed outward and may take a lock. The rule exists to close the
callback detour — foreign code, called from inside an open lock, calling
back into Nikaia and taking a lock — so D6’s boundary is its scope. A spawned
task is handed to our own runtime and runs later, so it cannot be inside an open
lock, and D3’s sentence stands unchanged.)
The same property as D3, and it is worth being exact about where it comes from:
contracts::send’s walk answers undecided for a function type, because a
lambda is its captures and nothing writes those down. The walk says so honestly,
which means the type can never answer this question. So this rides on D3’s body
walk: a lookup for a named function, the same walk for a lambda.
D6 and D7 are the two halves of one boundary. D6 asks what a foreign call’s
arguments can reach and has nothing to say about a function among them, because
the walk honestly answers undecided there; D7 is that missing answer. Neither
reaches past the foreign call, which is why D3’s spawn sentence is untouched by
both.
Today this is narrow, and the reason is in the specification: Nikaia’s type
grammar has no function type, so no source program declares a parameter of that
shape (Part I 5.4, Part III 13.5). It covers a lambda written at a foreign call
site and std’s own detached entries, enforced the way ADR-029 D4 is enforced — by
walking the entries rather than trusting them. It widens the day the type grammar
gains a function type.
Part I 1.2 says “What you choose when you build is how, never what, and there are exactly two things to choose.” The principle is untouched and is this switch’s own guarantee: for every program that satisfies D2, both builds behave identically. The switch decides only whether a violation is noticed.
(Corrected on first use. This decision was first written as a third switch,
making the count “three”. That was wrong by its own argument: the same paragraph
observed that ordering lives in [build] uncounted
(ADR-033 D8), which makes the answer four and not three. So
Part I 1.2 stops counting and names them instead — target,
user_parallelism, ordering and this one — because a count that has been
wrong twice reads as a promise nobody maintains. ordering gains the
subsection it never had there. cleanup-deadline is not among them: the
manifest still accepts the key and the compiler no longer reads it
(ADR-038 D5).)
Under D2 the check cannot fire in a correct compiler, and that is its new role:
self-control of D2’s rule, not error handling. No input can trigger it; if it
fires, the compiler has a hole. Without it such a hole appears as a silent hang
and, at no, as a stopped cleanup deadline (ADR-006 D5).
It is not named “debug” and is not a development aid to be removed later. It is a guarantee that can be declined, which is ADR-033 D8’s precedent: “A semantic default that cannot be switched off is a decision imposed rather than offered.” It lives in the manifest rather than on the command line only, because otherwise a shipped build is not reproducible, and it is a cache-key dimension like the other two (ADR-037 D4).
It belongs in the manifest’s [build] and not in the runtime settings file,
and that needs saying because cleanup-deadline moved the other way. The
difference: cleanup-deadline changes what a running program waits for and the
compiler need not know it, while this switch changes what the compiler emits.
A choice the compiler acts on is the compiler’s to read.
It also sits inside ADR-037 D7’s rule — what is observable is written, what is not is inferred, with safe as the floor. Under D2 a re-entrant acquisition is not observable in a correct program, so nothing observable is being switched.
SharedMut[T], from the start. Locked[T] stays, with its own use.Two wrappers are Rust’s shape and a wart there. The combination is the normal
case, so the normal case gets the short name and the exception gets the long one.
This is not a rename: nothing exists to rename, so there is no body of code
to split in half, and SharedMut is simply what the type is called. The short
form is a deliberate departure from this language’s habit of spelling words out —
for its most common type, SharedMutable is too long.
Locked[T] stays because it has a second real use: individually locked fields
inside a shared structure. What disappears is the hand-written nesting.
Part I 6.2 defines Locked[T] by that nesting — “Allows data inside a
Shared container to be modified”. Since Locked keeps the second use, that
definition is wrong as written rather than merely incomplete, and the
rewrite belongs to this decision.
One thing this gets for free: Part III 13.5 records a parameter’s type in the ledger as the source writes it, so a ledger entry is user-visible. With one name from the start there is no internal spelling that could appear in a diagnostic, a printed type, or an entry.
Today every access goes through the door that carries every rule. Three of the four need none of them.
| form | for | block may wait |
|---|---|---|
kasse.get() |
taking a copy out | — |
kasse.set(value) |
replacing, value computed outside | yes, outside |
kasse.update fn(mut v) { v += 100 } |
changing it, under the lock | no |
kasse.access fn(state) { … } |
in place, large values | no |
set needs no block because arguments are evaluated before the call: the lock is
open for the duration of one store. update hands the block the value as mut v — a copy
where the value is a word, the address otherwise, which is the compiler’s by type
(ADR-110 D2) — and the block returns nothing. access stays for everything
where copying is too expensive — a list of ten thousand entries is not copied to
append one.
The derivation this breaks, and the stronger one that replaces it. Part II
12.2 reasons: the lambda is sync, therefore nothing can fall due while the lock
is held — and ADR-006 D2 calls that composition free. set has no
lambda. The replacement is not a patch but a stronger sentence: while the lock
is open in get and set, no user code runs at all, so there is nothing that
could fall due. One sentence instead of a derivation.
get is a read; set, update and access are writes. Part II 12.2 says
two accesses to the same lock keep their order, and that sentence was written
when access was the only door and therefore had to count as a write. Under
ADR-033 D2 two reads of one resource are unordered, so two gets
are unordered and the three writing forms stay ordered. A refinement to be
written down, not a conflict.
Two refusals come with the doors: assigning to a SharedMut directly is
refused and names set, and a set whose argument contains a get on the
same container is refused and names update. The second reads the stamp a
value carries out of a lock (ADR-111), so it catches the pair
spread over two lines and over two functions as well as the one written inline.
D1 keeps one implementation per setting. The crossing verdict may not consult
the switch, so for a type whose implementation follows it the verdict takes the
worse of the two settings (ADR-037 D6) — may not cross. A
SharedMut[T] holds a lock, so it cannot be captured by a spawn, and the
shared counter of Part II 12.2 has no second task to reach.
The sharpest form, and it is sharper than a cost. At user_parallelism = yes
the cheap implementation is not built at all. What stands in the emitted
program is a real operating-system lock, under which that counter would be
entirely safe. It is refused on account of an implementation that does not occur
in that program. With the switch turned on, the compiler prevents the one thing
the setting exists for.
Two ways out. Neither is taken here.
A — the verdict takes the destination, and the portability rule costs nothing. What is judged stops being “may this type be on a foreign thread in the worst case” and becomes “may this value go to this destination“. Both answers are switch-independent:
| destination | answer | why, at no and at yes |
|---|---|---|
| a task of our own | may | at yes the lock is an OS lock and holds; at no nothing crosses, because no code of the user’s runs concurrently (ADR-037 D2) |
| foreign code whose end this compiler cannot see | may not | a foreign runtime’s threads are not bound by a switch over our code (ADR-038 D7) |
The verdict is therefore the same at both settings for each destination, which is the whole of what ADR-005 §1 Group B asks — that note already says “‘At every setting’ is a claim about the verdict, not about the severity.” The justification differs per setting; the answer does not. So A displaces no record.
A does not fail on the verdict machinery, and that is checked rather than
assumed. The two destinations are already two call sites in check:
crosses_into_a_task raises NK2501, crosses_into_an_unseen_call raises
NK2502, their polarities are already recorded separately in Part III C.3, and
both ask the same send::crossing(ty, own, library) and then only whether it
refused. The destination is already known where the question is asked; what is
shared is the one verdict function. A is that function learning the destination.
What A does cost, named so it is not discovered later:
contracts::send already wrote down. Its header requires every name
in PLAIN and CONTAINERS to be safe both to move to another thread and
to be looked at from one, and says: “The day a name belongs in one column
and not the other, this needs a second column; stating that here is cheaper
than discovering it.” A destination-dependent answer is that day. The cost was
predicted; A pays it.contracts::order asks
crossing of a signature’s result type to decide ordering. Which destination
an overlap boundary counts as is the one question A does not answer by itself.B — one implementation after all, which is the Mutex floor under another
name. The price is paid at no, the setting where it unlocks nothing, because
there is no second thread there to be a destination. Uniformity instead of
capability.
And the question that would have to be asked before B: does the cheap
implementation need a full lock to be shareable, or would a flag of atomic
instructions that refuses on conflict instead of waiting do? The measurement
behind this record answers it without new work — an uncontended lock is one
atomic and a branch, with zero futex calls in a million acquisitions. A
conflict-refusing flag needs the same atomic, so B does not get cheaper by being
weaker; and under D2 a conflict cannot arise at no at all, so its refusing
branch would be dead code. B stays where the measurement put it.
What this displaces. Part II 12.3’s “often” (D2); Part II 12.2’s safety-net
sentence (D2); ADR-005 D6’s last sentence (D2); Part I 1.2’s
“exactly two” — which D8’s own correction replaces with a named list rather than a larger number; Part I 6.2’s definition of Locked[T]
(D9); Part II 12.2’s sync-lambda derivation and ADR-006 D2’s
“for free”, both replaced by a stronger sentence (D10).
What it does not displace. ADR-037 D3’s second half is
answered, which D7 of that record explicitly left open. ADR-038
D7’s first rule is extended to locks. ADR-005 Group B needs
nothing: a crossing into a task at user_parallelism = no is already reported as
a lint rather than refused, so a spawned task taking a SharedMut is the
ordinary case there too.
What it costs. The type does not exist. Beside the analysis in D3–D7 this
needs SharedMut[T] and Locked[T] as types the checker knows and the emitter
lowers, their four doors, and the std entries behind them. Roughly thirty
normative sentences become incomplete, fourteen code and table sites and nine
Status notes need rewriting, and the diagnostics appendix needs codes for D2,
D10’s two refusals and D6’s refusal. That is follow-on work, not a second
decision.
A retry instead of a lock is ADR-110 D3: an update block
may run more than once, because sync says it does not wait, the touches
column (ADR-067 D1) says it takes nothing else, and its captures
are views — and the compiler uses that where the value is a word.
Nothing in this record is built. SharedMut does not exist, Locked does
not exist, neither does any of the four doors, and no check refuses D2’s nesting.
What exists is the probe in §1 and the measurement behind D1, and the machinery
D3 and D6 are to be built on: contracts::sync’s call graph and fixpoint, and
contracts::send’s structural walk.