Status: Superseded by ADR-312 — its D1-D3 are D6-D8 there
Related: ADR-281 (the open half this answers, and the two
ways out it set down), ADR-005 §1 Group B (the uniform-verdict rule
this keeps rather than bends), ADR-037 D6 (whose “no type answers
may not” this ends), ADR-038 D7 (the foreign-thread rule D3
applies), ADR-042 D1 and D2 (the borrow that makes the alternative
to D3 writable).
ADR-281 D4 kept one lock implementation per setting, and §3 of that
record wrote down what it had not: a lock’s implementation follows
user_parallelism, the crossing verdict may not consult the switch, so the
verdict takes the worse of the two settings and answers may not. A
SharedMut[T] therefore cannot be handed to a task, and Part II 12.2’s
counter — the program user_parallelism = yes exists to serve — cannot be
written.
The sharp form of it: at 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 is entirely safe, and it is refused on account of an implementation that
does not occur in it.
§3 set down two ways out. This is the first.
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”. There are two destinations and each gets an answer that is the same at both settings, which is the whole of what ADR-005 §1 Group B asks — its own note already says “‘At every setting’ is a claim about the verdict, not about the severity.” The justification may differ per setting; the answer may not.
At user_parallelism = yes a real operating-system lock is underneath, and
several threads are what it is for. At no the task is interleaved on the same
thread, so nothing crosses at all. Two different reasons, both sound, one answer.
The duplicated handle is the occasion for the question and not the answer to it. Two handles mean two places at one lock (ADR-040 D1). The owner count plays no part: it is the robust kind at both settings since ADR-037 D6. This is about the lock and nothing else.
With D2, 12.2’s counter is writable. That was the point.
This is deliberately the worse answer, and the record says so rather than implying a proof.
Strictly, at user_parallelism = yes it would be safe: a real lock is underneath
and a foreign thread may touch one. So here the answer really does depend on the
switch — and the cautious one is taken anyway, because the rule of equal verdicts
would otherwise break for this case. Anyone who trips over this in two years
should see that it was chosen.
What happens instead, and is untouched: the caller opens the lock and passes the inner value in. The foreign function sees an ordinary number or connection and no lock at all — the same shape already settled for ordinary functions (ADR-042 D1, D2, Part I 6.2).
The cost was first estimated as near zero on the grounds that the Rust type would differ per setting while a Rust library has one signature — so the case would barely be writable. The measurement moves that argument, and the conclusion survives it.
The count half does not depend on the switch. A handle handed to a call
nothing describes is forced to the atomic count, and --sharing says why:
atomic `db` (Shared[Conn])
could not decide: nothing written down describes `fremd::irgendwas`,
so this compiler cannot see the end of it - and starting a thread of
its own is among the things it may do (ADR-038 D7)So a Shared[T] that reaches foreign code is Arc<T> at both settings, and
for that type the foreign case is perfectly writable.
The lock half does. SharedMut[T] is a count around a lock, and the lock is
what follows user_parallelism (Part II 12.2). At a foreign call it is therefore
Arc<Mutex<T>> at yes and Arc<RefCell<T>> at no. A Rust library has one
signature, so it matches at most one setting — and a library written against the
yes form would compile at yes and fail at no.
So D3’s restriction is not empty; it is exactly reachable, and exactly the asymmetry ADR-005 §1 Group B exists to prevent. Refusing at both settings is what keeps a library written at one usable at the other. The argument rests on the lock alone, which is also the only thing the crossing question was ever about.
Part II 12.2’s counter becomes writable, and ADR-281’s open
half is answered rather than left standing. The second way out it named — one
implementation, the Mutex floor under another name — is not taken, and the
measurement that priced it is unchanged.
ADR-037 D6’s coda ends. It said that after it “no type answers
may not: NK2501 and NK2502 are built and fire on no program this language
can write”, and named the lock as the arm’s candidate. Under D3 the lock answers
may not at a foreign call, so the arm has its occupant — but under D2 it answers
may into a task, so NK2501 and NK2502 no longer share one verdict. Part III
C.5’s “built, and no program reaches it” goes with it.
ADR-005 §1 Group B is kept, not bent. Its rule is that the verdict may not consult the switch; D1 gives two verdicts, each switch-independent, and its own note about severity already draws the distinction D1 relies on.
What it costs in the compiler, from the check that was done when §3 was
written. crosses_into_a_task and crosses_into_an_unseen_call are already two
call sites with separately recorded polarities, both asking one verdict function
that does not know which of them called it — so D1 is that function learning the
destination. The debt is the one contracts::send’s own header wrote down: its
tables require every name to be safe both to move to another thread and to be
looked at from one, and say that the day a name belongs in one column and not
the other a second column is needed. This is that day. And contracts::order asks
the same function about a signature’s result for ordering, which is a third
destination D1 does not answer by itself.
All three predate this record and none is about the destination.
Part III 15.2 promises crate metadata the compiler does not read. Its
“Thread Safety (Send/Sync)” block says “The compiler reads the metadata of the
Rust Crate”, that a Send Rust type is allowed in a spawn task, and quotes an
error about Rc<i32>. No crate metadata is read: a foreign call is one no ledger
describes, and the verdict is taken on the argument’s Nikaia type. The section’s
Status note covers the lock rule and not this claim, so the claim stands
unmarked.
And the same section’s type mapping has no shared entry. It maps i32,
String and Option<T> and stops, so nothing written down says which Rust type a
Shared[T] is at a boundary — which is the type §3’s whole argument turns on.
Part III 15.3 says a single-threaded build generates no atomic operations.
“the compiler does not generate OS-level mutexes or atomic operations in this
mode” has been false since ADR-037 D6 made the owner count atomic
at both settings, and the measurement in §3 shows a foreign call forcing Arc
whatever the setting.
All three decisions. contracts::send::crossing takes a Destination —
Ours for a task of our own and for the closure statement overlapping builds,
Foreign for a call nothing written down describes — and the parameter is
threaded through the walk rather than asked before it, because a lock four fields
deep is still a lock. It reaches exactly one row of the table: every other name
answers the same wherever the value is going, which a test asserts by comparing
the two answers.
Locked and SharedMut are that row. Into Ours they are answered by what
they hold, like a container — a lock makes nothing crossable that was not, which
is Group B’s transitivity and not an exception to it. Into Foreign they are
refused. So NK2501 now refuses nothing a Nikaia program can write and NK2502
has the occupant ADR-037 D6’s coda named, which is §4’s prediction
coming true in both halves.
The third call site took Ours, and that was a decision this record did not
make for it: contracts::order asks the verdict about a signature’s result,
because overlapping two statements puts each inside a closure that hands its
value back. That closure is this compiler’s own, on this compiler’s own thread,
so it is the destination D2 is about. A probe::held() pair overlaps now where it
kept its place before.
Part II 12.2’s counter is writable, which was the point, and the test is the
program that record names: a Shared[Locked[i32]] captured by a spawn passes,
and the same value handed to fremd::irgendwas is NK2502 with D3’s way out —
open the lock, hand over the value inside it.
§4’s debt came due and the second column was the destination. That section
said contracts::send’s tables require every name to be safe both to move to
another thread and to be looked at from one, and that the day a name belonged in
one column and not the other the file would need two. A lock is exactly that name:
at user_parallelism = no it may be moved and may not be looked at. It never has
to be asked that way, because both destinations answer before the distinction
matters — into our own code the lock may go whichever of the two it is doing, and
into code nothing describes it may do neither. So the columns stay one and the
table splits by destination instead. send.rs’s header says so where the
prediction was written.
And the type is built now too (ADR-281), so D2 is a sentence
about programs rather than about a verdict waiting for something to be true of.
A lock handed to a task compiles and runs — and at user_parallelism = yes, since
ADR-055 §6 step 1’s second half, a task is a thread, so “several
threads are what it is for” is what actually happens: four tasks bumping one
SharedMut[i64] 2 500 times each print 10 000, and the same program prints the
same number at no. a_lock_shared_by_four_tasks_counts_every_increment in
tests/shared.rs is that program, and it is the one neither half could run
alone.
§5’s three findings are untouched, as that section says they would be: Part III 15.2 still promises crate metadata nothing reads, its type mapping still has no shared entry, and 15.3 still says a single-threaded build generates no atomic operations.