From 49009f40bd19b50586ab5c53b9135eabdecc82ad Mon Sep 17 00:00:00 2001 From: Mike Grier Date: Tue, 15 Sep 2026 13:38:57 -0400 Subject: [PATCH 1/9] docs: queue M23, a survey of how much algorithm correctness can be machine-checked The workspace checks its concurrency with recorded reasoning, unit tests, a sabotage suite and a mutation sweep. That combination has found real bugs, and it has a measured blind spot: weakening a producer's `Acquire` load of the consumer's position to `Relaxed` left the entire `windows-waitable-queues` suite green while every logic defect injected beside it was caught. A test observes what a run happened to do; it cannot observe an ordering a run happened not to need. M23 asks how much of that can be closed by machine checking, and is framed as a **scoping instrument rather than a replacement**: a method that proves a protocol correct for three producers and a capacity of two does not prove the shipping code correct, but it moves a class of question out of "argued carefully" and into "checked", leaving a short named list of what remains for inspection. That list is the deliverable. Five items: survey the workspace's argued-but-unchecked algorithms and match each to a tool class (TLA+/PlusCal, loom, bounded proof, `const` assertions, or none); pilot exactly one, chosen because parameter shrinking makes an untestable property exhaustive -- `reserving_mpsc`'s claim-position recurrence needs 2^32 pushes to manifest but a model wrapping at 8 reaches the same interleaving in seconds; record by name what the pilot could not reach; re-home `M31.6`; and decide adoption with its cost stated. Two things the item is careful about, both from existing repository decisions: - **It does not pre-empt D-31**, which decided on considered grounds that 0.1.0 ships without machine-checked orderings. D-31's reasoning is the starting point: a model checker covers atomics and cannot cover `SetEvent`/`ResetEvent`, so stubbing them verifies a model of `SetEvent` -- the "measures the model, not the thing" trap this workspace has already been caught by once. - **It names the cost that applies to any specification**: it is another statement of the contract, able to drift from the code with nothing to detect it. That is the CONTRACT INTEGRITY restatement problem applied to an artefact that looks authoritative, so a stale model that still passes is worse than none. The decision has to say what keeps the two in step and who re-runs it. "Adopt nothing, and say why" is a legitimate outcome. **M23.4 fixes something found while writing this.** `M31.6` -- the `loom` verification `windows-waitable-queues` tells adopters is planned before 1.0 -- is referenced three times in that crate's design notes and has no live checklist item anywhere in the repository; the crate has only a `COMPLETED-CHECKLIST.md`. A public commitment that nothing will cause anyone to pick up is exactly the "design notes are not a work queue" failure the repository instructions name. Verified: both files ASCII and LF-only; every relative link resolves; the `#d-31` anchor exists and matches how the rest of the repository links to D-numbers. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- CHECKLIST.md | 92 ++++++++++++++++++++++++++++++++++++++++++++++++++++ PLANS.md | 2 +- 2 files changed, 93 insertions(+), 1 deletion(-) diff --git a/CHECKLIST.md b/CHECKLIST.md index 4d01818e8..5394268c6 100644 --- a/CHECKLIST.md +++ b/CHECKLIST.md @@ -185,6 +185,98 @@ written before it was stated. function pointer, which is exactly where such a path would be. Depends on M22.1's classification. +## M23 -- Find out how much of this workspace's algorithm correctness can be machine-checked + +**Why now, and what this is not.** The workspace's concurrency is checked today by reasoning recorded +beside the code, an extensive unit suite, a sabotage suite that injects defects and requires each to +be caught, and a cargo-mutants sweep. That combination has found real bugs -- `D-15`'s lost wakeup +among them. It also has a measured blind spot: +[crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) records that +weakening a producer's `Acquire` load of the consumer's position to `Relaxed` left the entire suite +green, while every logic defect injected beside it was caught. A test observes what a run happened to +do; it cannot observe an ordering that a run happened not to need. + +**The goal is to narrow where hand-inspection has to look, not to replace it.** A method that proves +a protocol correct for three producers and a capacity of two does not prove the shipping code +correct -- but it moves a class of question out of "argued carefully" and into "checked", and what +remains uncheckable is then a short, named list rather than the whole surface. That list is the +deliverable. Formal methods here are a scoping instrument. + +**This milestone does not commit the workspace to any tool**, and it must not pre-empt +[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31), which decided on considered grounds that +0.1.0 ships without machine-checked orderings. D-31's +reasoning is the starting point rather than something to overturn: a model checker covers atomics and +cannot cover `SetEvent`/`ResetEvent`, so stubbing them verifies a model of `SetEvent` rather than +`SetEvent` -- the "measures the model, not the thing" trap this workspace has already been caught by +once. Any tool this milestone recommends has to be read against that. + +- [ ] **M23.1** -- Survey the workspace for algorithms whose correctness is currently argued rather + than checked, and match each to the class of tool that could check it. + + Candidates, not exhaustive: `reserving_mpsc`'s packed claim word and its reservation admission rule; + `slotwise_mpsc`'s per-slot sequence protocol; the experimental permit claim; the doorbell's mirror + flag against `SetEvent`/`ResetEvent`; `windows-file-watcher`'s contract state machine; + `windows-ioring-sys`' submission/completion ring. + + For each, record which of these fits and why: **TLA+/PlusCal** (protocol-level, exhaustive over a + small configuration, no memory model -- its actions are atomic and interleaved, which is sequential + consistency); **loom** (actual Rust under the C11 memory model, which is where the measured + weakened-`Acquire` blind spot lives); **kani or similar bounded proof** (Rust, memory-safety and + assertion checking); **`const` assertions** (arithmetic relationships between constants, already + used here and the cheapest of the four, because they fail the build rather than a run somebody + chose to make). + + The output is a table, and the "no tool fits this" rows are as valuable as the rest. + +- [ ] **M23.2** -- Pilot exactly one, chosen because parameter shrinking turns an untestable property + into an exhaustive one. + + `reserving_mpsc`'s claim-position recurrence (`SH-14.1`) is the strongest candidate: the defect + needs 2^32 pushes to manifest and is therefore beyond any test, but a model whose position wraps at + 8 makes the same interleaving reachable in seconds and yields a counterexample trace rather than a + suspicion. `capacity == 1` is a second such case -- the design notes record that two of the three + sequence states collapse to the same number there. + + Success is a counterexample for a deliberately broken variant, not a green run on the correct one. + A model that cannot produce the known bug when the bug is reintroduced has not been shown to be + checking anything -- the same sabotage discipline the test suites here already follow. + +- [ ] **M23.3** -- Write down what the pilot could NOT reach, by name. + + This is the item the milestone exists for. Expect the list to include: the memory orderings, if the + tool has no memory model; every syscall boundary, including the doorbell's; anything whose + correctness depends on the allocator, the scheduler, or real time; and the gap between the model + and the code, which no tool closes. + + Put it where a reader deciding how much to trust the crate will meet it -- beside the existing + "How far the memory orderings are verified, and how far they are not" section, which is already + written in the right register. + +- [ ] **M23.4** -- Re-home `M31.6`, which is currently orphaned. + + `windows-waitable-queues`' design notes reference `M31.6` in three places as the planned `loom` + verification, and [crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) + tells adopters it is planned before 1.0. There is no live checklist item for it anywhere in the + repository -- the crate has only a `COMPLETED-CHECKLIST.md`. That is the "design notes are not a + work queue" failure the repository instructions name: a public commitment that nothing will cause + anyone to pick up. + + Give it a real item in a real checklist, with its scope as D-31 describes it (both MPSC shapes or + neither), and make the design-note references point at it. + +- [ ] **M23.5** -- Decide what, if anything, the workspace adopts, and record the decision with its + cost. + + The cost to name explicitly, because it is the one this workspace keeps paying: **a specification is + another statement of the contract, and it can drift from the code with nothing to detect it.** That + is the restatement-drift problem in + [.github/copilot-instructions.md](.github/copilot-instructions.md)'s CONTRACT INTEGRITY section, + applied to an artefact that is harder to keep honest than prose because it looks authoritative. A + stale model that still passes is worse than no model. + + So the decision has to answer: what keeps the model and the code in step, who re-runs it, and what + happens when they disagree. "Adopt nothing, and say why" is a legitimate outcome -- D-31 reached it + once already on narrower grounds. ## M-inf -- Parked Ungated work with no identified predecessor deliverable. diff --git a/PLANS.md b/PLANS.md index 8441a8849..4d150a1c1 100644 --- a/PLANS.md +++ b/PLANS.md @@ -16,7 +16,7 @@ plans tracker: [crates/windows-file-enumeration-sys/PLANS.md](crates/windows-fil | Path to CHECKLIST.md | Status | Brief description | Design Notes | |---|---|---|---| -| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) | +| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M23: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0, which currently exists only in design notes with no live checklist item. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) | | [CHECKLIST-thread-ambient.md](CHECKLIST-thread-ambient.md) | in progress | M22-M23: extract the captured-context composite into `windows-thread-ambient-sys`, a standalone platform layer that captures a thread's ambient state and applies it on another thread. M24-M26: `windows-namespace-request-sys`, marshalable Win32 namespace call parameter sets, over a round-one entry list audited from three real consumers (this repository's watcher and enumeration crates, and `MikeGrier/Globazog-rs`) rather than guessed. M27: `windows-platform-probes`, a durable home for the measurements this workspace's designs rest on, under a three-tier scheme (asserted / ignored / binary-only) where every tier is compiled by an ordinary build. Feature-scoped and deleted when complete; it is the whole of the `mikegrier/thread-ambient` branch's work, and is deliberately separate from the deferred namespace-facility items in [CHECKLIST.md](CHECKLIST.md). | [crates/windows-thread-ambient-sys/DESIGN-NOTES.md](crates/windows-thread-ambient-sys/DESIGN-NOTES.md) | | [crates/windows-overlapped-io-sys/CHECKLIST.md](crates/windows-overlapped-io-sys/CHECKLIST.md) | not started | M14: finish the contract audit -- categories 1, 2, 6, 8, 9 were not examined -- and sweep `outstanding()` for the advisory-predicate hazard. | [crates/windows-overlapped-io-sys/DESIGN-NOTES.md](crates/windows-overlapped-io-sys/DESIGN-NOTES.md) | | [crates/windows-ioring-sys/CHECKLIST.md](crates/windows-ioring-sys/CHECKLIST.md) | in progress | Memory-safe Rust over the Windows `IoRing` submission/completion ring, as a new crate. M1-M7 (ring lifecycle through the `ring-copy` topology-aligned sample) are complete and archived. The parked, pinned-thread `M6+` work and the new M10 contract audit remain. | [crates/windows-ioring-sys/DESIGN-NOTES.md](crates/windows-ioring-sys/DESIGN-NOTES.md) | From 21bcc7f51ea97811a42ef2f8fe32ec509791741d Mon Sep 17 00:00:00 2001 From: Mike Grier Date: Tue, 15 Sep 2026 17:50:14 -0400 Subject: [PATCH 2/9] docs: renumber the formal-methods milestone M23 -> M30, which was taken M23 is already in use at the repository root. COMPLETED-CHECKLIST.md holds an archived M23, including M23.6 with its own anchor, from a milestone completed on 2026-09-01 -- so this branch gave a second, unrelated meaning to M23.1 through M23.5 and to the group heading itself. That is worse than untidy. The archive is append-only history, so the collision cannot be resolved later by editing the older entries; a `Completed item: M23.1` trailer would be ambiguous about which milestone it discharged, and any cross-reference to M23.x would resolve to whichever file the reader opened first. M30 is the next free number: the root pair references M1-M15 and M19-M29, with nothing above M29. Found while verifying a cross-reference from a design note on another branch -- the link checked out as a file but the anchor did not exist, and following that led here. Nothing about the milestone's content changes. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- CHECKLIST.md | 12 ++++++------ PLANS.md | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/CHECKLIST.md b/CHECKLIST.md index 5394268c6..cd70439c5 100644 --- a/CHECKLIST.md +++ b/CHECKLIST.md @@ -185,7 +185,7 @@ written before it was stated. function pointer, which is exactly where such a path would be. Depends on M22.1's classification. -## M23 -- Find out how much of this workspace's algorithm correctness can be machine-checked +## M30 -- Find out how much of this workspace's algorithm correctness can be machine-checked **Why now, and what this is not.** The workspace's concurrency is checked today by reasoning recorded beside the code, an extensive unit suite, a sabotage suite that injects defects and requires each to @@ -210,7 +210,7 @@ cannot cover `SetEvent`/`ResetEvent`, so stubbing them verifies a model of `SetE `SetEvent` -- the "measures the model, not the thing" trap this workspace has already been caught by once. Any tool this milestone recommends has to be read against that. -- [ ] **M23.1** -- Survey the workspace for algorithms whose correctness is currently argued rather +- [ ] **M30.1** -- Survey the workspace for algorithms whose correctness is currently argued rather than checked, and match each to the class of tool that could check it. Candidates, not exhaustive: `reserving_mpsc`'s packed claim word and its reservation admission rule; @@ -228,7 +228,7 @@ once. Any tool this milestone recommends has to be read against that. The output is a table, and the "no tool fits this" rows are as valuable as the rest. -- [ ] **M23.2** -- Pilot exactly one, chosen because parameter shrinking turns an untestable property +- [ ] **M30.2** -- Pilot exactly one, chosen because parameter shrinking turns an untestable property into an exhaustive one. `reserving_mpsc`'s claim-position recurrence (`SH-14.1`) is the strongest candidate: the defect @@ -241,7 +241,7 @@ once. Any tool this milestone recommends has to be read against that. A model that cannot produce the known bug when the bug is reintroduced has not been shown to be checking anything -- the same sabotage discipline the test suites here already follow. -- [ ] **M23.3** -- Write down what the pilot could NOT reach, by name. +- [ ] **M30.3** -- Write down what the pilot could NOT reach, by name. This is the item the milestone exists for. Expect the list to include: the memory orderings, if the tool has no memory model; every syscall boundary, including the doorbell's; anything whose @@ -252,7 +252,7 @@ once. Any tool this milestone recommends has to be read against that. "How far the memory orderings are verified, and how far they are not" section, which is already written in the right register. -- [ ] **M23.4** -- Re-home `M31.6`, which is currently orphaned. +- [ ] **M30.4** -- Re-home `M31.6`, which is currently orphaned. `windows-waitable-queues`' design notes reference `M31.6` in three places as the planned `loom` verification, and [crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) @@ -264,7 +264,7 @@ once. Any tool this milestone recommends has to be read against that. Give it a real item in a real checklist, with its scope as D-31 describes it (both MPSC shapes or neither), and make the design-note references point at it. -- [ ] **M23.5** -- Decide what, if anything, the workspace adopts, and record the decision with its +- [ ] **M30.5** -- Decide what, if anything, the workspace adopts, and record the decision with its cost. The cost to name explicitly, because it is the one this workspace keeps paying: **a specification is diff --git a/PLANS.md b/PLANS.md index 4d150a1c1..949dbd764 100644 --- a/PLANS.md +++ b/PLANS.md @@ -16,7 +16,7 @@ plans tracker: [crates/windows-file-enumeration-sys/PLANS.md](crates/windows-fil | Path to CHECKLIST.md | Status | Brief description | Design Notes | |---|---|---|---| -| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M23: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0, which currently exists only in design notes with no live checklist item. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) | +| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0, which currently exists only in design notes with no live checklist item. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) | | [CHECKLIST-thread-ambient.md](CHECKLIST-thread-ambient.md) | in progress | M22-M23: extract the captured-context composite into `windows-thread-ambient-sys`, a standalone platform layer that captures a thread's ambient state and applies it on another thread. M24-M26: `windows-namespace-request-sys`, marshalable Win32 namespace call parameter sets, over a round-one entry list audited from three real consumers (this repository's watcher and enumeration crates, and `MikeGrier/Globazog-rs`) rather than guessed. M27: `windows-platform-probes`, a durable home for the measurements this workspace's designs rest on, under a three-tier scheme (asserted / ignored / binary-only) where every tier is compiled by an ordinary build. Feature-scoped and deleted when complete; it is the whole of the `mikegrier/thread-ambient` branch's work, and is deliberately separate from the deferred namespace-facility items in [CHECKLIST.md](CHECKLIST.md). | [crates/windows-thread-ambient-sys/DESIGN-NOTES.md](crates/windows-thread-ambient-sys/DESIGN-NOTES.md) | | [crates/windows-overlapped-io-sys/CHECKLIST.md](crates/windows-overlapped-io-sys/CHECKLIST.md) | not started | M14: finish the contract audit -- categories 1, 2, 6, 8, 9 were not examined -- and sweep `outstanding()` for the advisory-predicate hazard. | [crates/windows-overlapped-io-sys/DESIGN-NOTES.md](crates/windows-overlapped-io-sys/DESIGN-NOTES.md) | | [crates/windows-ioring-sys/CHECKLIST.md](crates/windows-ioring-sys/CHECKLIST.md) | in progress | Memory-safe Rust over the Windows `IoRing` submission/completion ring, as a new crate. M1-M7 (ring lifecycle through the `ring-copy` topology-aligned sample) are complete and archived. The parked, pinned-thread `M6+` work and the new M10 contract audit remain. | [crates/windows-ioring-sys/DESIGN-NOTES.md](crates/windows-ioring-sys/DESIGN-NOTES.md) | From d4c30e4e786fe325a4f0ebf26c553c3731725fe4 Mon Sep 17 00:00:00 2001 From: Mike Grier Date: Tue, 15 Sep 2026 19:20:45 -0400 Subject: [PATCH 3/9] docs: correct the pilot's premise, which named the wrong reason and the wrong shape Eight findings. Two were factual errors in the milestone's central argument. M30.2 said SH-14.1 "needs 2^32 pushes to manifest and is therefore beyond any test". Both halves were wrong in a way that weakened the case it was making. 2^32 pushes is about 37 seconds of sustained maximum-rate pushing on the host the queue crate publishes -- far outside a unit suite budgeted in milliseconds, but not beyond a long integration test, so "beyond any test" overstated it. And the count is not the reason: the crate's README records that reaching the wrap is necessary but NOT sufficient, because a producer must also be stalled inside a window a few instructions wide. That is what no test can schedule. Corrected, and the corrected version argues the pilot better -- parameter shrinking earns its place by making the interleaving exhaustive rather than by making the count small. The same item offered `capacity == 1` as a second candidate. That is D-12, an edge case of slotwise_mpsc's slot SEQUENCE protocol, unrelated to reserving_mpsc's claim position -- and already resolved, by that shape refusing a capacity below two with a sabotage entry holding it. Verified before removing: every statement of the collapse in the crate attributes it to slotwise_mpsc's three-state sequence arithmetic. Left in place it would have pointed the one pilot at a different shape's settled property. M30.4 asserted that no live checklist item exists for M31.6 anywhere in the repository -- a statement its own existence falsifies once this lands. Reworded as the pre-M30.4 fact it is. The rest are reference hygiene: D-15 was a bare identifier and five crates define one, so it is now a link to the queue's; the queue's COMPLETED-CHECKLIST.md is a link; a blank line separates M30.5 from the M-inf heading per the checklist format; and PLANS.md's Design Notes cell no longer points M30 readers at the namespace-remoting anchor, which is unrelated -- M30 has no decision recorded yet, which is what M30.5 exists to produce. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- CHECKLIST.md | 36 ++++++++++++++++++++++++++---------- PLANS.md | 2 +- 2 files changed, 27 insertions(+), 11 deletions(-) diff --git a/CHECKLIST.md b/CHECKLIST.md index cd70439c5..6db4658ac 100644 --- a/CHECKLIST.md +++ b/CHECKLIST.md @@ -189,7 +189,8 @@ written before it was stated. **Why now, and what this is not.** The workspace's concurrency is checked today by reasoning recorded beside the code, an extensive unit suite, a sabotage suite that injects defects and requires each to -be caught, and a cargo-mutants sweep. That combination has found real bugs -- `D-15`'s lost wakeup +be caught, and a cargo-mutants sweep. That combination has found real bugs -- +[D-15](crates/windows-waitable-queues/DESIGN-NOTES.md#d-15)'s lost wakeup among them. It also has a measured blind spot: [crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) records that weakening a producer's `Acquire` load of the consumer's position to `Relaxed` left the entire suite @@ -231,11 +232,24 @@ once. Any tool this milestone recommends has to be read against that. - [ ] **M30.2** -- Pilot exactly one, chosen because parameter shrinking turns an untestable property into an exhaustive one. - `reserving_mpsc`'s claim-position recurrence (`SH-14.1`) is the strongest candidate: the defect - needs 2^32 pushes to manifest and is therefore beyond any test, but a model whose position wraps at - 8 makes the same interleaving reachable in seconds and yields a counterexample trace rather than a - suspicion. `capacity == 1` is a second such case -- the design notes record that two of the three - sequence states collapse to the same number there. + `reserving_mpsc`'s claim-position recurrence (`SH-14.1`) is the strongest candidate, and the reason + is the interleaving rather than the count. Reaching the wrap takes 2^32 pushes -- about 37 seconds + of sustained maximum-rate pushing on the host the crate publishes, which is far outside a unit + suite budgeted in milliseconds but is not in itself beyond a long integration test. What is beyond + any test is the rest of the condition: + [crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) records that + reaching the wrap is necessary but *not sufficient* -- a producer must also be stalled inside a + window a few instructions wide, and no test can schedule that deliberately. A model whose position + wraps at 8 makes the whole interleaving reachable in seconds and *exhaustive* rather than sampled, + and yields a counterexample trace rather than a suspicion. + + An earlier version of this item said the defect "needs 2^32 pushes to manifest and is therefore + beyond any test", which overstated the limitation and named the wrong reason for it. It also + offered `capacity == 1` as a second candidate; that is + [D-12](crates/windows-waitable-queues/DESIGN-NOTES.md#d-12), an edge case of `slotwise_mpsc`'s slot + *sequence* protocol and unrelated to `reserving_mpsc`'s claim position -- and one already resolved + by that shape refusing a capacity below two, with a sabotage entry holding it. Pointing the pilot + at it would have sent it after a different shape's settled property. Success is a counterexample for a deliberately broken variant, not a green run on the correct one. A model that cannot produce the known bug when the bug is reintroduced has not been shown to be @@ -256,10 +270,11 @@ once. Any tool this milestone recommends has to be read against that. `windows-waitable-queues`' design notes reference `M31.6` in three places as the planned `loom` verification, and [crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) - tells adopters it is planned before 1.0. There is no live checklist item for it anywhere in the - repository -- the crate has only a `COMPLETED-CHECKLIST.md`. That is the "design notes are not a - work queue" failure the repository instructions name: a public commitment that nothing will cause - anyone to pick up. + tells adopters it is planned before 1.0. Until this item, there was no live checklist item for it + anywhere in the repository -- the crate has only a + [COMPLETED-CHECKLIST.md](crates/windows-waitable-queues/COMPLETED-CHECKLIST.md). That was the + "design notes are not a work queue" failure the repository instructions name: a public commitment + that nothing will cause anyone to pick up. Give it a real item in a real checklist, with its scope as D-31 describes it (both MPSC shapes or neither), and make the design-note references point at it. @@ -277,6 +292,7 @@ once. Any tool this milestone recommends has to be read against that. So the decision has to answer: what keeps the model and the code in step, who re-runs it, and what happens when they disagree. "Adopt nothing, and say why" is a legitimate outcome -- D-31 reached it once already on narrower grounds. + ## M-inf -- Parked Ungated work with no identified predecessor deliverable. diff --git a/PLANS.md b/PLANS.md index 949dbd764..6fec056b4 100644 --- a/PLANS.md +++ b/PLANS.md @@ -16,7 +16,7 @@ plans tracker: [crates/windows-file-enumeration-sys/PLANS.md](crates/windows-fil | Path to CHECKLIST.md | Status | Brief description | Design Notes | |---|---|---|---| -| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0, which currently exists only in design notes with no live checklist item. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) | +| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0, which currently exists only in design notes with no live checklist item. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) for M19-M22; M30 has no decision recorded yet, which is the point of M30.5 | | [CHECKLIST-thread-ambient.md](CHECKLIST-thread-ambient.md) | in progress | M22-M23: extract the captured-context composite into `windows-thread-ambient-sys`, a standalone platform layer that captures a thread's ambient state and applies it on another thread. M24-M26: `windows-namespace-request-sys`, marshalable Win32 namespace call parameter sets, over a round-one entry list audited from three real consumers (this repository's watcher and enumeration crates, and `MikeGrier/Globazog-rs`) rather than guessed. M27: `windows-platform-probes`, a durable home for the measurements this workspace's designs rest on, under a three-tier scheme (asserted / ignored / binary-only) where every tier is compiled by an ordinary build. Feature-scoped and deleted when complete; it is the whole of the `mikegrier/thread-ambient` branch's work, and is deliberately separate from the deferred namespace-facility items in [CHECKLIST.md](CHECKLIST.md). | [crates/windows-thread-ambient-sys/DESIGN-NOTES.md](crates/windows-thread-ambient-sys/DESIGN-NOTES.md) | | [crates/windows-overlapped-io-sys/CHECKLIST.md](crates/windows-overlapped-io-sys/CHECKLIST.md) | not started | M14: finish the contract audit -- categories 1, 2, 6, 8, 9 were not examined -- and sweep `outstanding()` for the advisory-predicate hazard. | [crates/windows-overlapped-io-sys/DESIGN-NOTES.md](crates/windows-overlapped-io-sys/DESIGN-NOTES.md) | | [crates/windows-ioring-sys/CHECKLIST.md](crates/windows-ioring-sys/CHECKLIST.md) | in progress | Memory-safe Rust over the Windows `IoRing` submission/completion ring, as a new crate. M1-M7 (ring lifecycle through the `ring-copy` topology-aligned sample) are complete and archived. The parked, pinned-thread `M6+` work and the new M10 contract audit remain. | [crates/windows-ioring-sys/DESIGN-NOTES.md](crates/windows-ioring-sys/DESIGN-NOTES.md) | From e1c8d648fc4d128fdca331cf51cab42c101346dc Mon Sep 17 00:00:00 2001 From: Mike Grier Date: Tue, 15 Sep 2026 19:37:40 -0400 Subject: [PATCH 4/9] docs: give the pilot a refinement criterion, and move the rationale out of the queue Eight findings. Three were methodological gaps in the pilot's design, and the rest were scope and hygiene. M30.2 asked for a model whose position wraps at 8 without ever requiring anyone to say why that is evidence about a 32-bit field. Shrinking a parameter is itself a claim -- that the protocol's correctness does not depend on that width -- and if nobody states it, a green run proves something about the model alone. The item now requires the correspondence to be written down (which constants were shrunk, why the protocol is uniform in each, what a counterexample at 8 implies at 2^32) or the result reported as a counterexample in a toy model and nothing more. This is the "measures the model, not the thing" trap D-31 already names, wearing a second costume, so the rationale note now names it there too. M30.2's success criterion was half a criterion. It asked for a counterexample from a deliberately broken variant and explicitly NOT a green run on the correct one -- an overcorrection. A counterexample from the broken variant can also come from a malformed model that would find one anywhere, so it is an anti-vacuity check rather than a property check. Both halves are now required. M30.5 allowed "adopt nothing" without reconciling the three public places that promise machine-checked verification before 1.0 (README, lib.rs, D-31). A no-adoption outcome left as-is would recreate, in the same crate, exactly the orphaned-commitment failure M30.4 exists to fix. The sweep is now part of the item whichever way it goes. M30.4's sweep was scoped to the three design-note references. Counted: M31.6 appears five times across three files -- three in DESIGN-NOTES.md, one in src/doorbell.rs, one in sabotage.json. Completing it as written would have left a stale identifier in a source file and in the sabotage manifest. Opening queue work also obliges the crate's PLANS.md, which still says "No checklist is open against this crate"; adding that row is now part of the item. M30.3 said to put the uncheckable-list beside the existing memory-orderings disclosure without noting that the disclosure has two copies, README.md and src/lib.rs. Updating one would leave the other telling an adopter something the crate no longer believes. The item now requires both, and points out that the README is already a build input so deriving one from the other is available and cannot drift. The milestone opened with three paragraphs of rationale, which the action-only rule for checklist files forbids and which would have made the checklist a second design record able to drift from the first. Moved to DESIGN-NOTES.md under a new anchored section, with the checklist keeping a one-line pointer. The section states that no decision is recorded yet, so the absence of one is visibly intentional. The PR-metadata finding was already fixed before this review was submitted; the title and body have said M30 since the previous round. All 105 relative links in the three root documents were checked for file AND anchor resolution before commit -- the cross-branch anchor that would have shipped broken here was caught that way. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- CHECKLIST.md | 74 ++++++++++++++++++++++++++++++------------------- DESIGN-NOTES.md | 47 +++++++++++++++++++++++++++++++ 2 files changed, 92 insertions(+), 29 deletions(-) diff --git a/CHECKLIST.md b/CHECKLIST.md index 6db4658ac..06aeef2d4 100644 --- a/CHECKLIST.md +++ b/CHECKLIST.md @@ -187,29 +187,10 @@ written before it was stated. ## M30 -- Find out how much of this workspace's algorithm correctness can be machine-checked -**Why now, and what this is not.** The workspace's concurrency is checked today by reasoning recorded -beside the code, an extensive unit suite, a sabotage suite that injects defects and requires each to -be caught, and a cargo-mutants sweep. That combination has found real bugs -- -[D-15](crates/windows-waitable-queues/DESIGN-NOTES.md#d-15)'s lost wakeup -among them. It also has a measured blind spot: -[crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) records that -weakening a producer's `Acquire` load of the consumer's position to `Relaxed` left the entire suite -green, while every logic defect injected beside it was caught. A test observes what a run happened to -do; it cannot observe an ordering that a run happened not to need. - -**The goal is to narrow where hand-inspection has to look, not to replace it.** A method that proves -a protocol correct for three producers and a capacity of two does not prove the shipping code -correct -- but it moves a class of question out of "argued carefully" and into "checked", and what -remains uncheckable is then a short, named list rather than the whole surface. That list is the -deliverable. Formal methods here are a scoping instrument. - -**This milestone does not commit the workspace to any tool**, and it must not pre-empt -[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31), which decided on considered grounds that -0.1.0 ships without machine-checked orderings. D-31's -reasoning is the starting point rather than something to overturn: a model checker covers atomics and -cannot cover `SetEvent`/`ResetEvent`, so stubbing them verifies a model of `SetEvent` rather than -`SetEvent` -- the "measures the model, not the thing" trap this workspace has already been caught by -once. Any tool this milestone recommends has to be read against that. +Why this milestone exists, what it is not, and how it relates to +[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) are recorded in +[DESIGN-NOTES.md](DESIGN-NOTES.md#machine-checking-what-is-argued) rather than here, per the +action-only rule for checklist files. - [ ] **M30.1** -- Survey the workspace for algorithms whose correctness is currently argued rather than checked, and match each to the class of tool that could check it. @@ -251,9 +232,21 @@ once. Any tool this milestone recommends has to be read against that. by that shape refusing a capacity below two, with a sabotage entry holding it. Pointing the pilot at it would have sent it after a different shape's settled property. - Success is a counterexample for a deliberately broken variant, not a green run on the correct one. - A model that cannot produce the known bug when the bug is reintroduced has not been shown to be - checking anything -- the same sabotage discipline the test suites here already follow. + **Write down what makes the wrap-at-8 model evidence about `Balanced`, or record that it is not.** + Shrinking the position to 3 bits is a claim that the protocol's correctness does not depend on the + field's width -- that the shipping code refines the model. State that correspondence explicitly: + which constants were shrunk, why the protocol is uniform in each, and what a counterexample at 8 + therefore implies at 2^32. If it cannot be argued, the pilot's result is a counterexample *in a toy + model* and must be reported as exactly that. A reduced model that nobody has tied to the code can + pass and mean nothing, which is the "measures the model, not the thing" trap in a second costume. + + **Success needs both halves.** The unmodified model must satisfy its invariant, *and* a + deliberately broken variant must produce a counterexample. Neither alone is enough: a green run on + the correct model says nothing if the model is too permissive or the invariant vacuous, and a + counterexample from the broken variant can also be produced by a malformed model that would find + one anywhere. The first is the property check; the second is the anti-vacuity check, and it is the + same sabotage discipline the test suites here already follow. An earlier version of this item asked + only for the second, which overcorrected. - [ ] **M30.3** -- Write down what the pilot could NOT reach, by name. @@ -263,8 +256,12 @@ once. Any tool this milestone recommends has to be read against that. and the code, which no tool closes. Put it where a reader deciding how much to trust the crate will meet it -- beside the existing - "How far the memory orderings are verified, and how far they are not" section, which is already - written in the right register. + "How far the memory orderings are verified, and how far they are not" section. **That section has + two copies**, [README.md](crates/windows-waitable-queues/README.md) and + [src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and updating one would leave the other + telling an adopter something the crate no longer believes. Update both, or make one derive from the + other -- the README is already a build input via `#[doc = include_str!]`, so the second option is + available and is the one that cannot drift. - [ ] **M30.4** -- Re-home `M31.6`, which is currently orphaned. @@ -277,7 +274,17 @@ once. Any tool this milestone recommends has to be read against that. that nothing will cause anyone to pick up. Give it a real item in a real checklist, with its scope as D-31 describes it (both MPSC shapes or - neither), and make the design-note references point at it. + neither), and repoint every reference at it. **There are five, not three**: three in + [DESIGN-NOTES.md](crates/windows-waitable-queues/DESIGN-NOTES.md), one in + [src/doorbell.rs](crates/windows-waitable-queues/src/doorbell.rs), and one in + [sabotage.json](crates/windows-waitable-queues/sabotage.json). Sweeping only the design notes would + leave a stale identifier in a source file and in the sabotage manifest -- the same + fix-the-reported-site-not-the-class failure this repository keeps paying for. + + Opening queue work also obliges the component tracker: + [crates/windows-waitable-queues/PLANS.md](crates/windows-waitable-queues/PLANS.md) currently says + "No checklist is open against this crate", which this item falsifies. Add the row, as other crates + do for root-owned checklists. - [ ] **M30.5** -- Decide what, if anything, the workspace adopts, and record the decision with its cost. @@ -293,6 +300,15 @@ once. Any tool this milestone recommends has to be read against that. happens when they disagree. "Adopt nothing, and say why" is a legitimate outcome -- D-31 reached it once already on narrower grounds. + **Either outcome obliges a contract sweep, and a no-adoption outcome obliges it most.** Three + public places promise machine-checked verification before 1.0: + [README.md](crates/windows-waitable-queues/README.md), + [src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and D-31 in + [DESIGN-NOTES.md](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Deciding to adopt nothing + without reconciling those leaves the crate promising adopters something no item will deliver -- + which is the failure M30.4 exists to fix, recreated by the milestone that fixed it. Sweep all three + as part of this item, whichever way it goes. + ## M-inf -- Parked Ungated work with no identified predecessor deliverable. diff --git a/DESIGN-NOTES.md b/DESIGN-NOTES.md index bcb098811..1203345fb 100644 --- a/DESIGN-NOTES.md +++ b/DESIGN-NOTES.md @@ -1859,6 +1859,7 @@ written. The rule is about **discarded failure information**, not about discarde The audit this decision implies is queued as [CHECKLIST.md](CHECKLIST.md) -> `M22.1`; it is not scheduled by this note alone. + ## Prose volume is not the error surface; restatement count is **Decided: the error surface is proportional to how often a fact is restated, not to how much prose @@ -1908,3 +1909,49 @@ that has never been wrong while leaving the prose that keeps being wrong in prop was taken, which findings it is drawn from, what was rejected on the way, and the one cheap remedy that was costed but not adopted are in [DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#why-restatement-count-is-what-is-watched). + +## Machine-checking what is currently argued: why M30 exists and what it is not + +Context for [CHECKLIST.md](CHECKLIST.md) -> `M30`. It lives here rather than in the checklist +because a checklist is an action queue, and this is rationale. + +**What checks this workspace's concurrency today.** Reasoning recorded beside the code, an extensive +unit suite, a sabotage suite that injects defects and requires each to be caught, and a +cargo-mutants sweep. That combination is not weak, and it has found real bugs -- +[D-15](crates/windows-waitable-queues/DESIGN-NOTES.md#d-15)'s lost wakeup among them. + +**It has a measured blind spot, and the measurement is the reason for the milestone.** +[crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) records that +weakening a producer's `Acquire` load of the consumer's position to `Relaxed` left the entire suite +green, while every *logic* defect injected beside it was caught. That asymmetry is not a gap in the +suite's thoroughness; it is what a test is. A test observes what a run happened to do, and cannot +observe an ordering that a run happened not to need. + +The general form of that asymmetry -- classes with an oracle converge, classes without one do not -- +is worth keeping in view when reading the survey's results. Memory ordering has no oracle here. + +**The goal is to narrow where hand-inspection has to look, not to replace it.** A method that proves +a protocol correct for three producers and a capacity of two does not prove the shipping code +correct. What it does is move a class of question out of "argued carefully" and into "checked", so +that what remains uncheckable is a short, named list rather than the whole surface. **That list is +the deliverable**, which is why `M30.3` is the item the milestone exists for rather than a tidying +step after the pilot. Formal methods here are a scoping instrument. + +**This does not commit the workspace to any tool, and must not pre-empt +[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31)**, which decided on considered grounds +that 0.1.0 ships without machine-checked orderings. D-31's reasoning is the starting point rather +than something to overturn, and its central objection survives any tool choice: a model checker +covers atomics and cannot cover `SetEvent`/`ResetEvent`, so stubbing them verifies a model of +`SetEvent` rather than `SetEvent` itself. That is the "measures the model, not the thing" trap this +workspace has already been caught by once, and the doorbell is precisely where its one real ordering +bug lived. Any tool the milestone recommends has to be read against that. + +**The same trap has a second costume, which `M30.2` now guards against explicitly.** Shrinking a +model's parameters -- a position that wraps at 8 rather than 2^32 -- is itself a claim: that the +protocol's correctness does not depend on the width of that field. If nobody states why the shipping +code refines the reduced model, a green run proves something about the model alone. A reduced model +that has not been tied to the code can pass and mean nothing. + +**No decision is recorded here yet.** This section is context for queued work, not an outcome; +`M30.5` is what produces the decision, and "adopt nothing, and say why" remains a legitimate result +of it. From a6a9a8f5d93d3dad93cb275b7a98c1976ad5519f Mon Sep 17 00:00:00 2001 From: Mike Grier Date: Tue, 15 Sep 2026 19:46:44 -0400 Subject: [PATCH 5/9] docs: do the tracker update rather than queue it, and finish emptying the checklist Five findings. Four held and one did not. The queue crate's PLANS.md still said "No checklist is open against this crate" while M30.4 queues work against it. The previous round made updating it part of M30.4, which was the wrong call for the same reason M30.4's own text was wrong before this: the statement stops being true when the work is QUEUED, not when it is completed. The row is added here, and what M30.4 retains is keeping it accurate as the work proceeds. Format taken from the four other crates that already index root-owned checklists. Moving the milestone's rationale out last round left the revision history behind inside the items -- two "an earlier version of this item said..." paragraphs recording the untestability mis-attribution and the half-criterion. That is still history in an action-only file, and the previous commit's own pointer paragraph made it look addressed. Both moved to the DESIGN-NOTES section under a heading that says why they are worth keeping: each was an error in the argument FOR the pilot rather than in the plan, so a reader taking them on trust would have aimed the pilot wrongly. The checklist keeps only the actionable residue -- that capacity == 1 is not a candidate, and why. PLANS.md's row said M31.6 "currently exists only in design notes with no live checklist item", which this change falsifies twice over: it is queued as M30.4, and the references are not only in design notes -- one is in src/doorbell.rs and one in sabotage.json. Reworded to the past tense with the current location. The Design Notes cell now also links M30's rationale anchor, which existed but was not reachable from the tracker. DECLINED, with the check that settles it: the finding that M30.5's three links resolve to the repository root rather than the crate. They do not. The targets are crates/windows-waitable-queues/{README.md,src/lib.rs,DESIGN-NOTES.md} and all three resolve; only the link TEXT reads as a bare filename. Verified by resolving every relative link in all four changed files from its own file's directory -- 115 links, 0 broken. The instinct behind the finding is still worth acting on, though, because a bare "README.md" inside a root-level checklist genuinely does read as the root README, so the link text is now qualified ("that crate's README.md") at all five such sites. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- CHECKLIST.md | 42 +++++++++++-------------- DESIGN-NOTES.md | 20 ++++++++++++ PLANS.md | 2 +- crates/windows-waitable-queues/PLANS.md | 3 +- 4 files changed, 40 insertions(+), 27 deletions(-) diff --git a/CHECKLIST.md b/CHECKLIST.md index 06aeef2d4..5ec18b800 100644 --- a/CHECKLIST.md +++ b/CHECKLIST.md @@ -224,29 +224,22 @@ action-only rule for checklist files. wraps at 8 makes the whole interleaving reachable in seconds and *exhaustive* rather than sampled, and yields a counterexample trace rather than a suspicion. - An earlier version of this item said the defect "needs 2^32 pushes to manifest and is therefore - beyond any test", which overstated the limitation and named the wrong reason for it. It also - offered `capacity == 1` as a second candidate; that is - [D-12](crates/windows-waitable-queues/DESIGN-NOTES.md#d-12), an edge case of `slotwise_mpsc`'s slot - *sequence* protocol and unrelated to `reserving_mpsc`'s claim position -- and one already resolved - by that shape refusing a capacity below two, with a sabotage entry holding it. Pointing the pilot - at it would have sent it after a different shape's settled property. - **Write down what makes the wrap-at-8 model evidence about `Balanced`, or record that it is not.** Shrinking the position to 3 bits is a claim that the protocol's correctness does not depend on the field's width -- that the shipping code refines the model. State that correspondence explicitly: which constants were shrunk, why the protocol is uniform in each, and what a counterexample at 8 therefore implies at 2^32. If it cannot be argued, the pilot's result is a counterexample *in a toy - model* and must be reported as exactly that. A reduced model that nobody has tied to the code can - pass and mean nothing, which is the "measures the model, not the thing" trap in a second costume. + model* and must be reported as exactly that. **Success needs both halves.** The unmodified model must satisfy its invariant, *and* a deliberately broken variant must produce a counterexample. Neither alone is enough: a green run on the correct model says nothing if the model is too permissive or the invariant vacuous, and a counterexample from the broken variant can also be produced by a malformed model that would find - one anywhere. The first is the property check; the second is the anti-vacuity check, and it is the - same sabotage discipline the test suites here already follow. An earlier version of this item asked - only for the second, which overcorrected. + one anywhere. The first is the property check; the second is the anti-vacuity check. + + Not a candidate: `capacity == 1`. It belongs to `slotwise_mpsc`'s slot sequence protocol + ([D-12](crates/windows-waitable-queues/DESIGN-NOTES.md#d-12)), not to `reserving_mpsc`'s claim + position, and is already resolved by that shape refusing a capacity below two. - [ ] **M30.3** -- Write down what the pilot could NOT reach, by name. @@ -257,8 +250,8 @@ action-only rule for checklist files. Put it where a reader deciding how much to trust the crate will meet it -- beside the existing "How far the memory orderings are verified, and how far they are not" section. **That section has - two copies**, [README.md](crates/windows-waitable-queues/README.md) and - [src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and updating one would leave the other + two copies**, [that crate's README.md](crates/windows-waitable-queues/README.md) and + [its src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and updating one would leave the other telling an adopter something the crate no longer believes. Update both, or make one derive from the other -- the README is already a build input via `#[doc = include_str!]`, so the second option is available and is the one that cannot drift. @@ -275,16 +268,17 @@ action-only rule for checklist files. Give it a real item in a real checklist, with its scope as D-31 describes it (both MPSC shapes or neither), and repoint every reference at it. **There are five, not three**: three in - [DESIGN-NOTES.md](crates/windows-waitable-queues/DESIGN-NOTES.md), one in + [that crate's DESIGN-NOTES.md](crates/windows-waitable-queues/DESIGN-NOTES.md), one in [src/doorbell.rs](crates/windows-waitable-queues/src/doorbell.rs), and one in [sabotage.json](crates/windows-waitable-queues/sabotage.json). Sweeping only the design notes would leave a stale identifier in a source file and in the sabotage manifest -- the same fix-the-reported-site-not-the-class failure this repository keeps paying for. - Opening queue work also obliges the component tracker: - [crates/windows-waitable-queues/PLANS.md](crates/windows-waitable-queues/PLANS.md) currently says - "No checklist is open against this crate", which this item falsifies. Add the row, as other crates - do for root-owned checklists. + Opening queue work also obliges the component tracker. That row is added in this change rather than + deferred to this item, because + [crates/windows-waitable-queues/PLANS.md](crates/windows-waitable-queues/PLANS.md)'s "No checklist + is open against this crate" stops being true the moment M30.4 is queued, not when it is completed. + What remains for this item is to keep that row accurate as the work proceeds. - [ ] **M30.5** -- Decide what, if anything, the workspace adopts, and record the decision with its cost. @@ -301,10 +295,10 @@ action-only rule for checklist files. once already on narrower grounds. **Either outcome obliges a contract sweep, and a no-adoption outcome obliges it most.** Three - public places promise machine-checked verification before 1.0: - [README.md](crates/windows-waitable-queues/README.md), - [src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and D-31 in - [DESIGN-NOTES.md](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Deciding to adopt nothing + public places in `windows-waitable-queues` promise machine-checked verification before 1.0: + [that crate's README.md](crates/windows-waitable-queues/README.md), + [its src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and D-31 in + [its DESIGN-NOTES.md](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Deciding to adopt nothing without reconciling those leaves the crate promising adopters something no item will deliver -- which is the failure M30.4 exists to fix, recreated by the milestone that fixed it. Sweep all three as part of this item, whichever way it goes. diff --git a/DESIGN-NOTES.md b/DESIGN-NOTES.md index 1203345fb..fa42efacb 100644 --- a/DESIGN-NOTES.md +++ b/DESIGN-NOTES.md @@ -1955,3 +1955,23 @@ that has not been tied to the code can pass and mean nothing. **No decision is recorded here yet.** This section is context for queued work, not an outcome; `M30.5` is what produces the decision, and "adopt nothing, and say why" remains a legitimate result of it. + +### Two corrections the milestone's own drafting needed + +Recorded because both were errors in the *argument for* the pilot rather than in the plan, and a +reader taking them on trust would have aimed the pilot wrongly. + +**The untestability was mis-attributed to the count.** The first draft said `SH-14.1` "needs 2^32 +pushes to manifest and is therefore beyond any test". Both halves were wrong. 2^32 pushes is about 37 +seconds of sustained maximum-rate pushing on the host the queue crate publishes -- outside a unit +suite budgeted in milliseconds, but not beyond a long integration test. And the count was never the +reason: reaching the wrap is necessary but *not sufficient*, because a producer must also be stalled +inside a window a few instructions wide. That is what no test can schedule. The corrected reading +argues the pilot better, because parameter shrinking then earns its place by making the interleaving +*exhaustive* rather than by making a count small. + +**The success criterion was half a criterion.** The first draft asked for a counterexample from a +deliberately broken variant and explicitly *not* a green run on the correct one -- an overcorrection +against vacuous green runs. But a counterexample from a broken variant can equally be produced by a +malformed or over-permissive model that would find one anywhere, so it is an anti-vacuity check, not +a property check. Both are required, and the item now says so. diff --git a/PLANS.md b/PLANS.md index 6fec056b4..d78dc3a98 100644 --- a/PLANS.md +++ b/PLANS.md @@ -16,7 +16,7 @@ plans tracker: [crates/windows-file-enumeration-sys/PLANS.md](crates/windows-fil | Path to CHECKLIST.md | Status | Brief description | Design Notes | |---|---|---|---| -| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0, which currently exists only in design notes with no live checklist item. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) for M19-M22; M30 has no decision recorded yet, which is the point of M30.5 | +| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0: it was previously untracked, referenced from that crate's design notes, a source file and its sabotage manifest with no live checklist item anywhere, and is now queued as M30.4. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) for M19-M22; [DESIGN-NOTES.md](DESIGN-NOTES.md#machine-checking-what-is-argued) for M30's rationale -- its decision is not recorded yet, which is what M30.5 produces | | [CHECKLIST-thread-ambient.md](CHECKLIST-thread-ambient.md) | in progress | M22-M23: extract the captured-context composite into `windows-thread-ambient-sys`, a standalone platform layer that captures a thread's ambient state and applies it on another thread. M24-M26: `windows-namespace-request-sys`, marshalable Win32 namespace call parameter sets, over a round-one entry list audited from three real consumers (this repository's watcher and enumeration crates, and `MikeGrier/Globazog-rs`) rather than guessed. M27: `windows-platform-probes`, a durable home for the measurements this workspace's designs rest on, under a three-tier scheme (asserted / ignored / binary-only) where every tier is compiled by an ordinary build. Feature-scoped and deleted when complete; it is the whole of the `mikegrier/thread-ambient` branch's work, and is deliberately separate from the deferred namespace-facility items in [CHECKLIST.md](CHECKLIST.md). | [crates/windows-thread-ambient-sys/DESIGN-NOTES.md](crates/windows-thread-ambient-sys/DESIGN-NOTES.md) | | [crates/windows-overlapped-io-sys/CHECKLIST.md](crates/windows-overlapped-io-sys/CHECKLIST.md) | not started | M14: finish the contract audit -- categories 1, 2, 6, 8, 9 were not examined -- and sweep `outstanding()` for the advisory-predicate hazard. | [crates/windows-overlapped-io-sys/DESIGN-NOTES.md](crates/windows-overlapped-io-sys/DESIGN-NOTES.md) | | [crates/windows-ioring-sys/CHECKLIST.md](crates/windows-ioring-sys/CHECKLIST.md) | in progress | Memory-safe Rust over the Windows `IoRing` submission/completion ring, as a new crate. M1-M7 (ring lifecycle through the `ring-copy` topology-aligned sample) are complete and archived. The parked, pinned-thread `M6+` work and the new M10 contract audit remain. | [crates/windows-ioring-sys/DESIGN-NOTES.md](crates/windows-ioring-sys/DESIGN-NOTES.md) | diff --git a/crates/windows-waitable-queues/PLANS.md b/crates/windows-waitable-queues/PLANS.md index 85f260f4f..0d8da4538 100644 --- a/crates/windows-waitable-queues/PLANS.md +++ b/crates/windows-waitable-queues/PLANS.md @@ -5,5 +5,4 @@ in [COMPLETED-PLANS.md](COMPLETED-PLANS.md). | Path to CHECKLIST.md | Status | Brief description | Design Notes | |---|---|---|---| - -No checklist is open against this crate. +| [../../CHECKLIST.md](../../CHECKLIST.md) | not started | M30.4: re-home `M31.6`, the `loom` verification this crate's design notes reference in three places and its README promises adopters before 1.0, which had no live checklist item anywhere. Scope as [D-31](DESIGN-NOTES.md#d-31) describes it -- both MPSC shapes or neither -- and repoint all five references, which are in [DESIGN-NOTES.md](DESIGN-NOTES.md), [src/doorbell.rs](src/doorbell.rs) and [sabotage.json](sabotage.json). M30.5 may also oblige a sweep of this crate's three public promises of verification before 1.0, whichever way that decision goes. | [DESIGN-NOTES.md](DESIGN-NOTES.md#d-31), [../../DESIGN-NOTES.md](../../DESIGN-NOTES.md#machine-checking-what-is-argued) | From 45a184964579deb19fffa1322defd7a373aca624 Mon Sep 17 00:00:00 2001 From: Mike Grier Date: Tue, 15 Sep 2026 17:52:33 -0700 Subject: [PATCH 6/9] docs: move M30's rationale to Tier 2, where pre-decision context belongs Five findings. Two were claims I made about mechanisms without checking them. The rationale was in DESIGN-NOTES.md, which is the current-decision tier. No decision has been taken -- M30.5 is what produces one, and "adopt nothing" is a legitimate result -- so a reader could take queued context for an adopted contract. Moved wholesale to DESIGN-RATIONALE.md, which already exists at the root with design-sessions beside it. DESIGN-NOTES.md is now byte-identical to its pre-M30 state: the diff is a pure removal with no additions. The checklist still carried the model-selection argument and the tool taxonomy after last round moved the framing out. Both are rationale, and leaving them made the checklist a second source of design context able to drift from the first -- in a milestone whose own M30.5 names exactly that drift as the cost to watch. M30.1 and M30.2 are now deliverables plus numbered done-when criteria; everything that argues rather than instructs is in Tier 2. M30.3 offered "make one derive from the other" for the two copies of the memory orderings disclosure, on the grounds that the README is already a build input. Checked: the include_str is `#[cfg(all(doctest, windows))]` on a private ReadmeDoctests item, so it compiles the README's CODE as doctests and does not render its prose into the crate docs. The option does not exist with today's mechanism, and choosing it would have left both copies able to drift while looking addressed. The item now requires both, and says what making one derive would actually cost. The rationale asserted that D-31's objection is that "a model checker covers atomics and cannot cover SetEvent". That is wrong for TLA+, whose actions are atomic by construction and which has no memory model to cover atomics WITH -- and TLA+ is the first tool class M30.1 surveys, so the survey would have started from a false premise about its own leading candidate. The tool-independent part of D-31's objection is only the syscall boundary; how much of the atomics a tool sees is precisely what M30.1 is for. The crate tracker said M30.5 "may also oblige" the contract sweep where the checklist says either outcome obliges it. A tracker that weakens a required follow-up can be read as complete without it. Corrected to match. Repointing the rationale also required both PLANS.md rows, which cited the old DESIGN-NOTES anchor -- found by sweeping the anchor rather than by editing the files the review named. All 121 relative links across the five files verified for file and anchor resolution. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- CHECKLIST.md | 78 ++++++++---------- DESIGN-NOTES.md | 66 ---------------- DESIGN-RATIONALE.md | 100 ++++++++++++++++++++++++ PLANS.md | 2 +- crates/windows-waitable-queues/PLANS.md | 2 +- 5 files changed, 133 insertions(+), 115 deletions(-) diff --git a/CHECKLIST.md b/CHECKLIST.md index 5ec18b800..c4d4ebd0f 100644 --- a/CHECKLIST.md +++ b/CHECKLIST.md @@ -187,10 +187,11 @@ written before it was stated. ## M30 -- Find out how much of this workspace's algorithm correctness can be machine-checked -Why this milestone exists, what it is not, and how it relates to -[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) are recorded in -[DESIGN-NOTES.md](DESIGN-NOTES.md#machine-checking-what-is-argued) rather than here, per the -action-only rule for checklist files. +Rationale -- why this milestone exists, which tool classes are in scope and what each can see, why +`SH-14.1` is the pilot, and how this relates to +[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) -- is in +[DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#machine-checking-what-is-argued). No decision is recorded +yet; `M30.5` produces it. - [ ] **M30.1** -- Survey the workspace for algorithms whose correctness is currently argued rather than checked, and match each to the class of tool that could check it. @@ -200,46 +201,25 @@ action-only rule for checklist files. flag against `SetEvent`/`ResetEvent`; `windows-file-watcher`'s contract state machine; `windows-ioring-sys`' submission/completion ring. - For each, record which of these fits and why: **TLA+/PlusCal** (protocol-level, exhaustive over a - small configuration, no memory model -- its actions are atomic and interleaved, which is sequential - consistency); **loom** (actual Rust under the C11 memory model, which is where the measured - weakened-`Acquire` blind spot lives); **kani or similar bounded proof** (Rust, memory-safety and - assertion checking); **`const` assertions** (arithmetic relationships between constants, already - used here and the cheapest of the four, because they fail the build rather than a run somebody - chose to make). - - The output is a table, and the "no tool fits this" rows are as valuable as the rest. - -- [ ] **M30.2** -- Pilot exactly one, chosen because parameter shrinking turns an untestable property - into an exhaustive one. - - `reserving_mpsc`'s claim-position recurrence (`SH-14.1`) is the strongest candidate, and the reason - is the interleaving rather than the count. Reaching the wrap takes 2^32 pushes -- about 37 seconds - of sustained maximum-rate pushing on the host the crate publishes, which is far outside a unit - suite budgeted in milliseconds but is not in itself beyond a long integration test. What is beyond - any test is the rest of the condition: - [crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) records that - reaching the wrap is necessary but *not sufficient* -- a producer must also be stalled inside a - window a few instructions wide, and no test can schedule that deliberately. A model whose position - wraps at 8 makes the whole interleaving reachable in seconds and *exhaustive* rather than sampled, - and yields a counterexample trace rather than a suspicion. - - **Write down what makes the wrap-at-8 model evidence about `Balanced`, or record that it is not.** - Shrinking the position to 3 bits is a claim that the protocol's correctness does not depend on the - field's width -- that the shipping code refines the model. State that correspondence explicitly: - which constants were shrunk, why the protocol is uniform in each, and what a counterexample at 8 - therefore implies at 2^32. If it cannot be argued, the pilot's result is a counterexample *in a toy - model* and must be reported as exactly that. - - **Success needs both halves.** The unmodified model must satisfy its invariant, *and* a - deliberately broken variant must produce a counterexample. Neither alone is enough: a green run on - the correct model says nothing if the model is too permissive or the invariant vacuous, and a - counterexample from the broken variant can also be produced by a malformed model that would find - one anywhere. The first is the property check; the second is the anti-vacuity check. - - Not a candidate: `capacity == 1`. It belongs to `slotwise_mpsc`'s slot sequence protocol - ([D-12](crates/windows-waitable-queues/DESIGN-NOTES.md#d-12)), not to `reserving_mpsc`'s claim - position, and is already resolved by that shape refusing a capacity below two. + Tool classes to match against: TLA+/PlusCal, loom, a bounded proof such as kani, and `const` + assertions. What each can and cannot see is in the rationale. + + Done when: a table exists with one row per algorithm, each naming a tool class or "none fits" and + why. The "none fits" rows count as output, not as gaps in the survey. + +- [ ] **M30.2** -- Pilot exactly one: `reserving_mpsc`'s claim-position recurrence (`SH-14.1`). + + Done when all three hold: + + 1. **The refinement is stated.** Which constants were shrunk, why the protocol is uniform in each, + and what a counterexample at the reduced width implies at the shipping width. If it cannot be + argued, the result is reported as a counterexample *in a toy model* and nothing more. + 2. **The unmodified model satisfies its invariant** -- the property check. + 3. **A deliberately broken variant produces a counterexample** -- the anti-vacuity check. Neither + 2 nor 3 alone is sufficient. + + Not a candidate: `capacity == 1`, which belongs to `slotwise_mpsc` + ([D-12](crates/windows-waitable-queues/DESIGN-NOTES.md#d-12)) and is already resolved. - [ ] **M30.3** -- Write down what the pilot could NOT reach, by name. @@ -252,9 +232,13 @@ action-only rule for checklist files. "How far the memory orderings are verified, and how far they are not" section. **That section has two copies**, [that crate's README.md](crates/windows-waitable-queues/README.md) and [its src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and updating one would leave the other - telling an adopter something the crate no longer believes. Update both, or make one derive from the - other -- the README is already a build input via `#[doc = include_str!]`, so the second option is - available and is the one that cannot drift. + telling an adopter something the crate no longer believes. Update both. + + Deriving one from the other is **not** available with the mechanism that exists today: the + `#[doc = include_str!("../README.md")]` in that crate is `#[cfg(all(doctest, windows))]` on a + private `ReadmeDoctests` item, so it compiles the README's *code* as doctests and does not render + its prose into the crate documentation. Making one derive would mean introducing a shared fragment + both include, which is a separate piece of work and not a shortcut available to this item. - [ ] **M30.4** -- Re-home `M31.6`, which is currently orphaned. diff --git a/DESIGN-NOTES.md b/DESIGN-NOTES.md index fa42efacb..451807850 100644 --- a/DESIGN-NOTES.md +++ b/DESIGN-NOTES.md @@ -1909,69 +1909,3 @@ that has never been wrong while leaving the prose that keeps being wrong in prop was taken, which findings it is drawn from, what was rejected on the way, and the one cheap remedy that was costed but not adopted are in [DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#why-restatement-count-is-what-is-watched). - -## Machine-checking what is currently argued: why M30 exists and what it is not - -Context for [CHECKLIST.md](CHECKLIST.md) -> `M30`. It lives here rather than in the checklist -because a checklist is an action queue, and this is rationale. - -**What checks this workspace's concurrency today.** Reasoning recorded beside the code, an extensive -unit suite, a sabotage suite that injects defects and requires each to be caught, and a -cargo-mutants sweep. That combination is not weak, and it has found real bugs -- -[D-15](crates/windows-waitable-queues/DESIGN-NOTES.md#d-15)'s lost wakeup among them. - -**It has a measured blind spot, and the measurement is the reason for the milestone.** -[crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) records that -weakening a producer's `Acquire` load of the consumer's position to `Relaxed` left the entire suite -green, while every *logic* defect injected beside it was caught. That asymmetry is not a gap in the -suite's thoroughness; it is what a test is. A test observes what a run happened to do, and cannot -observe an ordering that a run happened not to need. - -The general form of that asymmetry -- classes with an oracle converge, classes without one do not -- -is worth keeping in view when reading the survey's results. Memory ordering has no oracle here. - -**The goal is to narrow where hand-inspection has to look, not to replace it.** A method that proves -a protocol correct for three producers and a capacity of two does not prove the shipping code -correct. What it does is move a class of question out of "argued carefully" and into "checked", so -that what remains uncheckable is a short, named list rather than the whole surface. **That list is -the deliverable**, which is why `M30.3` is the item the milestone exists for rather than a tidying -step after the pilot. Formal methods here are a scoping instrument. - -**This does not commit the workspace to any tool, and must not pre-empt -[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31)**, which decided on considered grounds -that 0.1.0 ships without machine-checked orderings. D-31's reasoning is the starting point rather -than something to overturn, and its central objection survives any tool choice: a model checker -covers atomics and cannot cover `SetEvent`/`ResetEvent`, so stubbing them verifies a model of -`SetEvent` rather than `SetEvent` itself. That is the "measures the model, not the thing" trap this -workspace has already been caught by once, and the doorbell is precisely where its one real ordering -bug lived. Any tool the milestone recommends has to be read against that. - -**The same trap has a second costume, which `M30.2` now guards against explicitly.** Shrinking a -model's parameters -- a position that wraps at 8 rather than 2^32 -- is itself a claim: that the -protocol's correctness does not depend on the width of that field. If nobody states why the shipping -code refines the reduced model, a green run proves something about the model alone. A reduced model -that has not been tied to the code can pass and mean nothing. - -**No decision is recorded here yet.** This section is context for queued work, not an outcome; -`M30.5` is what produces the decision, and "adopt nothing, and say why" remains a legitimate result -of it. - -### Two corrections the milestone's own drafting needed - -Recorded because both were errors in the *argument for* the pilot rather than in the plan, and a -reader taking them on trust would have aimed the pilot wrongly. - -**The untestability was mis-attributed to the count.** The first draft said `SH-14.1` "needs 2^32 -pushes to manifest and is therefore beyond any test". Both halves were wrong. 2^32 pushes is about 37 -seconds of sustained maximum-rate pushing on the host the queue crate publishes -- outside a unit -suite budgeted in milliseconds, but not beyond a long integration test. And the count was never the -reason: reaching the wrap is necessary but *not sufficient*, because a producer must also be stalled -inside a window a few instructions wide. That is what no test can schedule. The corrected reading -argues the pilot better, because parameter shrinking then earns its place by making the interleaving -*exhaustive* rather than by making a count small. - -**The success criterion was half a criterion.** The first draft asked for a counterexample from a -deliberately broken variant and explicitly *not* a green run on the correct one -- an overcorrection -against vacuous green runs. But a counterexample from a broken variant can equally be produced by a -malformed or over-permissive model that would find one anywhere, so it is an anti-vacuity check, not -a property check. Both are required, and the item now says so. diff --git a/DESIGN-RATIONALE.md b/DESIGN-RATIONALE.md index cce9fa325..2fc6019ea 100644 --- a/DESIGN-RATIONALE.md +++ b/DESIGN-RATIONALE.md @@ -447,3 +447,103 @@ prose-reduction pass is adopted, each needs its own item at that time. - [`SubmitThreadpoolWork`](https://learn.microsoft.com/windows/win32/api/threadpoolapiset/nf-threadpoolapiset-submitthreadpoolwork) - [WIL token helpers](https://github.com/microsoft/wil/blob/master/include/wil/token_helpers.h) - [`GetFileInformationByHandleEx`](https://learn.microsoft.com/windows/win32/api/fileapi/nf-fileapi-getfileinformationbyhandleex) + +## Why M30 exists, what it is not, and how the pilot was chosen + +Rationale for [CHECKLIST.md](CHECKLIST.md) -> `M30`. It is here, in Tier 2, rather than in +[DESIGN-NOTES.md](DESIGN-NOTES.md), because **no decision has been taken**: `M30.5` is what produces +one, and "adopt nothing, and say why" remains a legitimate result. Tier 1 records current decisions, +and recording pre-decision context there would let a reader mistake it for an adopted contract. + +### What checks this workspace's concurrency today + +Reasoning recorded beside the code, an extensive unit suite, a sabotage suite that injects defects +and requires each to be caught, and a cargo-mutants sweep. That combination is not weak, and it has +found real bugs -- [D-15](crates/windows-waitable-queues/DESIGN-NOTES.md#d-15)'s lost wakeup among +them. + +### The measured blind spot, which is the reason for the milestone + +[crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) records that +weakening a producer's `Acquire` load of the consumer's position to `Relaxed` left the entire suite +green, while every *logic* defect injected beside it was caught. That asymmetry is not a gap in the +suite's thoroughness; it is what a test is. A test observes what a run happened to do, and cannot +observe an ordering that a run happened not to need. + +The general form is worth keeping in view when reading the survey's results: classes with an oracle +converge, classes without one do not. Memory ordering has no oracle here. + +### The goal is to narrow where hand-inspection has to look, not to replace it + +A method that proves a protocol correct for three producers and a capacity of two does not prove the +shipping code correct. What it does is move a class of question out of "argued carefully" and into +"checked", so that what remains uncheckable is a short, named list rather than the whole surface. +**That list is the deliverable**, which is why `M30.3` is the item the milestone exists for rather +than a tidying step after the pilot. Formal methods here are a scoping instrument. + +### The tool classes, and what each can and cannot see + +- **TLA+/PlusCal** -- protocol-level, exhaustive over a small configuration. Its actions are atomic + and interleaved, which is sequential consistency: it has **no memory model at all**, so it cannot + see a weakened ordering. It checks the protocol, not the code that implements it. +- **loom** -- actual Rust under the C11 memory model, which is exactly where the measured + weakened-`Acquire` blind spot lives. +- **kani or similar bounded proof** -- Rust, memory-safety and assertion checking. +- **`const` assertions** -- arithmetic relationships between constants. Already used here, and the + cheapest of the four, because they fail the build rather than a run somebody chose to make. + +### Why `SH-14.1` is the pilot, and why the reason is not the count + +Reaching the claim position's wrap takes 2^32 pushes -- about 37 seconds of sustained maximum-rate +pushing on the host the queue crate publishes. That is far outside a unit suite budgeted in +milliseconds, but it is not in itself beyond a long integration test, so "beyond any test" would +overstate it. + +What is beyond any test is the rest of the condition. The crate's README records that reaching the +wrap is necessary but *not sufficient*: a producer must also be stalled inside a window a few +instructions wide, and no test can schedule that deliberately. A model whose position wraps at 8 +makes the whole interleaving reachable in seconds and **exhaustive** rather than sampled, and yields +a counterexample trace rather than a suspicion. Parameter shrinking earns its place by making the +interleaving exhaustive, not by making a count small. + +`capacity == 1` was offered as a second candidate in an early draft and is not one. It belongs to +`slotwise_mpsc`'s slot *sequence* protocol +([D-12](crates/windows-waitable-queues/DESIGN-NOTES.md#d-12)), not to `reserving_mpsc`'s claim +position, and is already resolved by that shape refusing a capacity below two. + +### This must not pre-empt D-31 + +[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) decided on considered grounds that 0.1.0 +ships without machine-checked orderings. Its reasoning is the starting point rather than something to +overturn, and its central objection survives any tool choice: **no candidate models the real +`SetEvent`/`ResetEvent` calls**, so stubbing them verifies a model of `SetEvent` rather than +`SetEvent` itself. That is the "measures the model, not the thing" trap this workspace has already +been caught by once, and the doorbell is precisely where its one real ordering bug lived. + +An earlier version of this section said the objection was that "a model checker covers atomics and +cannot cover `SetEvent`" -- which is wrong for TLA+, whose actions are atomic by construction and +which has no memory model to cover atomics *with*. The tool-independent part of D-31's objection is +only the syscall boundary; how much of the atomics a tool sees is exactly what `M30.1` is for. + +### The same trap has a second costume + +Shrinking a model's parameters -- a position that wraps at 8 rather than 2^32 -- is itself a claim: +that the protocol's correctness does not depend on the width of that field. If nobody states why the +shipping code refines the reduced model, a green run proves something about the model alone. A +reduced model that has not been tied to the code can pass and mean nothing. `M30.2` carries that as +an acceptance criterion. + +### Two corrections the milestone's own drafting needed + +Both were errors in the argument *for* the pilot rather than in the plan, so a reader taking them on +trust would have aimed the pilot wrongly. + +**The untestability was mis-attributed to the count.** The first draft said `SH-14.1` "needs 2^32 +pushes to manifest and is therefore beyond any test". Corrected above: the count is reachable, and +the stall window is what is not. + +**The success criterion was half a criterion.** The first draft asked for a counterexample from a +deliberately broken variant and explicitly *not* a green run on the correct one -- an overcorrection +against vacuous green runs. A counterexample from a broken variant can equally be produced by a +malformed or over-permissive model that would find one anywhere, so it is an anti-vacuity check, not +a property check. Both are required. diff --git a/PLANS.md b/PLANS.md index d78dc3a98..fcba033c1 100644 --- a/PLANS.md +++ b/PLANS.md @@ -16,7 +16,7 @@ plans tracker: [crates/windows-file-enumeration-sys/PLANS.md](crates/windows-fil | Path to CHECKLIST.md | Status | Brief description | Design Notes | |---|---|---|---| -| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0: it was previously untracked, referenced from that crate's design notes, a source file and its sabotage manifest with no live checklist item anywhere, and is now queued as M30.4. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) for M19-M22; [DESIGN-NOTES.md](DESIGN-NOTES.md#machine-checking-what-is-argued) for M30's rationale -- its decision is not recorded yet, which is what M30.5 produces | +| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0: it was previously untracked, referenced from that crate's design notes, a source file and its sabotage manifest with no live checklist item anywhere, and is now queued as M30.4. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) for M19-M22; [DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#machine-checking-what-is-argued) for M30's rationale (Tier 2, since no decision is taken yet) -- its decision is not recorded yet, which is what M30.5 produces | | [CHECKLIST-thread-ambient.md](CHECKLIST-thread-ambient.md) | in progress | M22-M23: extract the captured-context composite into `windows-thread-ambient-sys`, a standalone platform layer that captures a thread's ambient state and applies it on another thread. M24-M26: `windows-namespace-request-sys`, marshalable Win32 namespace call parameter sets, over a round-one entry list audited from three real consumers (this repository's watcher and enumeration crates, and `MikeGrier/Globazog-rs`) rather than guessed. M27: `windows-platform-probes`, a durable home for the measurements this workspace's designs rest on, under a three-tier scheme (asserted / ignored / binary-only) where every tier is compiled by an ordinary build. Feature-scoped and deleted when complete; it is the whole of the `mikegrier/thread-ambient` branch's work, and is deliberately separate from the deferred namespace-facility items in [CHECKLIST.md](CHECKLIST.md). | [crates/windows-thread-ambient-sys/DESIGN-NOTES.md](crates/windows-thread-ambient-sys/DESIGN-NOTES.md) | | [crates/windows-overlapped-io-sys/CHECKLIST.md](crates/windows-overlapped-io-sys/CHECKLIST.md) | not started | M14: finish the contract audit -- categories 1, 2, 6, 8, 9 were not examined -- and sweep `outstanding()` for the advisory-predicate hazard. | [crates/windows-overlapped-io-sys/DESIGN-NOTES.md](crates/windows-overlapped-io-sys/DESIGN-NOTES.md) | | [crates/windows-ioring-sys/CHECKLIST.md](crates/windows-ioring-sys/CHECKLIST.md) | in progress | Memory-safe Rust over the Windows `IoRing` submission/completion ring, as a new crate. M1-M7 (ring lifecycle through the `ring-copy` topology-aligned sample) are complete and archived. The parked, pinned-thread `M6+` work and the new M10 contract audit remain. | [crates/windows-ioring-sys/DESIGN-NOTES.md](crates/windows-ioring-sys/DESIGN-NOTES.md) | diff --git a/crates/windows-waitable-queues/PLANS.md b/crates/windows-waitable-queues/PLANS.md index 0d8da4538..e7b54cbc7 100644 --- a/crates/windows-waitable-queues/PLANS.md +++ b/crates/windows-waitable-queues/PLANS.md @@ -5,4 +5,4 @@ in [COMPLETED-PLANS.md](COMPLETED-PLANS.md). | Path to CHECKLIST.md | Status | Brief description | Design Notes | |---|---|---|---| -| [../../CHECKLIST.md](../../CHECKLIST.md) | not started | M30.4: re-home `M31.6`, the `loom` verification this crate's design notes reference in three places and its README promises adopters before 1.0, which had no live checklist item anywhere. Scope as [D-31](DESIGN-NOTES.md#d-31) describes it -- both MPSC shapes or neither -- and repoint all five references, which are in [DESIGN-NOTES.md](DESIGN-NOTES.md), [src/doorbell.rs](src/doorbell.rs) and [sabotage.json](sabotage.json). M30.5 may also oblige a sweep of this crate's three public promises of verification before 1.0, whichever way that decision goes. | [DESIGN-NOTES.md](DESIGN-NOTES.md#d-31), [../../DESIGN-NOTES.md](../../DESIGN-NOTES.md#machine-checking-what-is-argued) | +| [../../CHECKLIST.md](../../CHECKLIST.md) | not started | M30.4: re-home `M31.6`, the `loom` verification this crate's design notes reference in three places and its README promises adopters before 1.0, which had no live checklist item anywhere. Scope as [D-31](DESIGN-NOTES.md#d-31) describes it -- both MPSC shapes or neither -- and repoint all five references, which are in [DESIGN-NOTES.md](DESIGN-NOTES.md), [src/doorbell.rs](src/doorbell.rs) and [sabotage.json](sabotage.json). M30.5 also obliges a sweep of this crate's three public promises of verification before 1.0, whichever way that decision goes. | [DESIGN-NOTES.md](DESIGN-NOTES.md#d-31), [../../DESIGN-RATIONALE.md](../../DESIGN-RATIONALE.md#machine-checking-what-is-argued) | From 562bc6db3538a16c278246e434ecd1c24e2194d7 Mon Sep 17 00:00:00 2001 From: Mike Grier Date: Tue, 15 Sep 2026 18:02:07 -0700 Subject: [PATCH 7/9] docs: attribute the shape scope to D-29, and stop overstating what two tools see Seven findings. Two were wrong attributions, two overstated a tool's reach, and one was a trim I did by halves last round. M30.4 and the crate tracker both said the loom verification's "both MPSC shapes or neither" scope is what D-31 describes. It is not. That obligation is D-29's, recorded in its "The obligation this creates" section -- verified by locating the sentence and walking back to its owning heading. D-31 owns only the release timing, that verification gates 1.0 rather than 0.1.0. An implementer following the citation would have read the wrong decision for the acceptance criterion they were trying to satisfy. Both sites now cite D-29 for the scope and keep D-31 for the timing. The rationale called loom "actual Rust under the C11 memory model". It is an instrumented code-level model: the crate's logic runs, but the synchronization primitives are substituted for loom's instrumented types and the Windows calls are not executed as written. Overstating it blurred exactly the model-to-code gap that M30.2's refinement criterion and M30.3's could-not-reach list exist to record -- so the overstatement undercut two items in the same milestone. The same paragraph said TLA+ has "no memory model at all", which last round's fix introduced while correcting the opposite error. It is too absolute: TLA+ has no BUILT-IN hardware memory model and its ordinary interleaved-action semantics is sequentially consistent, but a specification can model weak-memory reordering explicitly. What it checks then is the modelled protocol rather than the emitted code, so the model-to-code gap survives either way. Stated that way, because M30.1 uses this distinction to decide what the survey can cover and a flat "no memory model" would rule out a legitimate approach. M30.3's could-not-reach list preclassified anything scheduler-dependent as unreachable. loom explores scheduler interleavings deliberately, so that would have recorded a false gap in the item whose whole output is the gap list. It now scopes the list to what the SELECTED tool cannot model, and says so. Last round trimmed M30.1 and M30.2 to deliverables and done-when criteria and left M30.3, M30.4 and M30.5 carrying their rationale -- a trim done by halves that made the checklist look action-only while three of five items were not. All five are now deliverables plus numbered done-when criteria. The root tracker's inventory of component trackers omitted the queue crate's. Sweeping the inventory rather than adding the named entry found a second omission the review did not report: windows-file-watcher-example-test-harness. Both added; the inventory now lists 13 of 13, checked by diffing it against `git ls-files`. All 123 relative links across the five files verified for file and anchor resolution. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- CHECKLIST.md | 100 ++++++++++-------------- DESIGN-RATIONALE.md | 29 +++++-- PLANS.md | 4 +- crates/windows-waitable-queues/PLANS.md | 2 +- 4 files changed, 67 insertions(+), 68 deletions(-) diff --git a/CHECKLIST.md b/CHECKLIST.md index c4d4ebd0f..4f8efc594 100644 --- a/CHECKLIST.md +++ b/CHECKLIST.md @@ -221,71 +221,55 @@ yet; `M30.5` produces it. Not a candidate: `capacity == 1`, which belongs to `slotwise_mpsc` ([D-12](crates/windows-waitable-queues/DESIGN-NOTES.md#d-12)) and is already resolved. -- [ ] **M30.3** -- Write down what the pilot could NOT reach, by name. - - This is the item the milestone exists for. Expect the list to include: the memory orderings, if the - tool has no memory model; every syscall boundary, including the doorbell's; anything whose - correctness depends on the allocator, the scheduler, or real time; and the gap between the model - and the code, which no tool closes. - - Put it where a reader deciding how much to trust the crate will meet it -- beside the existing - "How far the memory orderings are verified, and how far they are not" section. **That section has - two copies**, [that crate's README.md](crates/windows-waitable-queues/README.md) and - [its src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and updating one would leave the other - telling an adopter something the crate no longer believes. Update both. - - Deriving one from the other is **not** available with the mechanism that exists today: the - `#[doc = include_str!("../README.md")]` in that crate is `#[cfg(all(doctest, windows))]` on a - private `ReadmeDoctests` item, so it compiles the README's *code* as doctests and does not render - its prose into the crate documentation. Making one derive would mean introducing a shared fragment - both include, which is a separate piece of work and not a shortcut available to this item. +- [ ] **M30.3** -- Write down what the pilot could NOT reach, by name. This is the item the milestone + exists for. + + Done when both hold: + + 1. **The list names only what the *selected* tool cannot model**, not what tools in general cannot. + Expect the syscall boundary including the doorbell's, real-time behaviour, and the model-to-code + gap that no tool closes. Do **not** preclassify scheduler-dependence: loom explores scheduler + interleavings deliberately, so recording it as unreachable would be a false gap. Whether the + memory orderings are reachable likewise depends on which tool M30.1 selected. + 2. **Both copies of the disclosure are updated** -- the "How far the memory orderings are verified, + and how far they are not" section exists in + [that crate's README.md](crates/windows-waitable-queues/README.md) and + [its src/lib.rs](crates/windows-waitable-queues/src/lib.rs). Deriving one from the other is not + available today: the `include_str!` there is `#[cfg(all(doctest, windows))]` on a private item, + so it compiles the README's code as doctests and does not render its prose. Making one derive + would mean a shared fragment both include, which is separate work. - [ ] **M30.4** -- Re-home `M31.6`, which is currently orphaned. - `windows-waitable-queues`' design notes reference `M31.6` in three places as the planned `loom` - verification, and [crates/windows-waitable-queues/README.md](crates/windows-waitable-queues/README.md) - tells adopters it is planned before 1.0. Until this item, there was no live checklist item for it - anywhere in the repository -- the crate has only a - [COMPLETED-CHECKLIST.md](crates/windows-waitable-queues/COMPLETED-CHECKLIST.md). That was the - "design notes are not a work queue" failure the repository instructions name: a public commitment - that nothing will cause anyone to pick up. - - Give it a real item in a real checklist, with its scope as D-31 describes it (both MPSC shapes or - neither), and repoint every reference at it. **There are five, not three**: three in - [that crate's DESIGN-NOTES.md](crates/windows-waitable-queues/DESIGN-NOTES.md), one in - [src/doorbell.rs](crates/windows-waitable-queues/src/doorbell.rs), and one in - [sabotage.json](crates/windows-waitable-queues/sabotage.json). Sweeping only the design notes would - leave a stale identifier in a source file and in the sabotage manifest -- the same - fix-the-reported-site-not-the-class failure this repository keeps paying for. - - Opening queue work also obliges the component tracker. That row is added in this change rather than - deferred to this item, because - [crates/windows-waitable-queues/PLANS.md](crates/windows-waitable-queues/PLANS.md)'s "No checklist - is open against this crate" stops being true the moment M30.4 is queued, not when it is completed. - What remains for this item is to keep that row accurate as the work proceeds. + Done when all three hold: + + 1. **It has a live item in a live checklist**, scoped as + [D-29](crates/windows-waitable-queues/DESIGN-NOTES.md#d-29) requires -- the loom verification + covers both MPSC shapes or neither is verified. (D-29 owns that obligation; + [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) owns only the release timing, that + verification gates 1.0 rather than 0.1.0.) + 2. **All five references point at it.** Three in + [that crate's DESIGN-NOTES.md](crates/windows-waitable-queues/DESIGN-NOTES.md), one in + [src/doorbell.rs](crates/windows-waitable-queues/src/doorbell.rs), one in + [sabotage.json](crates/windows-waitable-queues/sabotage.json). + 3. **The component tracker row stays accurate** as the work proceeds. The row itself was added + when the work was queued, not deferred to this item. - [ ] **M30.5** -- Decide what, if anything, the workspace adopts, and record the decision with its cost. - The cost to name explicitly, because it is the one this workspace keeps paying: **a specification is - another statement of the contract, and it can drift from the code with nothing to detect it.** That - is the restatement-drift problem in - [.github/copilot-instructions.md](.github/copilot-instructions.md)'s CONTRACT INTEGRITY section, - applied to an artefact that is harder to keep honest than prose because it looks authoritative. A - stale model that still passes is worse than no model. - - So the decision has to answer: what keeps the model and the code in step, who re-runs it, and what - happens when they disagree. "Adopt nothing, and say why" is a legitimate outcome -- D-31 reached it - once already on narrower grounds. - - **Either outcome obliges a contract sweep, and a no-adoption outcome obliges it most.** Three - public places in `windows-waitable-queues` promise machine-checked verification before 1.0: - [that crate's README.md](crates/windows-waitable-queues/README.md), - [its src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and D-31 in - [its DESIGN-NOTES.md](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Deciding to adopt nothing - without reconciling those leaves the crate promising adopters something no item will deliver -- - which is the failure M30.4 exists to fix, recreated by the milestone that fixed it. Sweep all three - as part of this item, whichever way it goes. + Done when both hold: + + 1. **The decision answers three questions**: what keeps the model and the code in step, who + re-runs it, and what happens when they disagree. "Adopt nothing, and say why" is a legitimate + outcome. + 2. **The contract sweep is done, whichever way it went.** Three public places in + `windows-waitable-queues` promise machine-checked verification before 1.0: + [that crate's README.md](crates/windows-waitable-queues/README.md), + [its src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and + [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). A no-adoption outcome obliges this + most: left unswept it would recreate, in the same crate, the orphaned commitment M30.4 exists + to fix. ## M-inf -- Parked diff --git a/DESIGN-RATIONALE.md b/DESIGN-RATIONALE.md index 2fc6019ea..53984d461 100644 --- a/DESIGN-RATIONALE.md +++ b/DESIGN-RATIONALE.md @@ -483,11 +483,22 @@ than a tidying step after the pilot. Formal methods here are a scoping instrumen ### The tool classes, and what each can and cannot see -- **TLA+/PlusCal** -- protocol-level, exhaustive over a small configuration. Its actions are atomic - and interleaved, which is sequential consistency: it has **no memory model at all**, so it cannot - see a weakened ordering. It checks the protocol, not the code that implements it. -- **loom** -- actual Rust under the C11 memory model, which is exactly where the measured - weakened-`Acquire` blind spot lives. +- **TLA+/PlusCal** -- protocol-level, exhaustive over a small configuration. It has **no built-in + hardware memory model**, and its ordinary interleaved-action semantics is sequential consistency, + so by default it cannot see a weakened ordering. That is a property of the default model rather + than an absolute limit: a specification *can* model weak-memory reordering explicitly, with store + buffers or a reordering relation written into the spec. What it still checks in that case is the + protocol as written, not the orderings the Rust implementation actually emits -- so the + model-to-code gap remains, and `M30.1` should record which of the two is meant rather than + treating "no memory model" as settled. +- **loom** -- an instrumented code-level model. It runs the crate's own logic, but the + synchronization primitives must be substituted for `loom`'s instrumented types, and loom then + explores the executions the C11 model permits. That is much closer to the code than a protocol + spec, and it is where the measured weakened-`Acquire` blind spot lives -- but it is still a model: + what runs under loom is not the shipping binary, and the Windows calls are not executed as + written. An earlier version of this line called it "actual Rust under the C11 memory model", which + overstated the guarantee and blurred exactly the model-to-code gap `M30.2` and `M30.3` exist to + record. - **kani or similar bounded proof** -- Rust, memory-safety and assertion checking. - **`const` assertions** -- arithmetic relationships between constants. Already used here, and the cheapest of the four, because they fail the build rather than a run somebody chose to make. @@ -521,9 +532,11 @@ overturn, and its central objection survives any tool choice: **no candidate mod been caught by once, and the doorbell is precisely where its one real ordering bug lived. An earlier version of this section said the objection was that "a model checker covers atomics and -cannot cover `SetEvent`" -- which is wrong for TLA+, whose actions are atomic by construction and -which has no memory model to cover atomics *with*. The tool-independent part of D-31's objection is -only the syscall boundary; how much of the atomics a tool sees is exactly what `M30.1` is for. +cannot cover `SetEvent`" -- which is wrong for TLA+, whose ordinary interleaved-action semantics is +sequentially consistent and which has no *built-in* memory model to cover atomics with (a spec can +model reordering explicitly, but then it checks the modelled protocol rather than the emitted code). +The tool-independent part of D-31's objection is only the syscall boundary; how much of the atomics +a tool sees is exactly what `M30.1` is for. ### The same trap has a second costume diff --git a/PLANS.md b/PLANS.md index fcba033c1..43d67ff41 100644 --- a/PLANS.md +++ b/PLANS.md @@ -3,6 +3,7 @@ Master tracker for every active checklist in the repository. Each source-component also keeps its own plans tracker: [crates/windows-file-enumeration-sys/PLANS.md](crates/windows-file-enumeration-sys/PLANS.md), [crates/windows-file-watcher/PLANS.md](crates/windows-file-watcher/PLANS.md), +[crates/windows-file-watcher-example-test-harness/PLANS.md](crates/windows-file-watcher-example-test-harness/PLANS.md), [crates/windows-impersonation-token-sys/PLANS.md](crates/windows-impersonation-token-sys/PLANS.md), [crates/windows-ioring-sys/PLANS.md](crates/windows-ioring-sys/PLANS.md), [crates/windows-overlapped-io-sys/PLANS.md](crates/windows-overlapped-io-sys/PLANS.md), @@ -10,7 +11,8 @@ plans tracker: [crates/windows-file-enumeration-sys/PLANS.md](crates/windows-fil [crates/windows-platform-probes/PLANS.md](crates/windows-platform-probes/PLANS.md), [crates/windows-thread-ambient-sys/PLANS.md](crates/windows-thread-ambient-sys/PLANS.md), [crates/windows-threadpool-sys/PLANS.md](crates/windows-threadpool-sys/PLANS.md), -[crates/windows-topology-sys/PLANS.md](crates/windows-topology-sys/PLANS.md), and +[crates/windows-topology-sys/PLANS.md](crates/windows-topology-sys/PLANS.md), +[crates/windows-waitable-queues/PLANS.md](crates/windows-waitable-queues/PLANS.md), and [crates/wtf-string/PLANS.md](crates/wtf-string/PLANS.md). Checklists whose work is finished move to [COMPLETED-PLANS.md](COMPLETED-PLANS.md). diff --git a/crates/windows-waitable-queues/PLANS.md b/crates/windows-waitable-queues/PLANS.md index e7b54cbc7..8f8b82b33 100644 --- a/crates/windows-waitable-queues/PLANS.md +++ b/crates/windows-waitable-queues/PLANS.md @@ -5,4 +5,4 @@ in [COMPLETED-PLANS.md](COMPLETED-PLANS.md). | Path to CHECKLIST.md | Status | Brief description | Design Notes | |---|---|---|---| -| [../../CHECKLIST.md](../../CHECKLIST.md) | not started | M30.4: re-home `M31.6`, the `loom` verification this crate's design notes reference in three places and its README promises adopters before 1.0, which had no live checklist item anywhere. Scope as [D-31](DESIGN-NOTES.md#d-31) describes it -- both MPSC shapes or neither -- and repoint all five references, which are in [DESIGN-NOTES.md](DESIGN-NOTES.md), [src/doorbell.rs](src/doorbell.rs) and [sabotage.json](sabotage.json). M30.5 also obliges a sweep of this crate's three public promises of verification before 1.0, whichever way that decision goes. | [DESIGN-NOTES.md](DESIGN-NOTES.md#d-31), [../../DESIGN-RATIONALE.md](../../DESIGN-RATIONALE.md#machine-checking-what-is-argued) | +| [../../CHECKLIST.md](../../CHECKLIST.md) | not started | M30.4: re-home `M31.6`, the `loom` verification this crate's design notes reference in three places and its README promises adopters before 1.0, which had no live checklist item anywhere. Scope as [D-29](DESIGN-NOTES.md#d-29) requires -- both MPSC shapes or neither, which is D-29's obligation rather than [D-31](DESIGN-NOTES.md#d-31)'s; D-31 owns only the release timing -- and repoint all five references, which are in [DESIGN-NOTES.md](DESIGN-NOTES.md), [src/doorbell.rs](src/doorbell.rs) and [sabotage.json](sabotage.json). M30.5 also obliges a sweep of this crate's three public promises of verification before 1.0, whichever way that decision goes. | [DESIGN-NOTES.md](DESIGN-NOTES.md#d-29), [DESIGN-NOTES.md](DESIGN-NOTES.md#d-31), [../../DESIGN-RATIONALE.md](../../DESIGN-RATIONALE.md#machine-checking-what-is-argued) | From 239cc86fac54dba71d2264eca5ba34a0556dff2f Mon Sep 17 00:00:00 2001 From: Mike Grier Date: Tue, 15 Sep 2026 18:13:06 -0700 Subject: [PATCH 8/9] docs: a green run on the unmodified model would mean the model is unfaithful Three findings. The first is a logical contradiction in M30.2's acceptance criteria that would have failed a correct pilot and passed a broken one. M30.2 required the unmodified model to satisfy its invariant, with only a deliberately broken variant producing a counterexample. But SH-14.1 is a LIVE defect in the shipping claim protocol -- verified in reserving_mpsc's own rustdoc, which describes a producer resuming after a full wrap and claiming against a numerically identical but generations-later position, and disclosed to adopters in the README. A faithful model of that protocol, at a position width small enough to wrap, must therefore FIND the defect. "The unmodified model satisfies its invariant" could only be satisfied by a model that does not reproduce something this crate ships and documents. So the criterion was inverted. It would have been failed by a correct model and passed by one that quietly failed to model the hazard -- and the pilot exists precisely to produce that counterexample. Both checks survive, but they attach to configurations rather than to modified and unmodified code: faithfulness -- wrap reachable, producer able to stall across it -> must reproduce SH-14.1, or the model is not modelling this protocol anti-vacuity -- wrap unreachable: pushes bounded below it, or one producer, which has no race to lose -> must come back green, or the model is over-permissive and the counterexample above proved nothing The general form is recorded in the rationale, because it is not specific to this pilot: when the system being modelled has a known defect, a green run on the unmodified model is a failure signal rather than a success. This is the second correction to the same criterion. The first replaced "counterexample only, never a green run" with "both halves"; that was right about vacuity and wrong about which artefact each half attaches to. Also fixes M30.3's elliptical possessive, which a comma made ungrammatical -- the doorbell is a syscall boundary rather than a real-time concern, so the list now names SetEvent/ResetEvent and keeps real-time behaviour as its own entry. The PR description carried the superseded criterion and is updated in the same change; it is the third round in which a corrected claim survived only there, which is the surface no sweep reaches because it is not a file in the tree. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- CHECKLIST.md | 23 +++++++++++++++++++---- DESIGN-RATIONALE.md | 24 +++++++++++++++++++----- 2 files changed, 38 insertions(+), 9 deletions(-) diff --git a/CHECKLIST.md b/CHECKLIST.md index 4f8efc594..3e7f80d3f 100644 --- a/CHECKLIST.md +++ b/CHECKLIST.md @@ -209,14 +209,28 @@ yet; `M30.5` produces it. - [ ] **M30.2** -- Pilot exactly one: `reserving_mpsc`'s claim-position recurrence (`SH-14.1`). + **`SH-14.1` is a live defect in the shipping protocol, not a hypothetical**, and that inverts the + usual shape of a success criterion. A faithful model of the shipping claim protocol, at a position + width small enough to wrap, *must* find it. A green run on that model is therefore evidence the + model is **unfaithful**, not evidence the protocol is sound. + Done when all three hold: 1. **The refinement is stated.** Which constants were shrunk, why the protocol is uniform in each, and what a counterexample at the reduced width implies at the shipping width. If it cannot be argued, the result is reported as a counterexample *in a toy model* and nothing more. - 2. **The unmodified model satisfies its invariant** -- the property check. - 3. **A deliberately broken variant produces a counterexample** -- the anti-vacuity check. Neither - 2 nor 3 alone is sufficient. + 2. **Faithfulness: the model of the shipping protocol reproduces `SH-14.1`.** Configured so the + wrap is reachable and a producer can stall across it, it must yield the known counterexample -- + a claim succeeding against a numerically identical but generations-later position. A model that + cannot produce a defect the crate already documents is not modelling this protocol. + 3. **Anti-vacuity: the same model satisfies its invariant where no violation is possible.** + Configured so the wrap is unreachable -- total pushes bounded below it, or a single producer, + which has no race to lose -- it must come back green. A model that reports a violation there is + over-permissive, and its counterexample in (2) proved nothing. + + An earlier version of this item asked for (2) and (3) the other way round: the unmodified model to + satisfy its invariant, and only a deliberately broken variant to fail. That could only be satisfied + by a model that does *not* reproduce a defect this crate ships and documents. Not a candidate: `capacity == 1`, which belongs to `slotwise_mpsc` ([D-12](crates/windows-waitable-queues/DESIGN-NOTES.md#d-12)) and is already resolved. @@ -227,7 +241,8 @@ yet; `M30.5` produces it. Done when both hold: 1. **The list names only what the *selected* tool cannot model**, not what tools in general cannot. - Expect the syscall boundary including the doorbell's, real-time behaviour, and the model-to-code + Expect the syscall boundary -- including the doorbell's `SetEvent`/`ResetEvent` -- real-time + behaviour, and the model-to-code gap that no tool closes. Do **not** preclassify scheduler-dependence: loom explores scheduler interleavings deliberately, so recording it as unreachable would be a false gap. Whether the memory orderings are reachable likewise depends on which tool M30.1 selected. diff --git a/DESIGN-RATIONALE.md b/DESIGN-RATIONALE.md index 53984d461..5b35c885a 100644 --- a/DESIGN-RATIONALE.md +++ b/DESIGN-RATIONALE.md @@ -555,8 +555,22 @@ trust would have aimed the pilot wrongly. pushes to manifest and is therefore beyond any test". Corrected above: the count is reachable, and the stall window is what is not. -**The success criterion was half a criterion.** The first draft asked for a counterexample from a -deliberately broken variant and explicitly *not* a green run on the correct one -- an overcorrection -against vacuous green runs. A counterexample from a broken variant can equally be produced by a -malformed or over-permissive model that would find one anywhere, so it is an anti-vacuity check, not -a property check. Both are required. +**The success criterion went wrong twice, and the second error was the instructive one.** The first +draft asked for a counterexample from a deliberately broken variant and explicitly *not* a green run +on the correct one -- an overcorrection against vacuous green runs, since a counterexample from a +broken variant can equally be produced by a malformed or over-permissive model that would find one +anywhere. The fix was to require both: property check and anti-vacuity check. + +That fix was wrong for this particular pilot, and the reason is worth keeping. **`SH-14.1` is a live +defect in the shipping protocol**, documented in the crate and disclosed to adopters. So a faithful +model of the shipping claim protocol, at a position width small enough to wrap, *must* find it -- +and "the unmodified model satisfies its invariant" could only be satisfied by a model that does not +reproduce a defect the crate ships. The criterion was inverted: it would have been failed by a +correct model and passed by a broken one. + +The general form: **when the system being modelled has a known defect, a green run on the unmodified +model is a failure signal, not a success.** The two checks still exist, but they attach to different +configurations rather than to modified and unmodified code -- the model must reproduce the defect +where the wrap is reachable, and must come back green where it is not (total pushes bounded below +the wrap, or a single producer, which has no race to lose). `M30.2` carries that as its criteria 2 +and 3. From e5bc9c7a1c97e8651053cb3d41ffd0d35120d506 Mon Sep 17 00:00:00 2001 From: Mike Grier Date: Tue, 15 Sep 2026 18:52:55 -0700 Subject: [PATCH 9/9] docs: require M30.5 to state the cost its own heading promises Four findings, and the first is the interesting one. M30.5's heading says "record the decision with its cost", but its done-when criteria asked only for the model/code maintenance answers and the contract sweep. A future completion could therefore satisfy every criterion while omitting the cost entirely -- an item whose acceptance criteria do not cover its own stated deliverable. Added as criterion 1, naming what cost means here: wall-clock and whose time, tooling added and who maintains it, and the standing cost this workspace already knows it pays -- a specification is a second statement of the contract and can drift from the code with nothing to detect it, so a stale model that still passes is worse than no model. That paragraph used to sit in the item as prose; it belongs as a criterion, which is where it now is. Two more paragraphs of drafting history had accumulated in the active checklist since the last time history was moved out of it, and the milestone's rationale pointer had grown into five lines describing what the rationale contains. Both trimmed; the pointer is one line. This is the third round in which explanatory prose has had to be removed from this milestone, which is worth recording as a pattern rather than fixing quietly: each correction I make arrives with its own justification attached, and the justification belongs in Tier 2 rather than beside the work. The Design Notes column in both trackers carried a DESIGN-RATIONALE.md link. The repository convention reserves that column for DESIGN-NOTES.md paths or "N/A", so a Tier 2 link there invites a reader to take pre-decision rationale for a recorded decision -- the same misclassification that moving the rationale out of DESIGN-NOTES.md was meant to prevent. The rationale link moves into the description and the column reads "N/A for M30". Noted and deliberately not acted on: two rows predating this branch also diverge from that convention -- the root tracker cites a mutation-sweeps README, and windows-platform-probes' tracker cites its own DESIGN-RATIONALE.md. They are out of this PR's scope, and the divergence may mean the convention wants widening rather than the rows narrowing. Raised rather than silently changed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- CHECKLIST.md | 22 ++++++++++------------ DESIGN-NOTES.md | 1 - PLANS.md | 2 +- crates/windows-waitable-queues/PLANS.md | 2 +- 4 files changed, 12 insertions(+), 15 deletions(-) diff --git a/CHECKLIST.md b/CHECKLIST.md index 3e7f80d3f..0cef81b3b 100644 --- a/CHECKLIST.md +++ b/CHECKLIST.md @@ -187,11 +187,7 @@ written before it was stated. ## M30 -- Find out how much of this workspace's algorithm correctness can be machine-checked -Rationale -- why this milestone exists, which tool classes are in scope and what each can see, why -`SH-14.1` is the pilot, and how this relates to -[D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31) -- is in -[DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#machine-checking-what-is-argued). No decision is recorded -yet; `M30.5` produces it. +Rationale: [DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#machine-checking-what-is-argued). - [ ] **M30.1** -- Survey the workspace for algorithms whose correctness is currently argued rather than checked, and match each to the class of tool that could check it. @@ -228,10 +224,6 @@ yet; `M30.5` produces it. which has no race to lose -- it must come back green. A model that reports a violation there is over-permissive, and its counterexample in (2) proved nothing. - An earlier version of this item asked for (2) and (3) the other way round: the unmodified model to - satisfy its invariant, and only a deliberately broken variant to fail. That could only be satisfied - by a model that does *not* reproduce a defect this crate ships and documents. - Not a candidate: `capacity == 1`, which belongs to `slotwise_mpsc` ([D-12](crates/windows-waitable-queues/DESIGN-NOTES.md#d-12)) and is already resolved. @@ -273,12 +265,18 @@ yet; `M30.5` produces it. - [ ] **M30.5** -- Decide what, if anything, the workspace adopts, and record the decision with its cost. - Done when both hold: + Done when all three hold: - 1. **The decision answers three questions**: what keeps the model and the code in step, who + 1. **The cost is stated, not implied.** What running it costs in wall-clock and in whose time, + what tooling it adds and who maintains that, and the standing cost the workspace already knows + it pays here -- a specification is a second statement of the contract and can drift from the + code with nothing to detect it, so a stale model that still passes is worse than no model. An + adoption recorded without its cost is the half of this item that is easiest to skip and the + half the milestone exists to surface. + 2. **The decision answers three questions**: what keeps the model and the code in step, who re-runs it, and what happens when they disagree. "Adopt nothing, and say why" is a legitimate outcome. - 2. **The contract sweep is done, whichever way it went.** Three public places in + 3. **The contract sweep is done, whichever way it went.** Three public places in `windows-waitable-queues` promise machine-checked verification before 1.0: [that crate's README.md](crates/windows-waitable-queues/README.md), [its src/lib.rs](crates/windows-waitable-queues/src/lib.rs), and diff --git a/DESIGN-NOTES.md b/DESIGN-NOTES.md index 451807850..bcb098811 100644 --- a/DESIGN-NOTES.md +++ b/DESIGN-NOTES.md @@ -1859,7 +1859,6 @@ written. The rule is about **discarded failure information**, not about discarde The audit this decision implies is queued as [CHECKLIST.md](CHECKLIST.md) -> `M22.1`; it is not scheduled by this note alone. - ## Prose volume is not the error surface; restatement count is **Decided: the error surface is proportional to how often a fact is restated, not to how much prose diff --git a/PLANS.md b/PLANS.md index 43d67ff41..ee9262a34 100644 --- a/PLANS.md +++ b/PLANS.md @@ -18,7 +18,7 @@ plans tracker: [crates/windows-file-enumeration-sys/PLANS.md](crates/windows-fil | Path to CHECKLIST.md | Status | Brief description | Design Notes | |---|---|---|---| -| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0: it was previously untracked, referenced from that crate's design notes, a source file and its sabotage manifest with no live checklist item anywhere, and is now queued as M30.4. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) for M19-M22; [DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#machine-checking-what-is-argued) for M30's rationale (Tier 2, since no decision is taken yet) -- its decision is not recorded yet, which is what M30.5 produces | +| [CHECKLIST.md](CHECKLIST.md) | not started | M19: propagate the 2026-08-27 platform measurements (IoRing registration replaces the table; the completion-port/`IoRing` fork; `runs_long` as the growth mechanism; the measured 512 default maximum) into the crates whose code or documentation currently assumes otherwise. M20: decide the session-independent path form, now that path resolution is measured to follow the impersonated token's logon session. M21: reconcile with the impersonation and enumeration crates that landed during the session. M22: discharge the failable-call standard across the workspace. M30: find out how much of this workspace's algorithm correctness can be machine-checked -- a survey matching each argued-but-unchecked algorithm to a class of tool (TLA+/PlusCal, loom, bounded proof, `const` assertions), one pilot chosen because parameter shrinking makes an untestable property exhaustive, and a named list of what the pilot could not reach, which is the deliverable. Scoped as an instrument for narrowing hand-inspection rather than replacing it, and explicitly not a reversal of [D-31](crates/windows-waitable-queues/DESIGN-NOTES.md#d-31). Also re-homes `M31.6`, the `loom` verification the queue crate promises adopters before 1.0: it was previously untracked, referenced from that crate's design notes, a source file and its sabotage manifest with no live checklist item anywhere, and is now queued as M30.4. M30's rationale is in [DESIGN-RATIONALE.md](DESIGN-RATIONALE.md#machine-checking-what-is-argued) -- Tier 2, because no decision is taken yet; M30.5 is what produces one. | [DESIGN-NOTES.md](DESIGN-NOTES.md#remoting-synchronous-namespace-operations) for M19-M22; N/A for M30 | | [CHECKLIST-thread-ambient.md](CHECKLIST-thread-ambient.md) | in progress | M22-M23: extract the captured-context composite into `windows-thread-ambient-sys`, a standalone platform layer that captures a thread's ambient state and applies it on another thread. M24-M26: `windows-namespace-request-sys`, marshalable Win32 namespace call parameter sets, over a round-one entry list audited from three real consumers (this repository's watcher and enumeration crates, and `MikeGrier/Globazog-rs`) rather than guessed. M27: `windows-platform-probes`, a durable home for the measurements this workspace's designs rest on, under a three-tier scheme (asserted / ignored / binary-only) where every tier is compiled by an ordinary build. Feature-scoped and deleted when complete; it is the whole of the `mikegrier/thread-ambient` branch's work, and is deliberately separate from the deferred namespace-facility items in [CHECKLIST.md](CHECKLIST.md). | [crates/windows-thread-ambient-sys/DESIGN-NOTES.md](crates/windows-thread-ambient-sys/DESIGN-NOTES.md) | | [crates/windows-overlapped-io-sys/CHECKLIST.md](crates/windows-overlapped-io-sys/CHECKLIST.md) | not started | M14: finish the contract audit -- categories 1, 2, 6, 8, 9 were not examined -- and sweep `outstanding()` for the advisory-predicate hazard. | [crates/windows-overlapped-io-sys/DESIGN-NOTES.md](crates/windows-overlapped-io-sys/DESIGN-NOTES.md) | | [crates/windows-ioring-sys/CHECKLIST.md](crates/windows-ioring-sys/CHECKLIST.md) | in progress | Memory-safe Rust over the Windows `IoRing` submission/completion ring, as a new crate. M1-M7 (ring lifecycle through the `ring-copy` topology-aligned sample) are complete and archived. The parked, pinned-thread `M6+` work and the new M10 contract audit remain. | [crates/windows-ioring-sys/DESIGN-NOTES.md](crates/windows-ioring-sys/DESIGN-NOTES.md) | diff --git a/crates/windows-waitable-queues/PLANS.md b/crates/windows-waitable-queues/PLANS.md index 8f8b82b33..954f2bd3c 100644 --- a/crates/windows-waitable-queues/PLANS.md +++ b/crates/windows-waitable-queues/PLANS.md @@ -5,4 +5,4 @@ in [COMPLETED-PLANS.md](COMPLETED-PLANS.md). | Path to CHECKLIST.md | Status | Brief description | Design Notes | |---|---|---|---| -| [../../CHECKLIST.md](../../CHECKLIST.md) | not started | M30.4: re-home `M31.6`, the `loom` verification this crate's design notes reference in three places and its README promises adopters before 1.0, which had no live checklist item anywhere. Scope as [D-29](DESIGN-NOTES.md#d-29) requires -- both MPSC shapes or neither, which is D-29's obligation rather than [D-31](DESIGN-NOTES.md#d-31)'s; D-31 owns only the release timing -- and repoint all five references, which are in [DESIGN-NOTES.md](DESIGN-NOTES.md), [src/doorbell.rs](src/doorbell.rs) and [sabotage.json](sabotage.json). M30.5 also obliges a sweep of this crate's three public promises of verification before 1.0, whichever way that decision goes. | [DESIGN-NOTES.md](DESIGN-NOTES.md#d-29), [DESIGN-NOTES.md](DESIGN-NOTES.md#d-31), [../../DESIGN-RATIONALE.md](../../DESIGN-RATIONALE.md#machine-checking-what-is-argued) | +| [../../CHECKLIST.md](../../CHECKLIST.md) | not started | M30.4: re-home `M31.6`, the `loom` verification this crate's design notes reference in three places and its README promises adopters before 1.0, which had no live checklist item anywhere. Scope as [D-29](DESIGN-NOTES.md#d-29) requires -- both MPSC shapes or neither, which is D-29's obligation rather than [D-31](DESIGN-NOTES.md#d-31)'s; D-31 owns only the release timing -- and repoint all five references, which are in [DESIGN-NOTES.md](DESIGN-NOTES.md), [src/doorbell.rs](src/doorbell.rs) and [sabotage.json](sabotage.json). M30.5 also obliges a sweep of this crate's three public promises of verification before 1.0, whichever way that decision goes. The milestone's rationale is in [../../DESIGN-RATIONALE.md](../../DESIGN-RATIONALE.md#machine-checking-what-is-argued), Tier 2, because no decision is taken yet. | [DESIGN-NOTES.md](DESIGN-NOTES.md#d-29), [DESIGN-NOTES.md](DESIGN-NOTES.md#d-31) |