Shared Does Not Go Into Code Nothing Describes, So at One User Thread Its Count Is PlainStatus: Superseded by ADR-312 — its D1-D3 are D9-D11 there Narrows: ADR-037 D6, which made the atomic count the floor at both settings Related: ADR-045 D1 (the destination, and the verdict this does not touch), ADR-037 D7 (the per-value inference that made D1 here necessary), ADR-281 D6 (the same rule for the lock, decided first)
ADR-037 D6 made the atomic count the floor at both settings, and its
reason is one sentence: a Shared whose expansion moved with the switch had to be
refused a thread crossing at both settings — the verdict is about a type and
may never consult the switch — and that made Part II 12.2’s counter, the program
the switch exists to serve, unwritable. One representation bought the crossing
back for a measured +9 ns per clone-and-drop pair.
That was right, and two things have happened since.
D7’s per-value inference is built. Which count a particular value gets is
decided by contracts::sharing, and at user_parallelism = yes it works — run:
one value a task uses comes out Arc, one that stays home comes out Rc, in one
program.
And ADR-281 decided the same question for the lock the other way.
At one user thread every lock is the cheap shape, because nothing a user writes can
cross there: one user thread (ADR-037 D2), and the runtime’s I/O
thread carries no user code — rt::worker’s Op has three variants and none
carries a closure.
What came out of the two together is a shape that is never right. Measured, on
a program at no:
let c: std::sync::Arc<nikaia_std::lock::Local<i64>> = …An atomic count around a non-atomic lock. Either the value can cross a thread — and then both halves must bear it — or it cannot, and neither needs to. What stands there pays for a capability on one half that the other half forbids.
And one thing kept the cheap count from being unconditional at no. Measured
before deciding:
plain a nothing crosses a thread with it
atomic b `published` is public, so its callers are in a unit this build cannot
see, and one of them may cross a thread with itThat reason does not hold at no for a Nikaia caller: a package is built with
the settings of the program that uses it (ADR-286 D15 rule 4) and, since
ADR-286, as a crate of that same build — so the invisible caller is
at the same setting and cannot cross either. It held for exactly one caller: a
Rust one. contracts::send permits a bare Shared into code nothing
describes, and a Rust library brings threads no switch of ours binds.
Shared may not go into code nothing describes.The same refusal a lock already gets, for the sentence that was already the lock’s
reason: a Rust library has one signature. When D6 made the count atomic
everywhere there was one representation to name and nothing to refuse; D7 brought
the second one back, so a Shared[Conn] is an Rc for one value and an Arc for
another in the same program, and no foreign signature can name both. What
works today works by accident — the analysis forces the atomic count where a value
reaches an undescribed call — and where it does not, rustc refuses in Rust’s
words about a type the program never wrote.
The way out is to pass what is inside, a view or a copy; a foreign library that means to keep a value clones it into a hull of its own anyway.
A bridge type is reserved and not built. A hull whose representation a program
names, for the case where the hull itself must cross, is the answer if a program
shows that passing the contents is not enough. Its name is undecided and would not
be Rc’s or Arc’s: those are the machine’s words, and Part I 2.2 is the list of
this language’s.
user_parallelism = no, every count is plain.Nothing a user writes can cross a thread there, and since D1 there is no way out of the program either. So the seven reasons to decline are reasons to decline a proof about another thread, and there is no other thread to prove anything about.
The verdict is untouched. A Shared[Locked[i32]] may go into a task of ours at
either setting (ADR-045 D1), and no answer this compiler gives about
a type reads the switch. D2 is about what is emitted, not about what is
permitted — which is the distinction D6 could not make, because in 2026 the
emission and the verdict were the same decision.
sharing::infer writes a function’s caller-visible classes into the ledger, and
that is a contract — read by a person and by a later build. It is computed at
the floor whatever the switch says, because a contract that moved with a build
switch is the thing ADR-045 D1 refuses. The emitter asks the same analysis with the
setting in hand; the two are different questions and now have different answers.
Measured, on the program §1 ends with. At no all five positions are plain,
including the public function’s parameter, which was atomic. At yes the same
program is three plain and two atomic — the per-value answer, unchanged.
The floor across files stops being what makes two files agree at no, and they
agree anyway. ADR-037 D8’s ForeignFile row exists because one
file writing Arc and another Rc for one slot is a refusal in Rust’s words. At
no every file of the build is plain, so none can disagree; at yes the floor is
still what makes them agree. The tests that pinned this now assert agreement
rather than atomicity, at both settings.
What it costs: a Shared handed to a Rust function is refused where it was
accepted. No program in this repository does that.
examples/foreign-runtime/, which explains the boundary in terms of the
per-build expansion D6 replaced — “what Shared lowers to at
user_parallelism = no, namely an Rc“. It is stale against D6 and now against
this; #213 carries it.All three. contracts::send refuses Shared at the foreign destination beside
Locked and SharedMut, off one list whose name says what the three have in
common: their representation is chosen rather than written.
sharing::analyse_program takes the setting and flattens every count where nothing
can cross — applied to the finished answer, so one run is one code path at both
settings and the duplication sites, which are about handing a handle on rather than
about threads, are untouched. sharing::infer keeps the floor; the emitter and
--sharing take the setting.