Status: Accepted
Related: ADR-296 D10 (a par_fold with no parallelism is a
sequential fold), ADR-016 D3 (why the compiler’s own threads are
not the user’s), ADR-292 (the overlapping D2 bounds),
ADR-021 D5 (both switches are cache-key dimensions),
ADR-005 §1 Group B and §5.3 (the check D6 changes the input of),
ADR-020 D1 (the ledger D7 adds a column to),
docs/history/rc-or-arc.md (the measurement D6 rests on)
Two questions have to be answered before a program can be built, and they are independent:
std
can offer and what a panic does.Answering them with one switch forces the two to travel together, and they do not: a single-threaded service on a 64-core machine is a real thing to want, and so is a compute job that uses every core it can find.
target names the machine.| target | passed to the backend | threads available |
|---|---|---|
x86_64-linux |
x86_64-unknown-linux-gnu |
yes |
aarch64-linux |
aarch64-unknown-linux-gnu |
yes |
wasm32-unknown |
wasm32-unknown-unknown |
no |
The default is the machine the compiler runs on, where it is one of these, and
the triple is passed to the backend as Cargo’s --target.
The target decides what std can offer — whether fs::map exists at all — and
what a panic does: unwind where the machine unwinds, trap where it traps.
It decides nothing about what a program means. The same source compiles for every target and prints the same bytes, which is asserted by a test over every example rather than promised in prose.
A target the toolchain cannot build for yet fails with what is missing. It never emits code for a different machine.
user_parallelism says whether the user’s code may run concurrently. It is yes or no.Changed by ADR-292 D1 and D6: the compiler overlaps no statements of its own accord; a program asks with overlap, I/O the runtime performs may be in flight at either setting, and what no bounds is the program’s own computation.
| value | meaning |
|---|---|
no (default) |
nothing the user wrote ever runs concurrently |
yes |
it may, and the runtime decides how widely |
Not a count, deliberately. How many threads or cores serve a yes is a
scheduling question, and the answers belong to the machine and the moment: a
number in the source would be a promise the language cannot keep on hardware it
has not seen, and it would have to be re-tuned for every deployment it survives.
The program says what it permits; the runtime says how far it goes.
That also removes a question this would otherwise have owed an answer to. With a
number, a par_iter and the branches of an overlap block would both draw on
it, and something would have to say which yields. With a permission there is
nothing to divide.
What it governs: par_iter, spawn, task::scope, freedom from data races,
the structural Send check’s severity, and whether two computations in an
overlap block (ADR-292) may run at once.
The word user is load-bearing. The compiler is not bound by this switch;
only the program is. fs::map may validate UTF-8 on four cores at
user_parallelism = no, and the runtime may hand a blocking call to a sidecar,
because neither runs code the user wrote and neither is observable — the check
returns the same verdict and the same byte offset on one core and on sixty-four
(ADR-016 D3).
The line is therefore exact and testable:
The compiler may use as many threads as the target has, for as long as no code the user wrote runs concurrently. The moment it does, it is user parallelism and D2 bounds it.
Shared expands from user_parallelism, not from the target.Changed by D6 and D7 here: Shared is an atomic count at both settings, and a value the analysis proves stays on one thread gets a plain one; the switch chooses neither.
Which count a Shared gets is a property of the program, not of the
machine: a program that never runs its own code concurrently cannot race with
itself, whatever the machine underneath could do.
Shared itself stays written by hand. It is not an ownership annotation of the
kind the language refuses — a lifetime annotation changes nothing observable,
and sharing changes when a value is cleaned up (ADR-297).
Inferring it would move a destructor silently.
They change the emitted code, so a key without them would serve one build’s artifact to another (ADR-021 D5 and D7).
They stay out of nikaia.contracts. Borrow structure, tether state, trust
and the error set are identical whatever the machine and whatever runs at once,
so one ledger serves every combination (ADR-005 D8). Anything that
did depend on a switch would double the churn and put a build-time choice into a
file that ships with a package.
(D7’s sharing column belongs in that list and is worth saying so. It is
the one column about a *representation, so it is the one that looks as though it
might depend on a switch — and it does not, because D6 took the representation
off the switch. The analysis never reads user_parallelism, which is the same
sentence §3 says about the Send check’s verdict and for the same reason: an
answer that moved with the switch would make a library built at one setting wrong
at the other.)*
nikaia.toml carries them, because they are properties of a project rather than
of an invocation, and a committed value is one a reviewer sees. --target and
--user-parallelism override for a single build, which is what a benchmark and
a bug hunt need.
Shared expands to an atomic count at both settings. This narrows D3.Shared[T] is an atomic count whatever user_parallelism says, and the rest of
D3 holds — Shared is written by hand, for the reason D3 gives
(sharing changes when a value is cleaned up, ADR-297), and the
verdict of the structural Send check never consults the switch.
The reason is one sentence. A Shared whose expansion moved with the switch
had to be refused a thread crossing at both settings — because the verdict is
about a type and may never consult the switch (ADR-005 §1 Group B,
§5.3) — and that made Part II 12.2’s Shared[Locked[i32]] counter, the program
the switch exists to serve, unwritable; one representation costs a measured
+9 ns per clone-and-drop pair and buys the crossing back.
The atomic is a per-clone cost and not a per-use one; the expensive case is the contended one, an order of magnitude, and no choice can avoid it: a count several threads touch has to be atomic.
What it costs in the compiler is one row of a table. Shared is in
contracts::send’s container list, not its MayNot case, so it is answered
by what it holds — so Shared[Locked[i32]] is still not permitted to cross,
for the lock’s sake rather than the count’s, and that half is D3’s second
question and is not answered here.
Changed by ADR-312 D9 and ADR-290 D7: the
crossing refusals fire. NK2502 refuses a Shared handed to code nothing
describes, and a value of a described crate’s type that does not cross handed
to a call that may move it; NK2501 refuses such a value in a task.
Shared itself is not what makes a value non-crossable: at both settings its
count can cross, and what it holds decides.
Shared gets is inferred, and the inference may only ever take an atomic away.D6 makes the atomic count the floor. contracts::sharing is an optimisation
on top of it and nothing else:
Where the analysis can prove that nothing crosses a thread with a given value, that value’s count may be a plain one. Where it cannot prove that, the answer stays atomic. It may never add an atomic, and it may never make a program unsafe.
Those last two are the same sentence read from both ends, and the polarity is not negotiable: an atomic count where a plain one would have done costs 9 ns per clone-and-drop pair, while a plain count on a value that crosses is a data race (ADR-010 D1’s rule, on a question where the two directions cost different kinds of thing).
The two files have a contract with each other and it runs one way.
contracts::send answers may for a Shared of crossable data, and that answer
is true only because the count is atomic — so a value this analysis lowers must
not cross. Every crossing is therefore a seed, and a missed seed is
unsoundness rather than a missed optimisation. The seeds are
ADR-005 §5.2’s own enumeration, asked per value rather than per
type. An overlap branch is not one: it is polled on the block’s own thread and
nothing crosses out of it (ADR-292 D4). A Shared whose
allocation the analysis did not watch - one handed back by a call - stays at
the atomic floor for that reason alone.
Nothing new is introduced by it, and that is the argument for building it at all.
sync, throws, touches
and borrows: sharing = ["counts | <result>: plain"] — which of a
function’s Shared positions are one allocation, and which count each class
gets. nikaia.contracts already ships facts read off bodies, so this is a
column and not a mechanism (ADR-020 D1 and D2), and the
union-find that decides a count computes the summary already
(docs/history/rc-or-arc.md §5.1 names it as the summary that
composes). It is also the only column in that file that cannot make a
program wrong: the floor is safe, so an entry that says atomic about
everything describes a correct program that pays 9 ns.nikaia --sharing is an explanation, not a switch — per value, what was
decided and why, in the shape ADR-292 D2 gave --overlaps and
ADR-010 D7 gave --trust. It is what a person reads when they
want the 9 ns back.The rule that decides what is written and what is inferred:
What is observable is written. What is not is inferred, with safe as the floor.
Shared itself is written, because sharing changes when a value is cleaned
up — D3’s own reason, unchanged. Rc against Arc is inferred, because
docs/history/rc-or-arc.md §2 measured that nothing a program can
observe distinguishes them: same handle size, same owner count step for step,
the same cleanup point asserted against a written log, the same answers about
exclusive access and unwrapping. The one real difference — with an atomic count
the last handle may be dropped on another thread, so a Cleanup
(ADR-297) runs there — can only happen to a value that crosses,
which is a value this inference has no freedom about. The two counts differ only
in the case where the analysis has no choice, which is the sharpest form of the
equivalence and the reason the gate D3’s reason would have closed opens instead.
Locked is not decided by this, in either direction. RefCell against
Mutex differs in what a reentrant access does and in what a panic inside one
leaves behind (docs/history/rc-or-arc.md §7), so it is observable, so by the rule
above it is written and not inferred. What an always-Mutex floor would cost
against Part II 12.2 is a separate question and is not answered here.
The companion to D7 would be a way for a programmer to say use a plain count here, I know it does not cross. It is refused, and the reasoning is recorded because it will be proposed again.
Every fallback to atomic is one of two things, and the list is closed and
enumerated by --sharing:
| the fallback | would an override help? |
|---|---|
| handed to a call nothing describes | no — that wants a contract |
| handed to a method nothing describes | no — that wants a contract |
| handed over in an argument position no contract covers | no — that wants a contract |
held by a type whose fields are unrecorded |
no — that wants a contract |
| an origin this analysis cannot see, such as a call it hands back from | no — that wants a contract for the call |
| a public signature, or a public field of a public type | no, and must not |
The first five are a missing contract, and the remedy is to write it.
std.contracts growing is the mechanism by which programs get faster, and a
program compiled against a ledger that says nothing behaves exactly as it does
today. The same shape as ADR-288, where
writing a contract down is what let a caller earn sync.
The last one is a public signature, and an override there would be a promise
about code that does not exist yet: whether the value ever crosses is decided by
callers this build never reads. std.contracts already refuses to make that kind
of promise — it is why a higher-order method’s sync is sync(f) rather than a
committed answer (ADR-288 D31). And a representation cannot be
deferred to the caller that way at all: sync is a claim about behaviour, so the callee’s
compiled code is the same whichever answer it carries, while a count is a
representation and Rc<T> and Arc<T> are two different types — a published
artifact has already chosen which one it is
(docs/history/rc-or-arc.md §5.1).
So the language’s escapes are restrictions, not permissions. A request for a cheaper representation is a permission, and there is not one.
Revisited if somebody writes a real program where the analysis falls back, the contract that would decide it cannot be written, and the 9 ns can be measured. Until then the way to the plain count is the way to every other derived fact in this project: write down what the compiler cannot see.
Besides D1’s short names, target takes the short names aarch64-android,
x86_64-android and armv7-android, and any triple rustc --print
target-list prints, written as Rust writes it. A triple that has a short name
is that target. The list is the toolchain floor’s, kept in the compiler.
What such a target offers is read from its triple: a -none or -uefi triple
has no operating system, so no threads, no runtime and no std, and a panic
aborts; a wasm triple has no threads and aborts; any other has threads, the
runtime, and unwinds. A bare-metal target is refused with that reason rather
than built; every other one is handed to Cargo, and a toolchain without its
std is refused as D1 says.
Why every triple, and not a curated list. The backend is Rust’s, so a machine Rust builds for is one the program can be built for at no cost to the language; a list of our own would refuse what works and have to be kept. Android is the first that needs it.
Rejected: a target for each machine as a variant of its own (the list is Rust’s, and grows with it); accepting any string (a typo would reach Cargo).
Not decided here: build profiles. How a program on a bare-metal target starts and waits - a main loop or interrupt handlers - and other details of a machine belong in a named profile handed to the build, decided in its own record when the first such target is built for.
Freedom from data races is a property of the program rather than of a build
mode. At user_parallelism = no nothing the user wrote runs concurrently, so
nothing the user wrote can race — on any machine.
A library compiled at no and used in a program at yes is the case the
structural Send check exists for: it runs under both settings so that a
library cannot turn out to be un-compilable where it is used.
That check is ADR-005 §5 — it is Group B’s third member and that record is where it was decided. Two things about it belong here, because they are about this switch:
user_parallelism would answer differently at the two settings, which is the
whole failure the paragraph above describes.no nothing the user wrote runs concurrently, so the
emitter writes no task and a crossing into one does not happen in that build:
refusing it would refuse a program that compiles, so it is reported as a lint
(Part III C.3, NK2501). A crossing into a foreign runtime’s thread is not
bounded by this switch — D2’s “user” is load-bearing — so it is refused at both
settings (ADR-303 D7, NK2502).D6 answers the question that stood in front of Shared: the choice between the
two counts does not stay per build, so a Shared crosses, and the verdict still
does not depend on the build — which is why the answer had to be one
representation rather than a switch the check could read. What is left standing
in front of Part II 12.2’s counter is Locked.
overlapChanged by ADR-292 D1 and D6: the compiler overlaps nothing on its own, and the operations an overlap block hands the runtime are in flight together at either setting.
At no, the branches of an overlap block that are the program’s own
computation run one at a time, because both are code the user wrote; the I/O
the runtime performs for them is not, so it overlaps anyway. At yes two
computations may overlap too.
The switch is not “does this build have threads”. It has a second one at no
too: Part I 8.4’s Runtime Sidecar takes blocking I/O off the event loop, and is
safe precisely because no user code runs there. What no forbids is that
anything you wrote is in flight twice.
--target and --user-parallelism override [build] target and
[build] user-parallelism in nikaia.toml for one build (D5); both are in the
build-cache key and neither is in nikaia.contracts (D4).
One verdict at both settings. user_parallelism reaches exactly one line of
§3’s structural Send check — the severity — and nothing in the analysis
itself, so a test runs the same program at both settings and compares the
verdict rather than the exit code.
The count is the type a Shared is lowered to — std::rc::Rc<T> where
contracts::sharing proves the value stays on one thread, std::sync::Arc<T>
otherwise (D6, D7). The base case is asserted: a Shared that nothing crosses
with gets the plain count, without which an analysis that answered atomic
for everything would pass every other test. nikaia --sharing prints the
per-value report and the closed list of fallbacks with the remedy for each (D8).
wasm32-unknown is refused, not mis-emitted. The CLI accepts the name and
refuses it with what is missing behind it — std reaches for a memory mapping
and a thread pool, and neither exists there (D1).