diff --git a/CHECKLIST.md b/CHECKLIST.md index 4d01818e..0cef81b3 100644 --- a/CHECKLIST.md +++ b/CHECKLIST.md @@ -185,6 +185,105 @@ written before it was stated. function pointer, which is exactly where such a path would be. Depends on M22.1's classification. +## M30 -- Find out how much of this workspace's algorithm correctness can be machine-checked + +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. + + 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. + + 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`). + + **`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. **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. + + 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. + + 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 `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. + 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. + + 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. + + Done when all three hold: + + 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. + 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 + [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 Ungated work with no identified predecessor deliverable. diff --git a/DESIGN-RATIONALE.md b/DESIGN-RATIONALE.md index cce9fa32..5b35c885 100644 --- a/DESIGN-RATIONALE.md +++ b/DESIGN-RATIONALE.md @@ -447,3 +447,130 @@ 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. 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. + +### 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 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 + +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 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. diff --git a/PLANS.md b/PLANS.md index 8441a884..ee9262a3 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,13 +11,14 @@ 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). | 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. 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 85f260f4..954f2bd3 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-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) |