Locked[T] Is Decided Per Value, Not Per Build SettingStatus: Superseded by ADR-281 — its D1-D3 are D5-D7 there, and D4 is D9
Supersedes: Part II 12.2’s per-setting split (“similar to a RefCell with a
reentrancy check” at no, “a real OS-level Mutex” at yes), which is the
normative sentence this displaces
Related: ADR-037 D6 and D7 (the count: an atomic floor with a
per-value optimisation on top — the shape this copies), ADR-039 D8
(the re-entrancy check as a build switch), ADR-005 D6 (access
takes a sync lambda at every setting — the rule this does not touch),
mutex-floor.md (the measurements)
Locked[T] cannot be emitted. Everything behind it waits on one question — what
it is in the machine — and Part II 12.2 answers that per build setting: a
cheap borrow flag at user_parallelism = no, an OS mutex at yes.
Per setting is what blocks it. A value’s ability to cross a thread then depends on
the switch of whoever builds the program, not on the program, so a library
cannot know across its own boundary what its type is. And Arc<RefCell<T>> is not
Send: under the cheap shape a Shared[Locked[T]] cannot cross at all.
The investigation in mutex-floor.md put the obvious
alternative — an OS mutex everywhere, a lower bound under both settings — and
measured it: 11.3 ns per acquisition at no with no system call, against
Shared[Locked[T]] becoming crossable at all.
Both answers are wrong in the same way. Per setting decides a property of a
value somewhere other than where the value is. A lower bound under both settings
charges every value for a capability almost none of them use — and at no it
charges exactly what the switch exists to save, which makes it the switch working
against itself.
And there is a third answer that was already in the building. The reference
count asks this question per value today, and answers it. ADR-037 D6 makes the
atomic count the floor; D7 lets contracts::sharing lower a particular value to a
plain count where it proves nothing crosses a thread with it. Run, on one
program with user_parallelism = yes:
atomic `crossing` crosses: a `spawn` body uses it, and a task runs on a thread of its own
plain `local` nothing crosses a thread with it, so the count is loweredlet crossing: std::sync::Arc<Conn> = …
let local: std::rc::Rc<Conn> = …
let t = nikaia_std::task::TaskHandle::start(async move { crossing.id });Two values of one written type, two shapes, one program, compiled and run. The question this record asks is already asked and already answered — for the count.
Where it is not proved that nothing crosses a thread with a value, that value’s
Locked is the OS mutex. This is ADR-037 D6’s polarity and it is
not negotiable for the same reason: being wrong towards the mutex costs
nanoseconds, being wrong towards the flag costs correctness.
user_parallelism = no, every Locked 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 is not the user’s and
cannot reach a user lock — rt::worker’s Op carries no closure, and
on_io_worker() asserts the boundary at every public entry of rt::io
(mutex-floor.md §2.1).
So at no the mutex buys nothing and costs 11.3 ns per acquisition — which is
what the switch exists to save. And it keeps a diagnostic: re-entering one
lock is the only failure reachable at no, the cheap shape says so and the mutex
hangs for ever without saying anything, taking ADR-006 D5’s shutdown
deadline with it.
user_parallelism = yes, it is decided per value, by the analysis that already decides the count.A Locked is only reachable from two places through a shared handle, so the
answer contracts::sharing gives that handle is the answer for the lock inside
it. One analysis, two decisions, no second pass — and every one of its seven
named reasons to decline carries over unchanged.
Rc and Arc differ in cost and in nothing else, which is what makes a per-value
choice invisible to a reader. A borrow flag and a mutex do not: one says so
when a program re-enters a lock, the other hangs. Two behaviours for one written
type, picked by an analysis the reader cannot see, would be worse than either
thing this record replaces.
So the mutex shape carries an owner check — measured at +2.0 ns, ×1.15
(mutex-floor.md §4.3) — and re-entering says the same
thing whichever shape a value got. One behaviour, two prices.
Under ADR-039 D8 that check is a build switch, on by default, and
its role is unchanged here: self-control of a rule, not error handling. D2 makes
it free at no, and D3 makes it fall only on the values that actually cross, so
the set it is paid on is smaller than the switch has ever had to cover.
sync and may block
(ADR-006 D6), and ADR-005 D6’s gate sits on the
lambda rather than on the acquisition. This record leaves that gate alone.Locked[T] outside a Shared is. It has one owner, so nothing
can contend it; it takes the floor today because the analysis has no entry for
it, which is safe and wasteful. Left until a program makes the answer obvious.SharedMut[T] spells Shared[Locked[T]]. That is
ADR-039’s, and both spellings lower through this.The seed list carries twice the weight. contracts::sharing’s own words:
“every crossing is a seed, and a missed seed is unsoundness rather than a missed
optimisation”. Hanging the lock on the same answer means that list must be right
for two things. It has already learnt once — the overlap the compiler itself
chooses became a seed when it became one — and since spawn lowers, the crossing
side can finally be exercised end to end rather than reasoned about.
And one normative sentence is displaced, which is why this is a record and not a patch: Part II 12.2 decides both settings in plain words and no ADR did.
The shape, end to end. Not the surface it is reached through.
Built:
nikaia_std::lock carries both shapes behind one surface — Local on a
borrow flag, Crossing on a mutex with the owner check — and they report
the same thing when a program re-enters one lock, which is D4. Tested three
ways, including four threads on one Crossing, which is the capability the
cheap shape cannot have.sharing::lock_name answers from the count, and emit::written_name writes
it. The count already rides down through a type’s arguments, so
Shared[Locked[T]] asks one question once — D3, at no new cost.user_parallelism = no the cheap shape, always, whatever the count says —
D2.Locked::new any
more than there is a Shared::new. check::becomes_shared peels one lock, in
that order, so a value that is already a lock is never wrapped twice.std.contracts describes Locked::access with sync = "from(f)" — the entry
mutex-floor.md §3.1 found was missing, and what makes
Part II 12.2’s own idiom sync.Locked in a relayed message, like every
other substituted name (ADR-056 D1) — and a message naming both
at once is caught by that record’s comparison rather than by a rule of this
one.Not built, and each is named rather than left to be found:
yes yet. The
analysis declines with “it comes from an expression this analysis does not
follow”: let c: Shared[Locked[T]] = value is an allocation the checker now
records and contracts::sharing does not, so every such value falls to the
floor. D3 is correct and currently conservative in the safe direction; the fix
is the same extension in the analysis that becomes_shared got in the checker.access hands its lambda. Part II 12.2 writes
counter.access fn(n) { n + 1 }, and n is a &mut T below, so the body does
not compile as written. That is a question about the language’s surface and not
about this decision, and inventing an answer here is how a surface gets one
nobody chose.Locked[T] outside a Shared. §3 leaves it; the emitter writes the
floor for it, which is safe.