docs(roadmap,readme): v0.7 complete — record outcomes and deviations
Gotchas now lead with the consuming-wake invariant ('the only wildcard wake
is request_stop') and the obligations it puts on future wakers. Deviations
recorded: the no-park exit's retire_wait/clear_notify (a protocol piece the
plan missed), Drop-guard deregistration superseded by own-pid assert
relaxation, and closed arms being ready forever.
This commit is contained in:
+40
-10
@@ -152,7 +152,7 @@ Landed as two primitives, *without* the sketched monitor machinery:
|
||||
|
||||
---
|
||||
|
||||
## v0.7 — select, on epoch-stamped consuming wakes
|
||||
## v0.7 — select, on epoch-stamped consuming wakes ✅ DONE
|
||||
|
||||
Goal: cross-channel wait (`select`) without surrendering the precise-wake
|
||||
invariant. Decision record: the alternative ("wakes are hints", loop-and-
|
||||
@@ -181,14 +181,14 @@ Protocol (the consuming-wake rules):
|
||||
`wait_fd`) stay exactly as written: precise wakes are preserved, so a wake
|
||||
still *means* something.
|
||||
|
||||
### 1. Slot-word epoch + consuming unparks
|
||||
### 1. Slot-word epoch + consuming unparks ✅ (`4913835`)
|
||||
`slot_state.rs`: repack, `begin_wait`, epoch-matched/consuming `unpark`,
|
||||
epoch-preserving claim/yield/park transitions. Loom: existing theorems
|
||||
re-proved on the new word + a new stale-epoch theorem (an unpark stamped with
|
||||
a consumed epoch can never enqueue *or* notify). Plumbing only — no caller
|
||||
stamps yet; behaviour identical.
|
||||
|
||||
### 2. Stamp every registration-based wake; retire per-primitive wait seqs
|
||||
### 2. Stamp every registration-based wake; retire per-primitive wait seqs ✅ (`400854a`)
|
||||
The epoch IS the wait identity, so `channel::Inner.{cur_wait,next_wait_seq}`
|
||||
and `mutex`'s per-wait `seq` are subsumed: registrations become
|
||||
`(pid, epoch)`, `TimerTarget::on_timeout(pid, epoch)`, wakers call
|
||||
@@ -196,7 +196,7 @@ and `mutex`'s per-wait `seq` are subsumed: registrations become
|
||||
waiters stamped likewise. End-state invariant, auditable in one sentence:
|
||||
**the only wildcard wake is `request_stop`.**
|
||||
|
||||
### 3. `select` — ready-index wait over multiple receivers
|
||||
### 3. `select` — ready-index wait over multiple receivers ✅ (`00128f3`)
|
||||
`select(&[&dyn Selectable]) -> usize`: register self in each arm's
|
||||
`parked_receiver` (sequentially — the park protocol makes cross-arm atomicity
|
||||
unnecessary), park once, wake, scan, return the first ready index; caller
|
||||
@@ -207,7 +207,7 @@ documented, like BEAM receive clauses; no fairness promise. No cancel pass
|
||||
(see protocol above). Drop-guard deregistration on the unwind path only, to
|
||||
keep tests' single-parked-receiver asserts honest.
|
||||
|
||||
### 4. `select_timeout`
|
||||
### 4. `select_timeout` ✅ (`a0a93b6`)
|
||||
A `WaitTimeout` timer stamped with the select's epoch, whose target is a
|
||||
stateless `unpark_at`. The woken selector classifies the wake from state
|
||||
alone: some arm ready → that arm; none ready → with precise wakes the timer
|
||||
@@ -215,14 +215,33 @@ is the only remaining stamped waker → `None`. No flag, no shared waiter
|
||||
struct, no registration to leak. The timer entry expires as a stale-epoch
|
||||
no-op when an arm wins, per the no-cancellation convention in `timer.rs`.
|
||||
|
||||
### 5. Docs + integration proof
|
||||
### 5. Docs + integration proof ✅ (this commit)
|
||||
README module table, gotchas rewrite (the "No `select`" bullet becomes the
|
||||
consuming-wake invariant), and an integration test of the motivating
|
||||
pattern: a server selecting over its inbox and a monitor `Down` channel.
|
||||
pattern: a server selecting over its inbox and a monitor `Down` channel
|
||||
(`tests/select.rs::motivating_pattern_inbox_plus_monitor_down`).
|
||||
|
||||
Unblocked but deliberately out of scope: `gen_server::handle_info` (now an
|
||||
API-design question, not a runtime question — see Later).
|
||||
|
||||
### Deviations from the plan
|
||||
- **The no-park exit needed a protocol piece the plan missed.** A `select`
|
||||
returning an arm ready at *registration* time leaves earlier arms holding
|
||||
live-epoch registrations — a sender could still set RunningNotified and
|
||||
fault the actor's next one-shot park. Landed as `scheduler::retire_wait`
|
||||
(bump the epoch, eat a landed notification via the new
|
||||
`StateWord::clear_notify`, re-observe the stop flag — in that order) plus
|
||||
the loom theorem `retire_eats_late_arm_notification`. The parked path
|
||||
needed nothing: the winning wake's consume already retires the epoch.
|
||||
- **No Drop guard.** The planned unwind-path deregistration was superseded:
|
||||
the single-receiver debug_asserts relax to "none, or my own pid", so a
|
||||
leftover own-registration (consumed epoch — inert by theorem) is simply
|
||||
overwritten by the receiver's next wait on that channel. Less machinery,
|
||||
and the asserts still catch the real misuse (two actors on one channel).
|
||||
- **A closed arm is ready *forever*** — callers must drop it from the arm
|
||||
set once observed, or priority order starves every higher-indexed arm
|
||||
(documented on `select`; found the hard way by a livelocking test).
|
||||
|
||||
---
|
||||
|
||||
## Later
|
||||
@@ -278,9 +297,20 @@ hardware. Build + run full test suite on an aarch64 device; check
|
||||
field must be reset in all three.
|
||||
- **Pid = (index, generation).** Stale handles caught by generation mismatch in
|
||||
`slot()/slot_mut()`. The monitor `NoProc` path relies on this.
|
||||
- **No `select`, no unified per-process mailbox.** Why the supervisor uses the
|
||||
single `supervisor_channel` funnel. `recv_match` is per-channel only; a
|
||||
cross-channel merge is the still-unmade decision (see v0.6 #3).
|
||||
- **The only wildcard wake is `request_stop`, and it is terminal.** Every
|
||||
registration-based waker (channel sends, mutex grants, wait-timers, io
|
||||
completions, joiner wakes, `select` arms) carries the wait's park-epoch
|
||||
and wakes through `unpark_at`; every successful wake consumes the epoch.
|
||||
Wakes are therefore *meaningful*: one-shot park sites interpret them
|
||||
without loops, and `select` needs no cancellation pass. When adding a new
|
||||
waker, decide which form it is — if its registration handle can outlive
|
||||
the wait it was created for, it MUST be epoch-stamped; a wait that can
|
||||
exit without parking MUST `retire_wait` first (see slot_state.rs).
|
||||
- **`select` exists; a unified per-process mailbox still does not.** The
|
||||
supervisor keeps its single `supervisor_channel` funnel; `recv_match`
|
||||
stays per-channel. `select` composes channels at the wait, not into one
|
||||
queue — the mailbox-merge decision remains open (see Later:
|
||||
gen_server handle_info).
|
||||
- **Cooperative-only.** Preemption and cancellation both depend on the actor
|
||||
reaching `check!()`/yield/alloc/blocking points.
|
||||
- **Lock order is Leaf → Channel, one of each at most** (debug-asserted in
|
||||
|
||||
Reference in New Issue
Block a user