update_all Hands Back One Value Per LockStatus: Superseded by ADR-281 — its D1-D3 are D17-D19 there Answers: ADR-059 §4’s open question — “what such a door is called, and whether it hands a value back per lock” — which that record named as it created it Related: ADR-064 D2 (the same reason for the same arrangement), ADR-039 D2 (nesting two acquisitions is refused, which is what makes one door necessary), ADR-031 (the ledger binds from the receiver)
Part II 12.3 writes the transfer between two accounts as the worked example of
composed locking, and the language could not express it.
ADR-059 D1 made access a read, and access_all is the same
reading widened; update writes one. Take from one account and give to the
other, under both locks: no door.
And access_all itself was never built. Measured before deciding — what a
program that writes one gets today:
nothing written down describes `access_all`, so this compiler cannot see the end
of it — and starting a thread of its own is among the things it may do
`SharedMut[?]` holds a lock, and a lock may not go into code nothing written
down describesThe language’s own door for several locks is refused by the language’s own rule
for locks, because nothing describes it. It parses: the grammar has taken
access_all(a, b) fn(x, y) { … } since the trailing-lambda rule, as an ordinary
free call whose last argument stands outside the parentheses. What was missing was
never syntax.
Why a ledger entry cannot describe it. A signature binds its type variables
from the receiver (ADR-031); a door over several locks has none.
The locks are arguments, they hold different types, and how many there are is
open — (&SharedMut[$T], &SharedMut[$U], f: fn(&$T, &$U)) needs two variables
bound from arguments and still fixes the count at two.
The same arrangement as the hull constructors and for the same sentence (ADR-064 D2): the ledger binds from a receiver and there is none. The checker types the locks first, derives what each holds, and hands the block one parameter per lock — which is the one thing a written signature could not have said.
And not a construct, because the grammar already takes the call form. A keyword would cost a reserved word (ADR-051) and buy nothing.
Not a method on one of the locks either. konto_a.update_with(konto_b) reads
as first A, then B — and an order the source implies is exactly the bug this door
exists to prevent. The locks stand side by side because that is what they are.
What the ledger still says is the sync column, from an entry with no
signature at all: an acquisition adds no pausing of its own, so the block decides
(sync = "from(f)", ADR-029 D3). Each mechanism does the half it
can: the ledger carries the property, the compiler carries the types.
access_all reads, update_all writes one new value per lock.update’s rule widened, not a second rule: the block takes one mut per
lock, changes them, and returns nothing (ADR-110 D6).
update_all(konto_a, konto_b) fn(mut von, mut nach) {
von -= 30
nach += 30
}Nothing sees either lock between the two writes. Whether the block runs on copies and is retried, or on the addresses under the locks, is the compiler’s by the pair of types (ADR-110 D2); two words cannot be swapped together on every target, so the pair takes the locks in D3’s order.
std sorts the locks by address and takes them in that order, so access_all(a, b)
in one task and access_all(b, a) in another take them the same way round. There
is no cycle to deadlock in — the property Part II 12.3 states, made true rather
than described.
The names stand bare, beside println: a door over several locks belongs to the
language’s own vocabulary rather than behind a prefix, and it is exactly where a
reader of Part II 12.3 looks for it.
The transfer runs, at both settings, and prints 70 35. That is the first
program in Chapter 12 that was written down before it was possible and is possible
now.
Two threads doing it both ways round keep the total. Two thousand transfers
each, a minus one and b plus one against b minus one and a plus one:
neither deadlocks and nothing is created or lost. The address order is what that
measures.
Two locks need not hold the same type, or have got the same shape. Which shape
a value’s lock gets is decided per value (ADR-057), so one program
can hold both — a door written against Local or Crossing by name could not take
a pair. Door is the trait that says what a door needs of a lock, and a handle on
one is one too, so SharedMut[T] and a Locked[T] field reach the same door.
What it costs: NK1124, for a door handed something that is not a lock, one
lock where several are wanted, or a block that does not name one value per lock. A
number is refused there even though its type says nothing, because a literal
carries none on purpose (Part I 2.4) and reading that absence as “might be a
lock” is what sent the program to rustc.
std::lock does and is a different
mechanism. The refusal says “at least two” and the door takes two.println, which is where the language already keeps the words everybody has;
what the whole of that list should be is a question of its own.All three. nikaia_std::lock::Door with access_all and update_all over
it, implemented for both shapes and for a handle on either;
check::Checker::locks types the call and the block; the emitter writes the
locks by reference and the block last; std.contracts carries the sync column
for both names with no signature. Exercised by the transfer at both settings, by
two threads transferring in opposite directions, and by a pair of locks holding
different types.