Days Executor: exact safe-horizon CPU/GPU execution - #104
Open
baochunli wants to merge 231 commits into
Open
Conversation
First phase of the safe-horizon executor plan. Records what original Days does before P02 changes it, and states in one place what the new executor will and will not support. The baseline covers the eight existing FIFO/TailDrop fat-tree fixtures in both CPU modes, using only numbers the simulator already emits. Its purpose is narrow: plan section 10 keeps the pre-removal revision to report original Days behavior, and later correctness work compares against post-P02 Nexosim rather than against these numbers. The results live in the evidence repository. Two results are worth noting. None of the eight fixtures sets a scheduler batch size, so their effective batch is one and removing run batching in P02 will not change their behavior; no fixture needs a semantic-migration label. And the single-threaded medians reproduce exactly across two passes while three of the four multithreaded fixtures differ by two packets, which is direct evidence for the plan's position that Nexosim multithreaded ordering is not a semantic oracle. The scope document states the supported v1 model, what is out of scope for the project rather than impossible, and what is follow-on work after FIFO. It also records the error paths the executor must have and the phase that implements each, since the executor cannot be selected yet: a nonzero time quantum must be refused rather than silently ignored, a cross-LP channel without positive lookahead must be refused by the parallel backends, an unsupported scheduler or event kind must fail validation, and preemptive or cancellable service must be rejected. No simulator behavior changes in this phase. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Summary: - Add finite-capacity DRR and WRR intervening-arrival fixtures. - Add a regression test for the removed scheduler batch config key. Rationale: - Record the eager future-dequeue semantic failure before removing batching. - Require a clear migration diagnostic instead of accepting an unknown key. Tests: - cargo test --features test --test service_start_selection -- --nocapture (expected failure: legacy batching forwards packet 3) - cargo test --test config_migration -- --nocapture (expected failure: unrelated TOML parse error)
Summary: - Make FIFO, DRR, and WRR select one packet at each service start. - Remove scheduler and Wire batch fields, setters, loops, and config wiring. - Reject the removed config key with a clear migration diagnostic. - Update active configs, documentation, constructors, and test drivers. Rationale: - Future queue choices must observe arrivals before their service starts. - Eager dequeue released finite buffer capacity before transmission began. - Wire propagation remains independent while using single-event scheduling. Tests: - cargo build --release - cargo fmt --all --check - cargo clippy --all-targets -- -D warnings - cargo test --features test - cargo run --release --bin days -- configs/simple.toml
Summary: - Add a byte-capacity FIFO fixture with a 100 Gbit/s backlog. - Assert packet identity and nanosecond departure times. - Verify the 101 ns arrival is admitted after the backlog drains. Rationale: - Eager batching rounds cumulative deadlines and leaves one packet until 102 ns. - Per-service-start selection rounds each interval independently and drains the backlog by 100 ns, changing TailDrop admission. Tests: - current: cargo test --features test --test service_start_selection - fbd7d88: focused FIFO test fails with packet 19 at 102 ns and packet 20 absent
Summary: - Add the dependency-free days-executor crate and workspace wiring. - Define canonical fixed-width event, image, and closed model records. - Add exact checked serialization and arrival-time arithmetic. - Cover event ordering and integer boundary behavior. Rationale: - Shared records remain pointer-free for future CPU and GPU backends. - Exact timing avoids legacy cumulative floating-point rounding. - Zero rates and time overflow fail explicitly instead of wrapping. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test - cargo build --manifest-path executor/Cargo.toml --no-default-features
Summary: - Replace homogeneous nodes and links with role-aware descriptors. - Store host and switch state arenas in one semantic simulation image. - Add link-qualified channels and descriptor-based arrival timing. - Define and exhaustively test the closed role/event dispatch shape. Rationale: - Host and switch LPs own different state and transition handlers. - Both roles share one channel table, event set, horizon, and exchange. - Backend role worklists are physical views, not semantic images. - The contract stays dependency-free, pointer-free, and lock-free. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test - cargo build --manifest-path executor/Cargo.toml --no-default-features
Summary: - Add the canonical global EventKey executor and normalized run result. - Model owned host transmit state and switch FIFO/TailDrop admission. - Cover state, timing, drops, and the stop-boundary residual with a hand-derived golden. Rationale: - Keep scalar execution as the permanent executable oracle for later backends. - Select exactly one packet at each TxReady and schedule the next choice only after the committed transmission completes. - Preserve exact integer link timing and message-only cross-LP effects. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - Change the final queued packet pair to two bytes each. - Update the hand-derived departures, arrivals, drop, and residual event. - Document the independent-versus-cumulative rounding calculation. Rationale: - The previous three-byte/one-byte pair rounded to the same total under correct and eager selection, so it could not guard the service rule. - Independent service starts now take twelve nanoseconds while an eager cumulative reservation takes eleven, shifting observable output. - A temporary greedy executor failed on P3 at 35 ns versus the 36 ns golden; the faithful executor passes after byte-for-byte restoration. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - lower supported FIFO/TailDrop Days configs into one mixed-role image - retain canonical flow routes and switch-owned per-egress queues - reject unsupported or lossy source behavior with named diagnostics Rationale: - semantic topology and traffic keys make identity independent of legacy process-global counters, construction order, and map iteration order - exact ordered images give every backend one stable scenario contract Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - Reverse two distinct flow sets across equivalent source fixtures. - Use a diamond topology to cover canonical equal-cost route selection. - Assert exact image identity and updated dense-ID and packet counts. Rationale: - Flow sets share one seeded RNG, so source order must not change endpoint draws, flow IDs, payload IDs, or initial events. - The test now fails if canonical flow-set sorting is removed. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - derive route-specific channel bounds from exact serialization and propagation, and validate the complete image contract - implement non-preemptive switch transmission and sink delivery with one packet selected per TxReady - add mutation diagnostics, end-to-end lowering, and eager-selection goldens Rationale: - an overstated channel bound can raise the global lookahead and safe horizon above a possible remote arrival, allowing an LP to consume an event too soon - an understated bound only narrows the horizon and reduces parallel progress, so positive conservative understatements remain valid Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - Exercise mixed packet sizes on one link and reject the larger delay. - Cover distinct initial events whose keys are not ascending. Rationale: - Validator logic was already correct; these tests close mutation gaps. - The minimum delay is soundness-critical because it bounds the safe horizon. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test - mutation: per-link min to max (expected failure) - mutation: removed initial-event ordering check (expected failure)
Summary: - Store the exact exclusive stop time as `SimulationImage::stop_time_ns`. - Clamp scalar runs to the image boundary and cover lowering regressions. Rationale: - Lowering accepted top-level `duration` but silently discarded it. That is worse than rejection because runs can return plausible, incorrect results beyond the configured boundary without any error. - Keeping the fixed-width stop time in the image preserves the complete backend input contract while the existing run horizon remains an earlier prefix-execution clamp. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - Process events through the image's inclusive simulation stop while preserving an optional half-open execution horizon for partial runs. - Add boundary regressions and the comparison example. Tighten the P01 pending-event expectation. Rationale: - The exclusive scalar stop produced 11,992 sends while Nexosim produced 12,000: eight source events at the 1,500-second endpoint were skipped. - Scalar must match legacy inclusive `duration` to remain the executable oracle and preserve the frozen P01 baselines. - The safe horizon stays half-open because it is a safety boundary. The inclusive scenario endpoint carries no lookahead-safety meaning. Validation: - Post-fix k4 observations agree at 12,000 sent, 11,992 received, and zero dropped on both paths. - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - Replace scalar node, link, packet, and flow scans with checked indexed lookups. - Require each descriptor ID to equal its dense table index in the load-time validator, with mutation coverage for all four tables. Rationale: - The oracle's linear packet-table lookups made execution quadratic in packet count. - Validation now enforces the positional invariant that permits direct indexing. A fallback preserves behavior for hand-built callers that skip validation. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - Report step_until duration apart from terminal statistics and CSV flush. - Preserve the legacy total-time line and add precise stepping and total lines. - Cover the additive timing output with an integration test. Rationale: - Make the scalar and Nexosim executor timing boundaries comparable without changing simulation behavior, event ordering, statistics, or reports. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - replace linear descriptor resolution with checked dense indexing - aggregate packet counts by flow and node for counter and origin checks - index service events and route channels while preserving input order - remove the scalar benchmark's duplicate Scalar validation pass Rationale: - per-node packet/flow/route rescans dominated k8 validation, followed by event-to-packet scans; the cited channel scan was real but inactive in the measured PacketArrival-only baseline - dense vectors and ordered maps/sets replace repeated scans without weakening checks or changing diagnostic traversal order - all indexes are validation-only and never determine image output order, so canonical lowering and byte-identical reordering remain intact Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - Store closed, fixed-width generator state on each source host and lower one initial packet and PacketArrival per active flow. - Generate packets through host transitions, route ordinary feedback packets into source-owned state, and represent blocked and stop-limited flows without requiring a pending emission. - Allocate payload identities from checked per-node monotone counters and keep packet size and direction on each packet. - Default scalar runs to wide summary counters while retaining complete packet descriptors, arrivals, and departures in explicit full-observation mode. Rationale: - Materializing every packet made image construction and validation scale with the packet count, imposing a memory ceiling before execution. - A state-driven transition supports reactive closed-loop traffic later; closed-form times and sizes would bake open-loop assumptions into the image. - Fresh payload allocation keeps retransmissions distinct even when transport sequence numbers repeat. - Feedback state, reverse routes, no-event blocked state, and a closed feedback action contract accommodate future closed-loop generators without adding an EventKind or implementing TCP now. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test - k4/f8 exact legacy terminal-observation agreement - k8/f64 and k16/f512 compile time/RSS measurements - k32/f4096 end-to-end scalar run
Summary: - Reject scheduled payload identities already consumed by their generator. - Require feedback packets to retain source-owned generator state and reserve pending arrivals against the generator counter. - Enforce source provenance for preloaded data payloads and add regressions. Rationale: - Validation accepted three malformed image classes that runtime execution then mishandled through identity reuse, feedback misclassification, or a feedback-state overflow. - Whole-run PayloadId uniqueness makes retransmission representable: every emission needs a fresh counter allocation even when its transport sequence repeats. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test - cargo run --release --example scalar_benchmark -- configs/benchmarks/baseline/fattree_k4_f8_st.toml
Summary: - Share one transition state between the global queue and round drivers. - Compute H=min(S,min_i N_i+L) from an owner-local lazy frontier heap. - Drain local work half-open and radix-order remote outbox exchange. - Retain sparse per-round work, efficiency, and cost instrumentation. Rationale: - Events exactly at H must wait because unseen remote work is only bounded at H. The configured stop remains inclusive by representing S as one nanosecond after stop_time_ns, including the u64::MAX endpoint. - Lazy generations, active heap pops, sparse outboxes, linear radix order, and target-only updates keep round overhead independent of total LPs. - Event-key normalization keeps complete observations comparable across legal intra-round LP execution orders. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test - release idle-node falsification: 1.024x time for 100x idle LPs - fattree_k4_f8_st: 12000 sent, 11992 received, 0 dropped
Summary: - Reject a payload whose initial events span incompatible lifecycle states. - Accept only matching completion/remote siblings for an in-flight packet. - Pin blocked generators out of the frontier reduction with an exact horizon. Rationale: - Validation admitted a packet that was both unsourced and already delivered. Global execution removed it first, while round execution sourced and started it first, breaking the scalar oracle equivalence. - A transmission emits completion and remote arrival as consecutive siblings, while TxReady payloads can be control tokens rather than packet residency. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test - cargo run --release --example round_benchmark -- configs/benchmarks/baseline/fattree_k4_f8_st.toml
Keep a scoped crossbeam worker pool alive across safe-horizon rounds and park workers on channel receives between extract, execute, and merge barriers. Fixed LP ownership provides local frontier minima, while moved LP values keep the hot path free of shared mutable state. Model assignment as one LPT-ordered chunk dispatcher. The static extreme uses one ceil(active/workers) chunk per bulk worker; finer granularities request more chunks for better balance at additional message cost. A single dominating LP cannot be improved by reassignment, so classify stragglers into explicit worklists, start them first, and reserve dedicated workers for them. Reduce the safe horizon from worker-local minima and route remote events directly to target owners for parallel radix-ordered inbox merges. Dynamic dispatch remains deterministic because LP state is disjoint, identifiers are node-local, and cross-LP events merge by the canonical event key. Cover full-state equality across the 128-seed corpus, worker counts, granularities, classifications, incast, accepted orphan snapshots, injected failures, capacity and arithmetic errors, and the lowered k4 golden.
Summary: - drain worker failures on abort and prefer panic root causes over disconnection symptoms - batch remote events once per source-worker and target-owner pair while returning LP state through existing completion and restore messages - expose reserved straggler workers and deterministic physical LP probes - report fused-message counts in the round benchmark Rationale: - remove channel operations from the per-event path without replacing message passing or changing canonical merge order - make dedicated routing and sparse idle-LP traversal falsifiable rather than relying on semantic counters or timing Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Fuse each unclassified static round into one wake and one aggregate completion per worker. Keep deterministic LP shards resident, route fused remote batches through the next round command, and reduce the next minimum at the coordinator. Bound every per-round command and reply wait with 4096 optimistic polls before parking. These channels and polls are pool-lifecycle synchronization at round boundaries; they do not touch the per-event path and introduce no atomics or locks. Fast-path exact same-time TxComplete-to-TxReady continuations and skip invariant byte passes in the stable radix exchange. Retain radix sorting because multi-egress switch LP outboxes are not globally ordered by target and event key. Report actual channel crossings, synchronization phase timing, continuation counts, and scalar remote events. The k16 median moves from the 5.069 s program baseline to 1.832 s at four workers (30.56 us/round), below the 1.956 s gate; channel traffic falls from 38.15 to 8.00 messages/round. Validated with cargo build --workspace, cargo build --workspace --release, cargo fmt --all --check, cargo clippy --workspace --all-targets -- -D warnings, cargo test --workspace, and cargo test --features test.
Summary: - Attribute resident inbox merge counters to their producing round. - Retain Finish-time merge counters beyond the execution horizon. - Cover cross-transport metrics, resident failures, and queue collisions. Rationale: - Keep load-bearing semantic metrics consistent across CPU transports. - Lock down resident teardown and full-key continuation ordering. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - Route legacy FIB installation and exact descriptors through one deterministic shortest-path table. - Assert all-scale per-flow physical route equality and document the migration comparison preconditions. Rationale: - Canonical BFS and legacy selection assigned different equal-cost paths, so prior migration rows observed different networks. - Keep rate-limited endpoint attachment semantics unchanged while making future structural drift fail before observation comparison. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - Share legacy PacketSwitch FIB installation with diagnostic snapshots. - Walk installed forward and reverse FIBs before comparing observations. - Document the settled endpoint-attachment migration direction. Rationale: - Selector-to-selector checks could not detect skipped or incorrect FIB hops. - Structural parity must gate interpretation of cross-engine observations. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - Add a default-off model_host_attachment topology option. - Install one shared full-duplex FIFO attachment per host with exact rates, capacities, propagation, and flow demultiplexing. - Reuse an installed attachment snapshot to assert forward and reverse stage parity through k32. Rationale: - Exact lowering requires positive-delay host LP channels and models physical host links. - Opt-in legacy stages preserve historical behavior while enabling same-network executor comparisons. Results: - Key-off artifacts remain byte-identical to the pre-change baseline. - Key-on route and stage structures match, but terminal counts retain small-to-congested tie-order residuals rather than reaching exact equality. Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
Summary: - Start idle legacy FIFO service at max(packet time, busy deadline). - Snapshot endpoint rate, direction, and wiring from installed models. - Add a one-ULP regression and strengthen endpoint image parity. Rationale: - Exact-versus-f64 comparison exposed a legacy one-ULP deadline gap that could leave an idle port's queued packet without a wakeup. - Configuration-derived endpoint descriptors could not detect runtime rate or mailbox-wiring regressions. Validation: - Both doubled-rate and miswired-source mutations fail endpoint parity. - Key-on k8 now matches exact at 95,936 received packets. - Completed 8 us legacy MT bars: k16 2.944217208 s and k32 11.818190458 s (one warmup, median of three). - Passed workspace debug/release builds, fmt, clippy, workspace tests, and feature-enabled tests.
Summary: - derive deterministic switch-port LP identities from physical switch and egress-link keys while preserving physical link IDs - route remote arrivals directly to the selected downstream port LP and validate per-port ownership, physical continuity, and channel coverage - add pre/post physical-oracle, lookahead, route-parity, determinism, and complete scalar/CPU matrix coverage Rationale: - dividing hot switches by egress port raises available parallelism without adding intra-switch messages or processing latency - keep radix exchange ordering because route-dependent targets still falsify the proposed sorted-run invariant Tests: - cargo build --workspace - cargo build --workspace --release - cargo fmt --all --check - cargo clippy --workspace --all-targets -- -D warnings - cargo test --workspace - cargo test --features test
The canonical contract is amended: pending_events denotes LIVE events. A retransmission timeout that stops being a flow's armed timer stops being pending state, so scalar, CPU, and safe-horizon rounds now remove it from the owning LP's ordered future map inside the transition that supersedes it. The transition owns sender state while the backend owns the queue, so every `active_timer` Some -> None edge records a SupersededTimer identity that the queue owner drains after each dispatch. Removal is a bounded range scan over the one canonical key range that can hold the identity, which reproduces the retired lazy recognition's choice exactly. The lazy pop-skip survives only for legacy-import residue and is now guarded by a provenance debug assertion. Tests: the two retention assertions retire in favour of their inverses plus a closure matrix that pins one pending event per armed timer across scalar, safe-horizon rounds, and CPU at five horizons.
Metal and CUDA carry the same live-state contract as the host lanes. The per-flow TCP ledger metadata word +3, previously reserved and zero, now holds the flow's fallback-heap record position as `slot + 1`, and every heap movement repairs it: push claims the arming record before its sift-up, pop resolves ownership before the restructure can relocate another live timer into the vacated root, and the shared swap and move helpers retarget whichever record they carry. The repair is conditioned on the moved record already being the flow's recorded owner, so an imported duplicate carrying the same flow cannot steal ownership. `heap_remove_timer` performs the interior deletion at both ACK-driven disarm sites: it validates the full event identity at the recorded slot, fills the hole with the last record, repairs in whichever direction the fill violates, and refreshes the fallback-source min cache exactly as a pop would. The retired lazy recognition becomes a checked invariant rather than a silent skip: an owned record must match the armed timer and an unowned record must not, so semantic code 61 latches a corrupted slot index. Legacy import residue carries no owning flow and keeps the lazy path as its only consumer. Import publishes the same ownership rule the runtime uses, giving each armed timer the canonically first heap record carrying its identity.
The retained allowance paid for every superseded retransmission timeout an execution could install, capped per flow at twice the measured frontier failure average. Eager removal makes a flow's physical fallback-heap residency exactly its armed timer, so the per-TCP term collapses to one record and the constant is renamed for what it now bounds. Both device planners call the same bound through the shared capacity context, so the T20e legacy/precomputed equality holds by construction. Route and service slack, the initial-event floor, and the pacing base slot are unchanged: imported legacy residue is still resident until its deadline, so initial events remain a hard floor. The sizing mirror carries the per-LP composition and the outward-safety argument for each term. Non-TCP frozen plan bytes are unaffected, which the T20e bit-equal gate and the k48 wide-corpus arena freeze both confirm.
The CUDA port landed the heap machinery but not two of the transition-body edits: the fast-retransmit disarm still dropped its armed timer without removing the record, and the retransmission-timeout dispatch still took the silent lazy skip instead of checking the ownership invariant. Both now mirror Metal, which a whole-file anchor count over the T20g symbols confirms: the only remaining Metal surplus is its diagnostics-only FEL probe kernel, which CUDA does not build.
The dispatch invariant catches a slot that points at a record the armed timer does not match, but it cannot see the failure mode where a disarm forgets to remove and the following re-arm quietly overwrites the slot. Arming now requires the flow's slot to be empty, which is true after firing and after an eager disarm and false exactly when a removal the contract required did not happen. This is the check that would have caught the fast-retransmit gap the previous commit closed by inspection.
The `c3_t24_smoke_campaign` row ran `T24_CORPUS=fattree_k4_tcp_cubic_f16_smoke.toml` against a corpus list that never contained the smoke fixture, so the filter skipped every member and the campaign passed in 0.00s having compared nothing. The fixture was excluded because `CORPORA` is the formal k16/k32 ladder whose manifests are pinned by name, and the k4 image is deliberately not a ladder point. That is a reason to keep it out of the ladder assertions, not out of the execution campaign: it is a canonical TCP image and the campaign is a correctness campaign. So `CORPORA` stays the ladder, and a new `CAMPAIGN_CORPORA` (smoke + ladder) is what the lowering and four-backend byte-identity campaigns iterate. Both now run five corpora. A filter that selects no campaign member is now a harness error rather than an empty pass, and each corpus prints what it compared, so no automated row can report an execution that never happened. Selection is factored into a pure function so the miss cases are tested without touching process environment. Two non-ignored guards cover campaign membership and selection semantics. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Three in-repo sites still stated the retention contract the T20g item-2 amendment retired. `RunResult::pending_events` was documented as "Unprocessed events in canonical `EventKey` order" — the exact wording the blocker report cited as the reason a user ruling was required — and the Metal and CUDA planner comments still justified the fallback bound by stale timers staying resident until their deadlines, sitting directly above the call whose bound this task changed to one record per flow. All three now state the live-state amendment: a superseded retransmission timeout is removed at the invalidating edge on every backend, imported timeouts that no armed timer owns are the exception, and both planner comments say not to restore a per-attempt reservation. Cited to Mechanism API errata E5. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
RED. The gate lowers each fixture serially and under several route-worker budgets and requires byte-identical SimulationImage values, identical Debug byte counts, and identical FNV-1a-64 fingerprints over those Debug bytes. Three fixtures also carry the frozen pre-T20h lowering hashes, so a scatter that reordered a route would be caught against bytes that predate this task. The budget knob does not exist yet, so the gate fails to build: unresolved import `days::scenario::compile_config_with_route_workers` no `RouteWorkers` in `topos::route` Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
GREEN. `compute_shortest_path_route_table` now partitions the submitted flows by index into at most `RouteWorkers` contiguous chunks and computes each chunk on its own scoped thread, writing only into that chunk's disjoint slice of a pre-sized result buffer. There is no shared mutable state, no lock, and no channel: the workers borrow the immutable canonical graph and the cached fat-tree classification, and scatter into index-addressed slots. The pathfinder was already pure. `canonical_routing_graph` and `fat_tree_params` run once before the scatter, and `try_compute_route_in_classified_canonical_graph` allocates its own scores, predecessor, and heap state per call, consults no cache, draws no randomness, and never iterates a hash map. A route is therefore a function of the graph and the endpoints alone. Error reporting keeps submission order rather than completion order: the scatter stops at the first repeated key, exactly where the serial table stopped asking for routes, and the reported failure is the first failing submission position. `compile_config_with_route_workers` exposes the budget so the equality gate can pin the parallel scatter against `RouteWorkers::serial()`. The gate passes on the k4, k8, k4-TCP-smoke, k16-TCP and k32 load fixtures under 2, 3 and 4 workers, and the three fixtures that carry frozen pre-T20h lowering hashes still reproduce them exactly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The scatter's subtlest obligation is that a wider budget must not change which failure is reported. Five unit tests hold it, each run at budgets 1, 2, 3, 7 and 64: - the canonical k4 fat-tree table is identical at every budget over all 56 ordered switch pairs; - the A* fallback table on a five-node two-component graph is identical at every budget, so the non-fat-tree path is covered too; - the reported error is the first failing SUBMISSION position: an unreachable flow before a repeated key outranks it, a repeated key before an unreachable flow outranks it, and a position that is both is diagnosed as a repeat; - an empty submission needs no worker and yields no chunk; - the widest budget still classifies the topology exactly once, so no worker reclassifies the immutable graph. Mutation check on the error-ordering test: replacing the duplicate-key routing horizon with `keys.len()` makes it FAIL at every budget, because the table then reports the later unreachable flow instead of the earlier repeated key. The test is not vacuous. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Review round 1 finding M1: the "classified once" invariant was blind inside the scatter. `FAT_TREE_LAYOUT_CHECKS` is a `thread_local!`, and T20h moved per-flow route computation onto worker threads, each of which gets its own copy of it. A `fat_tree_params` call made by a worker incremented that worker's cell, while the assertion read the submitting thread's — so the reviewer's regression probe (one full O(edges) re-classification per chunk, inserted at the top of `fill_route_chunk`) left both guarding tests green. Add a process-wide `static ROUTE_FILL_LAYOUT_CHECKS: AtomicUsize` counting every classification taken while per-flow routes are being filled, on any thread, and assert it is zero in both tests. The counter is never reset, so unrelated route tests running concurrently in the same test binary can neither erase a regression's evidence nor manufacture one: zero is the correct value for every caller. `a_wide_budget_still_classifies_the_topology_once` also now asserts its budget really produces eight chunks, so neither assertion can hold vacuously on a serial partition. RED: with the reviewer's regression applied, both `a_wide_budget_still_classifies_the_topology_once` and `route_table_checks_fat_tree_layout_once_for_all_flows` fail (45 worker-side classifications observed); at be7f88e the same regression left 11/11 green. GREEN: regression removed, 11/11 route tests and 33/33 lib tests pass, stable over 20 consecutive parallel runs. The production route path is unchanged: every added line is `#[cfg(test)]`, and the only edit to a non-test expression is reshaping the `scope.spawn` closure body into a block that compiles to the identical call. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Review round 1 finding L1. The module docstring told the reader that shortest-path routing "Selects a random candidate from a set of shortest paths". That described `RandomSimplePath::compute_route`, which drew from `all_simple_paths` with an RNG and was deleted in 2023; `grep -rn "RandomSimplePath|all_simple_paths"` over src, legacy/src and executor/src matches nothing but this docstring today. The first thing anyone auditing lowering determinism reads therefore said the opposite of the truth, in the file whose per-flow loop T20h had just parallelized. Describe what the code does: canonicalize the graph, take the fixed-order uniform-cost best-first search on a canonical fat tree, fall back to petgraph A* at uniform cost otherwise, and break equal-cost alternatives by enumeration order rather than by choice. Note the deleted protocol so the fossil is not re-introduced by someone who remembers it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…rface Folded in at the review round's request. This breakage is provably not T20h's: `days-executor` does not depend on `days` (its dependencies are crossbeam, num-bigint, num-rational and the optional device crates), the dependency runs the other way, and `git diff --name-only 4bbae38..be7f88e` touches nothing under `executor/` or `legacy/`. The review confirmed the attribution independently. Three classes: - `unused import: RunResult` in `executor/tests/scalar_switch_schedulers.rs` and `executor/tests/safe_horizon_rounds.rs`. The only unqualified uses are in `assert_device_full_result_eq`, which is `#[cfg(any(cuda, metal-spike+apple))]`; the two remaining uses spell the type out. Move the import under the same gate rather than deleting it, so the device builds still compile. - Dead code under `planner-test-hooks`: `device_sizing::exact_plan_report` and `PlannerCapacityContext::matches_legacy`. Every caller of either is a `planner-test-hooks` function inside `cuda.rs` or `metal.rs`, modules that only exist under `cuda` / `metal-spike`, so `any(test, planner-test-hooks)` compiled them dead whenever the feature was on without a device backend. Narrow each cfg to the configurations that actually have a consumer — `exact_plan_report` keeps its `test` arm (its own `#[cfg(test)]` unit test calls it), `matches_legacy` does not (nothing under plain `cfg(test)` calls it, which is why it was dead on the `metal-spike` surface as well). - Nine `days-legacy` integration tests tripping needless_borrow, manual_range_contains, manual_range_patterns, while_let_on_iterator and assertions_on_constants. These only surface behind `--features test`, and the earlier aborts masked all but the first few, so the fix took two passes. Eight surfaces now pass `-D warnings`: fmt; `-p days-executor` at default, planner-test-hooks, metal-spike and metal-test-hooks; `-p days --features test`; `-p days-legacy --features test`; and the workspace default. Every edited test binary was re-run green, and the T20h default equality gate still reproduces all five frozen fingerprints exactly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… scans The de-quadratification of `validate` replaces eight linear rescans of `initial_packets`/`initial_events` with flow-keyed index walks. Six of the eight sites fold with `count`, `min` or `max` and are order-insensitive, but two return on the first offending element and name it in the diagnostic: * `validate_tcp_segment_ledger` reports the first initial TCP segment of the generator's flow at or beyond `next_sequence`. * `validate_origin_sequences` reports the first switch-owned payload sequence at or above the switch's next origin sequence. Neither had a multi-violation case in the corpus, so nothing pinned *which* offender is named. These two cases pin it against the pre-change scan, before the scan mechanics change. Reversing either scan in the current code makes the new cases fail with the second offender's identity (sequence 1024 instead of 512; sequence 3 instead of 2). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
`validate` answered "which initial packets, or preloaded ACK arrivals, belong to this flow?" with a full linear filter over the 262,144-entry `initial_packets`/`initial_events` tables, once per TCP generator, at eight sites. The load-time validator was therefore O(F x P): the T20j decomposition measured 276.10 s of a 277.4 s `compile_config` on the frontier fixture inside `validate`, and 99.7% of that inside those eight rescans. The tables are now indexed once per `validate` call: * `FlowIndex` holds a CSR grouping of `initial_packets` by dense flow slot, built by one forward counting pass, so a group lists its members in initial-table order; identifiers outside the dense table keep an unindexed group that a query filters by equality. * The same pass records, per flow, the number of preloaded TCP ACK arrivals and the subset inside the run horizon — the two counts the timer-installation and attempt bounds took a scan each to recompute per generator. * The admissible-event-time minimum is hoisted: it never depended on the generator it was recomputed for. * `future_work` is derived once, at its first consumer (`validate_global_time_capacity`), and passed to the three validators that used to recompute it. Deriving it there rather than in `validate` keeps a rejection raised while deriving it attributed to the same validator. * `validate_origin_sequences` buckets payload sequences by node-strided owner in one pass instead of rescanning every packet per switch LP. Threading the index also removes the same rescan from `maximum_drr_frame_bytes`, a ninth consumer the decomposition did not reach because the frontier fixture has no DRR queues. No formula, predicate or ordering changes. `initial_packets` is strictly ascending in `PayloadId`, so each owner bucket is ascending in sequence, and a CSR built by a forward pass preserves initial-table order inside each group: the two sites that name the first offending element name the same one. `tests/t20j_validate_flow_index.rs` is the verdict-equality gate: on every executor-lowerable fixture family in `configs/`, on running checkpoints of them, on an image with flows outside the dense table, and across stop times that split the preloaded ACK arrivals, the indexed walk must visit exactly the elements the retained scan visits, in the same order, and fold to the same values. Perturbing the CSR fill order, the horizon filter, the arrival-target discrimination, or the bucket order each makes it fail. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
`cargo xtask audit` whitelists every semantic feature gate in the executor by path, predicate and exact count. The retained pre-index scans and their equality hook add `feature = "planner-test-hooks"` twice in `validate.rs` and once in `lib.rs`, so the audit reported them as unapproved. They are registered with the purpose they serve. The audit still reports three findings in `device_sizing.rs` and `planner_capacity.rs`. Those pre-date this branch: `cargo xtask audit` fails with exactly those three at 3df9388, and this change makes its output byte-identical to that baseline rather than adding to it. Also corrected: the `FlowIndex` doc said "eight sites", but threading the index covers nine call sites — the ninth is `maximum_drr_frame_bytes`, which the T20j decomposition never reached because the frontier fixture has no DRR queues. And the equality hook now looks its owner bucket up with `get` instead of indexing, so a non-dense node table would make the gate report a mismatch rather than panic. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Review finding A-2: `flow_indexed_walks_match_the_scans_for_flows_outside_the_
dense_table` never issued a query that resolved outside the dense flow table.
The equality harness derived every query from `image.flows`, all of whose ids
are dense, so `FlowIndex::packets_for_flow`'s `None => (unindexed_packets, true)`
arm was never taken by the gate. The reviewer's red probe confirmed it: replacing
that arm with an empty slice left all five tests green while rustc reported
`unindexed_packets` as never read.
The harness now also queries every identifier that labels an initial packet
without resolving to a dense slot — the only query shape that reaches the
fallback — and compares that walk against the retained scan.
The test additionally retargets a packet to a *second* outside identifier, so
the shared unindexed group holds members of two distinct flows and the
fallback's equality filter is load-bearing rather than inert, and asserts that
the set of outside queries the gate will issue is exactly those two (the
coverage assertion; an empty set would make the new loop vacuous again).
RED (both perturbations applied to the shipped index, gate re-run, tree
restored):
- `None => (&[][..], true)` (the reviewer's probe) now FAILS:
`unindexed flow FlowId(21) indexed packet walk [] differs from the scanned
walk [PayloadId(0), PayloadId(3)]`
- dropping the fallback's `packet.flow == id` filter now FAILS:
`unindexed flow FlowId(21) indexed packet walk [PayloadId(0), PayloadId(3),
PayloadId(5)] differs from the scanned walk [PayloadId(0), PayloadId(3)]`
GREEN: 5/5 at the restored tree.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Review finding A-1 (MEDIUM). `validate_blocked_tcp_timer` counted the initial
retransmission-timeout events carrying a timer's executable identity with a full
linear scan of `image.initial_events`, once per Blocked TCP generator — exactly
the O(F x E) shape this task exists to remove, and the one site of ten that the
first round missed. It is not marginal: `scalar.rs` sets `Blocked` on every TCP
emission, so on a TCP checkpoint essentially every in-flight flow reaches it. The
reviewer measured 1,024 full passes over a 3,072-event table (~3.1M element
visits) per `validate` on `p11/rq9_closed_k16`, and 100% of TCP generators
Blocked-with-timer on every TCP checkpoint of the gate's own grid.
`FlowIndex` now also carries `retransmission_timeouts`, a count per
`(target, payload, deadline_ns)` identity folded during the same single forward
pass over `initial_events` that already computes the ACK counts and the
admissible-time minimum. The key is a timer's executable identity rather than a
flow, matching the key `validate_generators` already uses to reject two flows
whose timers would consume the same event. `count` is order-insensitive, so no
diagnostic changes: the only consumer rejects on a count of zero and its message
is byte-identical.
The pre-index scan is retained verbatim in `mod legacy_scans` and the
verdict-equality gate compares against it two ways: the buckets must partition
exactly the timeout events of the table, and at every TCP generator holding an
active timer the count must match at the timer's own key and at three
single-component perturbations of it. A new coverage assertion in the checkpoint
test requires the corpus to reach at least one Blocked-with-timer generator, so
the comparison cannot run zero times.
RED (each perturbation applied to the shipped tree, gate re-run, tree restored):
- index keyed per node (`(target, PayloadId(0), 0)`) FAILS:
`node NodeId(1) payload PayloadId(0) deadline 1000000000 has 1 indexed
timeout events but 0 scanned ones`
- index admits every event kind FAILS:
`timeout-identity buckets cover 48 events, but 16 are retransmission
timeouts`
- per-key count inflated by one FAILS:
`timeout-identity buckets cover 32 events, but 16 are retransmission
timeouts`
- coverage helper stubbed to 0 FAILS:
`the checkpoint corpus must reach the Blocked TCP timer event-count site at
all`
GREEN: 5/5 at the restored tree; fmt and clippy (executor default and
planner-test-hooks, --all-targets, -D warnings) clean.
Also corrects the gate's stale "eight sites" docstring to ten (finding A-5).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Review finding A-3: §3.8 row 6 pinned `maximum_drr_frame_bytes` with "DRR corpus green", but all nineteen `FIXTURES` declare FIFO, and `maximum_drr_frame_bytes` is reached only from the `SchedulerKind::DeficitRoundRobin` arm of `validate_scheduler_state`. The gate never invoked the ninth site at all, so there was no DRR corpus behind that cell. There is no lowerable DRR config to add: `configs/benchmarks/scheduling/*_drr_*` select `routing` and `configs/ci/leanguard_drr.toml` uses explicit flow identifiers and an explicit graph, all of which `compile_config` rejects for reasons unrelated to scheduling. The DRR image is therefore built from a lowered TCP fixture by rewriting every switch queue's scheduler as single-class DRR. The new test does more than run the site: it pins the value the site computes, through the validator's own verdict. The DRR arm rejects exactly when `quantum + (maximum_frame - 1)` overflows `u64`, so the largest accepted quantum is `u64::MAX - (maximum_frame - 1)` and acceptance is a step function of the ninth site's frame bound. The test asserts both sides of that step and that the rejection names the frozen bound (1460, this fixture's CUBIC MSS). RED: adding one byte to `maximum_drr_frame_bytes`'s use of `tcp_future_data_max_frame` FAILS the accept side — `switch node NodeId(16) queue 0 DRR class 0 cannot accumulate enough deficit for a 1461-byte packet without overflowing`. Tree restored. GREEN: 6/6; fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Review finding A-1, second instance. `future_work`'s PFC reservation resolved
"which executable residents belong to this flow?" with a linear filter over the
derived resident table, twice per `(PFC ingress, flow)` pair
(`validate.rs:5316` and `:5337` at `ed0181e`) — the same per-flow-filter shape
this task removes, wrapped around a `packet_can_still_cross_link` call that is
itself `O(N + E)` per surviving packet. `FlowIndex` cannot answer it because the
table is derived by `executable_resident_packets`, not stored on the image.
`ResidentFlowGroups` groups that derived table once, by the same CSR
construction and with the same dense-slot/unindexed-fallback argument as
`FlowIndex::packets_for_flow`, and the two filters become group walks. Both
folds are `count()`, so only the element set matters; the grouping preserves
resident-table order anyway. It is built after the per-flow counting loop so
that a resident outside the dense flow table still reaches that loop's direct
index first, leaving the panic/rejection order untouched.
Reachability, stated because it decides how this is gated: every PFC-carrying
config in the tree is rejected by `compile_config` (`configs/pfc.toml` and
`configs/ci/leanguard_pfc.toml` for refresh/drain timers, the four DCQCN configs
for an eight-entry `link.pfc.xoff`), and no fixture in the T20j corpus carries a
live PFC ingress — so the *reservation* is reached only from the hand-built
images in `executor/tests/pfc_semantics.rs` (33 tests, not modified by this
work, several of which — `pfc_reservation_ignores_packet_past_controller`,
`pfc_maximum_frame_ignores_packet_past_controller` — pin exactly this count).
The *grouping*, which is all that changed, is gated on the whole T20j corpus:
the equality hook now compares the indexed resident walk against the retained
scan for every flow, dense and unindexed, plus the partition property.
RED (each applied to the shipped tree, gate re-run, tree restored):
- dense resident groups emptied FAILS: `flow FlowId(0) indexed resident walk
[] differs from the scanned walk [PayloadId(109), PayloadId(205),
PayloadId(301)]`
- resident CSR filled in reverse FAILS: `flow FlowId(0) indexed resident walk
[PayloadId(6707), PayloadId(563)] differs from the scanned walk
[PayloadId(563), PayloadId(6707)]`
Both fire on real residents, so the new comparison is not vacuous.
GREEN: T20j gate 6/6; days-executor nextest green including pfc_semantics;
fmt and clippy (planner-test-hooks, --all-targets, -D warnings) clean.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Layer 2 of T20i, informed by layer 1's measured demand law. Three changes land together because the plane layout, its kernels, its readback and its consumer cannot compile apart. RING CONVERSION (user-ruled fold-in). The per-flow segment ledger becomes a head/tail ring. Layer 1 measured that its operations are ring-perfect: occupancy IS the congestion window, new segments append past the highest sequence, retransmissions replace in place, and cumulative ACKs remove a prefix. Prefix removal now advances a head word instead of compacting O(n) records, and both O(n) sequence scans become a binary search over the ring window (valid because the ledger is strictly ascending and duplicate-free). Interior inserts still shift, but inside the ring; a prefix insert retreats the head in O(1). Canonical state is untouched. Logical index i lives at physical slot (head + i) mod capacity, and every reader walks i = 0..count, so the decoded record order and content are identical to what the shifting array produced. `executor/src/tcp_ledger_ring.rs` carries transliterations of BOTH algorithms and replays op traces through them, asserting canonical-byte equality at every step; breaking the head advance turns 6 of 9 red. The whole Metal `tcp_semantics` matrix (61 tests, including the four-backend cartesian byte-identity gate) passed the ring change on its first run. OCCUPANCY-VECTOR FAULT PAYLOAD. Ledger metadata widens from 4 words to 6: a ring head and an occupancy high-water mark, maintained at the single site that raises `count`. On a ledger capacity fault the backends read the whole per-flow high-water vector off the plane the fault aborted on and attach it to the failed attempt. High-water is a max over a deterministic execution, so it is pure state; it is advisory sizing input only and never reaches simulation semantics. PER-FLOW, VECTOR-INFORMED GROWTH. `TcpCapacityClassFloors` becomes `TcpCapacityFloors`: class-together growth is RETIRED for the segment ledger (T20g proved it needs 129.1 GB at the measured demand, beyond madrid's whole pool, while layer 1 showed the demand is carried by 377 of 262,144 flows) and the arena is keyed by FlowId. One replan now sizes EVERY flow at `max(8 * high_water + 8, derived)` instead of repairing the one flow the fault named. The factor is argued from the measured law in device_capacity.rs: a stalled recovery grows linearly in simulated time, so attempt n+1 reaches `s + k * (t_n - s)` and 8 is the knee for the frontier's 21x ratio, at a cost of 0.6 GiB out of boston's 6.4 GiB margin. Gates: cargo fmt; clippy -D warnings on executor default, executor metal-spike, leanguard-run, shared test+metal-spike, and cuda-planner-test; `cargo test -p days-executor --lib` 45 passed; the Metal `tcp_semantics` suite; the T20e bit-equal planner gates (the 0695f02 plan anchor moves by exactly 8 flows x 2 words x 8 B = 128 B, the metadata widening and nothing else); the T20h frontier and k32 lowering fingerprints. `cargo xtask audit` registers the two new gate sites; its four remaining failures are unchanged from e78a2a9. New gate `metal_tcp_ledger_occupancy_vector_sizes_every_flow_in_one_replan` under-caps two flows with a retry budget of one; with the vector raise removed it fails exactly as layer 1 predicted -- retry 1 repairs FlowId(0), then FlowId(1) faults -- which is the 377-attempt chain in miniature. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
CUDA cannot execute here and the follow-up measurement round owns remote runs, so the CUDA half of the ring conversion had no gate at all. It has one now: `executor/tests/t20i_ledger_ring_kernels.rs` extracts the five ledger functions from both kernel sources, erases the Metal/CUDA spelling difference, and requires the results to be identical character for character -- so the CUDA ledger inherits whatever the Apple `tcp_semantics` suite proves about the Metal ledger. Four more assertions pin the properties the ring exists for, in both kernels: the six-word metadata row, the acknowledge compaction loop being DELETED rather than gated (the sole surviving record access is the partial-ACK boundary re-key), the high-water word having exactly one writer -- which is what makes the fault payload a max over a deterministic execution -- and neither sequence lookup walking the ledger linearly any more. The Metal `tcp_ledger_slot` signature is rewrapped to the CUDA line breaking so the transliteration check needs no whitespace exemption. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ion precondition Closes review round 1 LOW 7 and LOW 6. LOW 7 — gate coverage of the two new metadata words was asymmetric. `the_high_water_word_has_exactly_one_writer_in_each_kernel` pinned word +5's writer count at 1, but nothing pinned word +4, the ring head. Only `the_acknowledge_compaction_loop_is_deleted_not_gated` mentioned it, and only to assert R7 exists. The head is the ring's single reordering degree of freedom, so a stray third write would rotate the canonical decode without touching `count`, `high_water` or any record byte. RED, and it is the reviewer's exact scenario: a semantically neutral third head write (`tcp_state[meta + TCP_LEDGER_META_HEAD] = head;` after R2) added identically to BOTH kernels leaves every existing gate green — the transliteration gate, the compaction gate, the high-water gate and the linear-scan gate all pass, and so do all 63 Metal `tcp_semantics` tests on the real device — while the new `the_ring_head_word_has_exactly_two_writers_in_each_kernel` fails with `left: 3, right: 2`. Reverted; 6/6 green. LOW 6 — the mirror could not detect a violation of the kernels' modulo precondition. `ledger_record_slot` uses a total `%`; both kernels reduce with a single conditional subtraction, which is a complete modulo only while `head + logical <= 2 * capacity - 1`. A future call site past that bound would be right on the host and wrong on the device with the byte-identity gate still green. Chosen fix: assert the precondition in the mirror (`debug_assert!`, at `ledger_record_slot` and at R7, the tightest consumer) rather than adopt the kernels' arithmetic, because `%` keeps the host answer correct where the device answer would be wrong, and this runs once per resident record per flow in the frontier readback. The residual limitation — release builds do not check it — is stated in the source. Two new mirror tests: one exhaustive equivalence of the two reduction forms over the whole precondition domain (capacity 0..=12), which also shows exactly where they part company outside it; one `#[should_panic]` non-vacuity probe for the assertion itself. RED demonstrated by deleting the `debug_assert!`: "test did not panic as expected". Restored; 13/13 ring tests green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Closes review round 1 LOW 1 and LOW 3. Every figure below was recomputed from layer 1's raw whole-run per-flow peak array (`p11_t20i_l1_..._ledger_probe.txt.peaks.bin`, 262,144 u32 LE, max 11,058), not copied from the review. LOW 1 — `TCP_LEDGER_OCCUPANCY_SLACK_RECORDS` claimed the `+ 8` costs "3,025 records — 121 kB". It costs 8 records on each of the 9,298 flows the `k = 8` factor lifts off the derived floor (exactly the flows with peak >= 65, since `8 * 64 + 8 = 520` does not clear it) = 74,384 records = 2,975,360 B = 2.98 MB. That is 24.6x the filed figure. 3,025 is not reproducible from any of the three probe arrays and is not even a multiple of 8. LOW 3 — three slips in `TcpCapacityFloors`: - "class keying costs 4.66x boston" divided 120.198 GiB by boston's 25.757 GB read as GiB. Bytes over bytes is 129,062,061,272 / 25,757,220,864 = 5.011x, which section 6 of the report already stated correctly. - "120.195 GiB" for the class-uniform alternative; it is 120.198 GiB. - "48.9 GB for one plane, 1.90x boston's whole device, and 129.1 GB for the whole plan" was bracketed as one computation "at the measured demand". They are at two different demands: 48.9 GB is the tcp_state plane at T20g's device-measured 4,633 (whole plan there is 61.7 GB), while 129.1 GB is the whole plan at layer 1's whole-run 11,058. Split into two labelled figures. Also labelled, self-found: "per-flow keying costs 24.6 MiB over the plan that already fits" is the k = 1 exact-peak cost (18,588,901,112 - 18,563,122,392 = 25,778,720 B = 24.58 MiB), not the implemented k = 8 cost of 0.669 GiB. Both are now named. Docs only; no behaviour change. fmt clean, all five clippy surfaces clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Carry-over from the T20j round-2 review. `tests/t20j_validate_flow_index.rs:301` justified the frozen 1,460-byte DRR frame bound by saying the CUBIC MSS "dominates the 40-byte ACKs and the (empty) initial packet table". The initial packet table is not empty. Verified directly against the fixture (`configs/benchmarks/tcp/fattree_k4_tcp_cubic_f16_smoke.toml`, lowered through `compile_config`): `initial_packets` holds 16 entries, one per flow, every one a `TcpData` packet of 1,460 B at sequence 0. So the site's `initial_packets` term is also 1,460 and agrees with the MSS rather than being absent. The term that really contributes 0 is the *indexed* retransmission term in `tcp_future_data_max_frame`, and for a different reason: every TCP generator in the fixture is still at `next_sequence = 0`, so the filter's `header.sequence < tcp.next_sequence` is `0 < 0` for every packet the flow index yields. Comment corrected with that verified reason. Comment only; the frozen constant and the assertions are untouched. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The goal-row round found an honest coverage gap. T20i layer 2 added two small deterministic ledger fixtures -- the typed capacity-retry fault and the one-replan occupancy-vector sizing -- and both existed only for Metal. The CUDA retry loop reaches the identical shared policy in `device_capacity`, and it was exercised on hardware at frontier scale, but nothing cheap and deterministic pinned it. `cuda_tcp_ledger_capacity_retry_is_typed_and_byte_identical` and `cuda_tcp_ledger_occupancy_vector_sizes_every_flow_in_one_replan` mirror their Metal counterparts assertion for assertion: whole-struct equality on the typed `CudaError::CapacityExceeded`, byte identity against the scalar oracle over the complete state, and every field of the single retry record including the `8 * high_water + 8` replacement capacity that replaced the retired additive class retreat. They follow the convention of the pair already in this file, `metal_tcp_timer_checkpoint_is_byte_identical` / `cuda_tcp_timer_checkpoint_is_byte_identical`: same file, sibling placed after its Metal counterpart, CUDA gated on the feature alone with no `target_vendor` and no `#[ignore]`. The `tcp_two_flow_image` builder and the `DeviceCapacityCaps` import move to the `any(cuda, all(metal-spike, apple))` form the file already uses for its shared device helpers. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
`cargo xtask audit` has been red on this branch since 3df9388 ("T20h review 1: Fix the pre-existing clippy breakage on every gated surface"), which narrowed two cfg gates to kill dead_code under -D warnings but did not touch xtask/src/main.rs. Four findings, two distinct source gates: each narrowed gate reports once as unapproved and once as a missing/changed approved entry. `git log -S`/-G/-L over both gate strings converge on 3df9388 alone; 8f950d6 edited device_sizing.rs afterwards but changed no cfg line there. The registry exists to catch gates added without review, so both were audited against their consumers rather than rubber-stamped: - `device_sizing::exact_plan_report` is called by its own `#[cfg(test)]` unit test, by `cuda::size_cuda_plan_for_testing` (a `planner-test-hooks` item in the `cuda`-gated module) and by `metal::size_metal_plan_for_testing` (ditto under `metal-spike` + `target_vendor = "apple"`). The three-arm gate is the exact union of those configurations — no arm without a consumer, no consumer without an arm. - `PlannerCapacityContext::matches_legacy` is `pub(crate)` and reached only from `assert_cuda_planner_bit_equal_for_testing` and `assert_metal_planner_bit_equal_for_testing`. Its lack of a `test` arm is therefore correct, not an oversight: nothing under plain `cfg(test)` calls it. Both feature combinations already appear in the registry for the matching lib.rs re-exports, and every feature name is declared in executor/Cargo.toml, so neither gate is a typo, an over-broad combination, or dead code. The fix belongs in the registry, and no executor source changed. Registry: `device_sizing.rs` keeps count 1 with the three-arm predicate; `planner_capacity.rs any(test, planner-test-hooks)` drops 18 -> 17 (exactly the one converted site — the gate count on 3df9388^ is 18, on the working tree 17); a new `planner_capacity.rs` entry approves the `matches_legacy` gate and records why it carries no `test` arm. Audit red before, green after. fmt clean; clippy -D warnings passes on the workspace default, `-p days-executor` at default/planner-test-hooks/metal-spike/ metal-test-hooks, `-p days` at test/lean/test,metal-spike, and `-p days-legacy --features test` — the four executor surfaces being exactly where an over-broad gate would resurface as dead_code, which is independent confirmation the gates are tight. The T20e planner bit-equal gate runs 4/4 green on `-p days --features test,metal-spike`, exercising `matches_legacy` under the narrowed gate; `planner_capacity.rs` is byte-identical to c244e65. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
`tcp_ledger::normalize_image` walked every host state's generator list to apply each TCP sender's `highest_ack` to the segment ledger. Both seeding entry points call it, and `seed_packets` is called once per LP by `cpu::build_lps`, so on a fat-tree k32 image the walk ran ~9.5k times over ~8.2k host states. An image with no TCP data descriptors produces an empty ledger, and `acknowledge_segments` returns before touching anything when the ledger does not carry the generator's flow. An empty ledger is therefore a fixed point of the whole loop: it can neither change nor report a conflict. Returning early is a cost reduction with no reachable behavior difference. DIAGNOSTIC red/green, examples/round_benchmark on configs/benchmarks/width_via_load_full/fattree_k32_load_90.toml (rounds 18, events 31,104,461), --workers 18, M5 Max, n=3 medians: 3,271 ms before this commit, 2,647 ms after. The T20 trilogy bisect attributed +606 ms on this fixture to 89bf4d4, which is the commit that introduced the walk. Tests: - cargo nextest run -p days-executor - cargo nextest run -p days-executor --features metal-spike - lake build and the P10c mechanism, P10c AQM, SP and WFQ LeanGuard campaigns Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
`switch_tx_ready` rebuilt four vectors over the entire egress queue on every `TxReady` — a packet lookup, a flow lookup and a full route walk per queued payload — then cloned the scheduler and projected the eligible packets into a record shape, all before selecting anything. Every one of those is only observable through a mechanism that can reorder service or hold a packet back: PFC pausing, or the deficit/weighted round-robin disciplines. `switch_tx_complete` and `switch_remote_arrival` paid smaller versions of the same bill, a queue scan and a route walk that only a PFC monitor reads. The cost was quadratic in queue depth on a fixture that instantiates none of those mechanisms, which is why the T20 trilogy measured it growing with run length. This commit splits the service plan in two. A queue with no PFC monitor cannot report a paused priority, so every queued packet is eligible; FIFO, static priority and weighted fair queueing all maintain service order in the queue itself, which is exactly why `scheduler_select_position` answers position zero for all three. Under those conditions the plan is the queue head, and the selection, the removal and the state updates are what the eligible-packet path computes. `queue_serves_head` classifies the disciplines with an exhaustive match, so a new discipline cannot silently inherit the head-only plan. `scheduler_before` and the round-robin packet projection move behind the two disciplines that read them. `switch_remote_arrival` derives the incoming link only for a queue that carries a monitor. RED first: mutating the head plan to pop the queue's back makes the new test fail on nine departures, because the monitored image takes the eligible-packet path and the unmonitored one takes the head plan. GREEN with the plan as written. Byte identity, DIAGNOSTIC control fixture (configs/benchmarks/width_via_load_full/fattree_k32_load_90.toml): the scalar run's complete printed result is identical to pristine 08452f3, and the parallel run's every semantic field is identical (rounds, events, active LPs, remote events, same-time continuations, LP probes, owner batches, pool messages, sourced/received/dropped packets); only timing telemetry moves. The LeanGuard corpora are unchanged. DIAGNOSTIC, M5 Max, n=3 medians on that fixture, --workers 18: 2,647 ms before this commit, 909 ms after, against 806 ms for the bd7015c P08 reference built on the same host — 4.06x over reference at 08452f3, 1.12x after. Scalar: 51.9 s at 08452f3, 10.46 s after, against 10.62 s for the reference. Tests: - cargo fmt --all -- --check - cargo clippy -D warnings on the workspace, -p days-executor at default, metal-spike, planner-test-hooks and metal-test-hooks, -p days at test,metal-spike and lean, -p days-legacy --features test, and the leanguard-run bin - cargo xtask audit - cargo nextest run -p days-executor (291), --features metal-spike (361), -p days (125), -p days --features test,metal-spike (143) - the T20e planner bit-equal gate, 4/4 - lake build and the P10c mechanism, P10c AQM, SP and WFQ LeanGuard campaigns Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implements the Days Executor plan — one logical process per network node, with different LPs advancing concurrently only under a conservative safe-horizon rule.
All twelve phases land on this single branch. Intermediate phases leave the tree in states where the executor crate exists but no backend runs it yet, so merging them separately would put partially built features on
main. The branch builds and passes its tests at every phase boundary.This description is updated after each phase.
Progress
P01 — Baseline and scope
Records what original Days does before P02 changes it, and states what the new executor will and will not support. No simulator behaviour changes.
The eight existing FIFO/TailDrop fat-tree fixtures were measured in both CPU modes using only output the simulator already emits; results live in the evidence repository. None of the eight sets a scheduler batch size, so P02's removal does not change their behaviour. Single-threaded medians reproduce exactly across two passes while three of four multithreaded fixtures differ by two packets — direct evidence that Nexosim multithreaded ordering is not a semantic oracle.
Scope document at
docs/content/docs/architecture/executor-scope.mdx.P02 — Remove legacy run batching
A safe horizon guarantees no unseen remote event precedes a consumed one. It does not authorise a handler to choose future packets. Legacy scheduling violated that by popping up to
run_batch_sizepackets in one call and committing departures for service starts that had not happened yet.Every scheduler now inspects the queue at
t, selects at most one packet, commits that non-preemptive transmission, and schedules the nextTxReadyonly when service can start again.Three adversarial fixtures, each exposing a distinct mechanism, all verified to fail before the removal and pass after:
[0,1,2,3]instead of[0,1,2]).The FIFO case was initially believed impossible: packet-count occupancy is invariant in batch width. That algebra is correct but incomplete — the divergence lives in byte occupancy driven by rounding drift. Review caught it.
run_batch_sizeis gone from FIFO, DRR, WRR, and Wire; SP, WFQ, and VirtualClock were untouched as they already selected once per service start. Configurations still carrying the key now fail with a migration diagnostic across all three construction paths.P03 — Executor foundation
Adds the
days/executorcrate: canonicalEventKeyordered lexicographically over(time_ns, phase, origin_node, origin_seq), fixed-width image records with no callback, trait object, pointer, or backend handle, and exact integer time arithmetic —ceil(8·B·10⁹ / r) + d_propwithu128widening confined inside the helper, since the device ABI cannot assume nativeu128.The image is heterogeneous: one semantic
SimulationImageholds both host and switch LPs with separate state arenas selected byNodeKind, dispatched through(NodeKind, EventKind). Role separation is physical, not semantic — backends may derive role-specific views and even separate kernels, but all share one horizon, one channel table, and one exchange barrier.The scalar executor is the permanent oracle every other backend will be judged against. Its golden is hand-derived on paper: at 3 Gb/s with 2 ns propagation, service starts
[0, 8, 24, 32], departures[8, 24, 32, 35], arrivals[10, 26, 34, 37], with a 1-byte packet exercising the ceiling (8/3 → 3 ns), a TailDrop at capacity two, and arrivals landing between service starts.Review found the golden could not detect eager multi-selection — a regressed
TxReadycould reserve two packets and reproduce every asserted value. Strengthened and verified by making the executor greedy: it now fails withdeparted_packets3 vs 4 andnext_origin_seq13 vs 16.No locks,
Arc, atomics, orunsafeanywhere in the crate — LPs own their state exclusively and communicate by message, which is what makes concurrent advancement sound.Phase gates: P02 and P03 both passed with no findings.
P04 — Scenario lowering and validation
Days host, switch, topology, link, and traffic data now lower into a single
SimulationImagethat the scalar executor runs end to end. Scenario-local IDs derive from semantic topology keys rather than allocation order, so reordering equivalent source collections yields a byte-identical image. The phase gate confirmed that guarantee is load-bearing by removing ID canonicalization, route ordering, and flow-set sorting in isolation and observing tests fail each time.validate()rejects invalid role/state slots, unsupported role/event pairs, bad link endpoints, duplicate or missing ownership, undeclared remote emission, zero or overstated channel bounds, non-monotone keys, and overflow — each with a specific diagnostic asserted against its complete string.The channel bound is the soundness crux. An overstated bound raises the safe horizon above what the guarantee supports and causes silent misordering; an understated one merely costs speed. Review found the implementation correct but the tests unable to prove it stayed correct: differently sized packets sat on disjoint links, so
minandmaxcoincided and a mutation survived all nine tests. A link now carries two packet sizes, and flippingmintomaxfails.Three real defects surfaced, each found by a different mechanism:
durationaccepted and silently discarded (phase gate). A config withduration = 1.0lowered cleanly and then delivered packets past its own boundary. The stop time now lives on the image asstop_time_ns, so the image remains the complete input contract when it later crosses to a GPU.step_untilis inclusive: 11,992 versus 12,000 packets sent. The arithmetic pinned it exactly — inclusive gives t = 1…1500 × 8 flows = 12,000. The scenario endpoint is now inclusive to match the oracle's referent, while the safe horizon stays strictly half-open; these are different quantities and are now pinned by separate tests.Measured against Nexosim
With lowering and switch service both in place, the same configuration runs through both paths for the first time. Terminal observations agree exactly — 12,000 sent, 11,992 received, 0 dropped — which is meaningful here because the corpus is exactly representable: 320 kbit/s with 1,000-byte packets serializes in precisely 25,000,000 ns and interarrivals are exactly 10⁹ ns, so nothing rounds on either side.
run_scalarstep_untilStatistics and CSV flushing accounted for only 0.11 ms and 0.17 ms, so they do not explain the margin. The representational win is real but modest, and it buys speed with generality — closed event kinds, FIFO/TailDrop only, no arbitrary futures. It is not on its own an order-of-magnitude case for the rewrite; the parallelism phases still have to deliver.
The comparison earned its keep mainly by finding two quadratics that unit tests could not see:
.find()scans over tables that grow with the scenario, making execution O(N·P). The first measurement showed scalar 150× slower than Nexosim at k8 — an artifact, not a verdict. Direct indexing fixed it (33× at k4, 202× at k8; scaling exponent 1.97 → 1.13). Density is now enforced invalidatewith per-table diagnostics rather than assumed, so a future backend cannot index out of range.BTreeMap/BTreeSet— no hashed iteration reaches output.k16/f512 now completes end to end: 14,321,891 events, 768,000 packets sourced, 0 dropped, 0.56 s to lower and validate, 1.38 s to execute.
Interlude — the image becomes generator-based (pre-P05)
Lowering previously materialized every packet of the whole run — 768,000 descriptors and initial events at k16, a memory ceiling before a time ceiling. Packets are now produced by per-flow generator state owned by the source host: one initial
PacketArrivalper flow, each emission scheduling the next,EventKindunchanged.PayloadIdcomes from per-node monotone counters, so a future TCP retransmission of the same sequence gets a fresh identity by construction; the closed-loop hooks (feedback-driven emission, a flow blocked with no scheduled event) exist and are tested even though v1 implements only the constant generator.Measured at k16: compile 549 ms → 34 ms, peak RSS 465 MiB → 7 MB; k32/f4096 becomes feasible at 27.7 MiB peak. The accepted cost — resident packets moved to a
BTreeMap, k16 execution 1.32 → 2.33 s — is recorded in the plan with its replacement (a slot-allocated arena) owned by P08/P11. Review closed three validation gaps (payload-ID reuse, feedback packets silently counted as data, unreserved feedback counters), each with red→green shown.P05 — Multicore CPU
T9 builds single-threaded round-by-round execution sharing every transition handler with the global priority-queue oracle:
H = min(S, minᵢ Nᵢ + L), half-open drain, per-LP outboxes, canonical radix exchange. Equivalence is proven over 128 randomized heterogeneous seeds plus targeted regimes (events exactly at H, blocked flows, one active LP among thousands idle). Per-round cost is O(active LPs + messages): 100× more idle LPs changes round time by 1.024×. Review found one high — validation admitted causally incompatible initial positions for a payload, making round and global modes disagree on a physically unrealizable image — fixed by rejection at validation.T10 adds the persistent crossbeam worker pool: chunked LPT dispatch with one granularity parameter (static partition = one chunk per worker), per-round straggler classification routed to dedicated workers, sender-side batched exchange merged per owner,
Hfrom an O(workers) reduction, all-or-nothing failure. Correctness is a 4,608-comparison matrix — 128 seeds × workers 1–4 × three granularities × three classifications — all byte-identical to the scalar oracle, plus an incast fixture proving the dominating LP is classified, dispatched first, and isolated.The phase gate ran the load-bearing measurement — the three-way legacy comparison §9.2 demands (legacy MT with and without
time_quantum_ns, since the published 1574× FatTree-32 result rested on quantization):The initial pool was overhead-dominated — 83.6 µs/round at k16 against an 8.7 µs critical path — and the gate fired the plan's pull-forward trigger. Four exactness-preserving mechanisms landed: spin-then-park waits (4,096-poll bound, worth 13.7 µs/round), fused per-round messaging (exactly 2W = 8 messages/round at four workers, down from 38), radix byte-pass skipping (the sorted-run merge was correctly halted — the invariant is false while one LP owns several egress links), and a same-time
TxComplete→TxReadycontinuation fast path (1.27M heap operations removed at k16, guarded on the full event key against multi-queue collisions).Result: the exact executor now beats unquantized legacy MT at k8 and k16 — parallelism paying without approximation, where legacy Days needed quantization (measured here as negligible: an 8 µs quantum cannot coarsen 25 ms event spacing). Two honest residuals: k32 still trails legacy MT (8.63 vs 7.11 s) and is now purely ceiling-limited — worker wait is 116 of 141 µs/round at parallel efficiency 0.034 — which the next phase (P05b, one LP per switch egress port) exists to raise; and legacy-vs-new terminal observations diverge at scale (24 packets at k16, 355K at congested k32), under investigation for attribution to legacy
f64timing outside the exact domain versus a semantic gap.Reviews across the phase closed one high and eight mediums, each verified by falsification; instrumentation (per-LP and per-worker times, parallel efficiency, message counts) is cross-transport-equivalent and load-bearing for design decisions.
The divergence investigation, and what it found
The gate's legacy comparison carried an asterisk: terminal observations diverged (24 packets at k16, 355K at congested k32). Root-causing it produced the phase's most consequential findings — the engines were simulating different networks. Lowering chose equal-cost paths by canonical BFS where legacy uses
ShortestPath::compute_route_in(99.2% of the k32 gap), and lowering models rate-limited host-attachment stages legacy lacked (the rest). Fixes, each falsification-verified: one shared route selector called by both engines; structural parity asserted from legacy's installed FIBs and instantiated endpoint wiring rather than recomputed configuration; and an opt-inmodel_host_attachmentstage in legacy (default off, key-off byte-identity enumerated) so both engines simulate the identical network.On that identical network the comparison converged to its irreducible layer, yielding two results now recorded for the paper:
EventKey(flows 16, 20, 50, 51); Nexosim's ST executor pops same-time runnables LIFO (51, 50, 20, 16). Both deterministic; only one canonical. k16 residual +1, k32 ~0.13% — the same ordering cascading through congestion.packet_time >= busy_untilpredicate can fail by one ULP, stranding a queued packet on an idle link until an unrelated arrival wakes it (observed: 1499.35 s until 1500.15 s, past the stop). Exact integer time makes the class unrepresentable. Fixed minimally with a red/green regression; key-off effects enumerated (7 of 32 baseline artifacts, MT delivery counts +2/+3/+11).Final fair bars (identical networks, warmup + median of three): the exact CPU backend beats every legacy configuration — k16: 1.449 s vs 2.308 (MT), 2.332 (ST), 2.944 (MT quantized); k32: 9.249 s vs 9.439 (MT), 11.818 (MT quantized), 20.406 (ST). Quantization now hurts legacy on this corpus, so the exact-parallelism claim holds against legacy's strongest variant. P05 is closed.
P05b — one LP per switch egress port
Each switch egress port is now its own LP with canonical identity derived from
(switch, egress link), its own origin-sequence cursor, and counters; arrivals route directly to the egress-port LP over the inbound physical link, so no intra-switch messages exist and the certified lookahead is pinned unchanged at exactly 25,000,000 ns.The mission was the ceiling, and it moved decisively:
k32 wall improved to 8.933 s (5.4% under the fair legacy-MT bar; the gate's own rerun measured 7.876 s). Honest costs, measured and owned by P05c: k8/k16 walls regressed (+15/+17%) to per-LP machinery — the round now costs ~5× per LP touch what the LP's ~0.1 µs of work costs — and 8 workers still invert because the barrier takes a max over more noisy completions of ever-smaller work.
Review found one critical with a subtle lesson: per-port identities re-key the canonical equal-time tiebreak, so public observation vectors permute at equal timestamps versus pre-split — and the comparison oracle was sorting before comparing, masking it. The contract is now explicit: times, dispositions, drop identities, per-flow order, and terminal state must match exactly across versions (verified over 128 full and partial comparisons — none differ); equal-time record order is documented version-specific semantics, pinned by a star fixture that fails if either the real invariants break or someone re-masks the permutation.
The gate passed P05b conditionally: oracle equality, the cross-version contract, ceiling gains, L invariance, layering (no topology-family term exists in
executor/src— a newly recorded design principle), and scope all clean; the decisive k32 margin and wall recovery transfer to P05c.P05c — harvest the ceiling
Six commits turned P05b's raised ceiling into wall-clock results, every change ablated:
The k32 round fell 149 → 66.8 µs (wait 108.6 → 49.5 via direct worker-to-worker exchange with early merge overlapping the straggler tail; coordinator "other" 34.9 → 16.8 via wake-as-published-
Hwith workers draining self-owned active sets; exchange 4.1 → 0.22; per-LP touch 250 → 112 ns via SoA hot-field arrays). A topology-agnostic route-load partition replaced modulo ownership — the executor reads only image data, never topology shape, now a recorded design principle. Honest retirements with measurements: fused classification (still 2.24× slower than off on this corpus; machinery kept and tested for the GPU hybrid), and per-(source,target) sorted sub-runs (0.7–3% regression; provisionally retired, raw logs not retained). W8 still trails W4 by 13% — measured cause: pool crossings 24 → 77/round against shrinking per-worker work.The strategic measurement: a new small-lookahead fixture (100 Gbps, 1 µs propagation — the regime GeDES and ns-GPU evaluate in; lookahead exactly 1,080 ns) runs 792,030 rounds per simulated second at a 2.35 µs/round floor, with terminal observations exactly matching legacy Nexosim (99,000/99,000/0). The dense-datacenter regime is contestable on CPU alone; device-resident multi-round batching stays an optimization for P07, not a rescue.
Determinism is now enforced by a fully Cartesian matrix: 18,432 complete-
RunResultcomparisons (2 partitions × 4 worker counts × 3 granularities × 3 classifications × 2 horizon cuts × 128 images) in six seconds of test time.The gate passed all eight acceptance items on its own fresh measurements, with one wording ruling adopted project-wide: the central claim is scoped to the published contention-bound regime — on this same-network corpus at k32, unquantized legacy MT does beat legacy ST, so the honest claim is the 2.37× same-network margin plus the published-regime quantization history, never "legacy MT can't pay without approximation."
P06 — the formal proof
The Lean development (
lean/DaysExecutor/, beside the existing LeanGuard package) proves all five theorems about the executor as shipped:G + Lpolicy the Rust computesTrust base:
[propext, Classical.choice, Quot.sound]for every theorem — Lean's bare standard axioms; zerosorry/admit/axiom/native_decidein the development. Premises are exhibited jointly satisfiable by a heterogeneous three-round formal execution with distinct host and switch branches both stepping, and F5's commutation premise is discharged for the concrete instance (license-in-hand for the Metal backend's clustering).Getting the statements right was most of the phase: eleven model-hardening rounds — four adversarial statement reviews, then proof attempts as stricter reviewers — foreclosed 22 defect classes, each a bug a parallel-simulator implementer could actually write and none now expressible: eager selection via hidden state, preemption by erasure, commitment duplication, observation-key aliasing, descriptor resurrection, reference laundering, order-sensitive stores, unreachable-start over-quantification. Two statement corrections were sanctioned along the way (F2's reachability premise, F5's co-pending scope), both discovered by proof, both restoring semantics the plan had always stated in prose. The proofs also explained the implementation: serializability was unprovable until the model adopted the executor's reference counting — decrements commute where discretionary cleanup cannot — and the
BTreeMap's canonical order turned out to be load-bearing for order-independence. Not one production Rust line changed during the phase.P07 — the GPU feasibility gauntlet
Five bounded spikes, each with a fair matched comparator, each catching its predecessor's flaw:
objc2-metal, 16,384 rounds/encoder?Every verdict is scoped and reproducible: 10–50M-event budgets enforced in code, matched CPU replays with nine-plane state equality, three review rounds with the final round clean. The chapter's conclusion is precise: on this corpus the CPU pool wins everywhere the fabric can physically reach — and the binding limit at the end is the corpus, not the fabric.
P08 — the Metal backend and the crossover-reduction ladder
P08 is reinstated by directive (July 29, 2026): the paper's GPU story is central, so the Metal backend is built regardless, with these measurements shaping it rather than gating it. First T13f: an opt-in
hosts_per_edgebuilder option restores the canonical k³/4 host population (8,192 at k32, matching GeDES/ns-GPU corpora) and re-runs the width sweep as the compliant 10–90% load experiment T13e was designed to be — measuring the true achievable width and P08's target regime. Then T14/T15 build the production backend against the measured cost structure: device-side worklist construction, role-split kernels, straggler mitigation for the 13× skew, plane fusion. The framing: a GPU/CPU crossover exists on every device tier — the spikes measured the unoptimized Apple-silicon crossover (~7,073 real-skew LPs), and P08's success metric is reducing it, each optimization an ablation reported by how far it moves the crossover down. CUDA (P09) inherits the optimization ladder at a lower crossover on faster silicon; Metal is the first-try crossover-reduction result, not a stepping stone.T13f (P08's opening task) delivered the regime. An opt-in
hosts_per_edgerestored the canonical k³/4 host population (8,192 hosts at k32 — the previous builder attached one host per edge switch, 512, which was T13e's hidden ceiling), and a compliant 10–90% load sweep achieved 3,816–12,383 mean active LPs, clearing the 7,073 reference at just 29% load. After review round 1 removed a unified-memory measurement confound (~861 MB of retained harness state inflated CPU-first GPU walls 68.6% while device medians were order-stable at 0.65%; controlled protocol collapsed the order split below 0.1%), the sweep measured the crossover directly: pooled GPU/W4 parity at 10,323 mean active LPs, and the unoptimized device substrate 1.37× faster than the matched four-worker CPU at the 12,383-LP frontier, with a nearly flat GPU curve against linearly growing CPU curves. The fairest CPU (W18) still leads the GPU by 1.246× at the frontier, closing monotonically across the sweep — T14's first crossover-reduction target.T14 landed the production backend's correctness milestone. The real semantics now run on device — MSL kernels for horizon reduction and round execution (lazy generators, FIFO/TailDrop, one-selection-per-service-start, exact integer time, boundary-only exchange), genuinely device-resident with host syncs only at bounded, counted wave boundaries. Byte-identical
RunResultagainst the scalar oracle across the conformance corpus, rich mid-state checkpoints, and an end-to-end 10.6M-transition k32 fixture; run-to-run deterministic; explicit device capacity faults. Three review rounds closed one high (au64::MAXsentinel aliasing a real timestamp at the domain edge) and three mediums (sound service-rate capacity bounds, watchdog-safe continuation relaunches, bounded wave encoding); final round clean. Execution is deliberately serial on-device — T15 is the parallelization ladder that turns correctness into the crossover-reduction result.T15a parallelized it — and recalibrated the ladder. One lane per active LP, deterministic parallel exchange, geometry-independent results: 14.8× over serial T14, and Metal now beats the scalar oracle end-to-end from 29% load. But rung 1 exposed that the T13f replay numbers were a machinery-free ceiling: production pays ~96× the replay's per-round cost for real FEL heap operations, event construction, and divergent bodies — so it still trails W4 by 5.1× end-to-end at the frontier. Rung 2 proceeds profile-first: a device-counter decomposition of the round cost decides between the calendar FEL (O(1) FEL ops from the image's exact time lattice), role-split kernels, kind clustering, and layout coalescing.
T15b profiled instead of guessing — and the profile overruled every candidate. Opt-in device-timestamp instrumentation decomposed the round: the four planned optimization rungs together touch at most ~24% of the cost, while serial control machinery — literally one-thread dispatches scanning all 49,152 LPs between the parallel phases — consumes 53% at the frontier and 66% at narrow width. The session honestly landed no optimization (the brief forbade token rungs) and the review returned zero findings at any severity. Rung 2 (T15c) parallelizes those control scans with the same deterministic prefix-sum machinery the worklist uses; upper bound ~2× end-to-end at the frontier.
T15c parallelized the control machinery — rung 2 delivered its full upper bound. The three one-thread scans became 1,024-lane kernels with fixed slot-indexed reduction trees; the control subtotal collapsed 99.75% (84 → 0.21 ms/round) and device time fell 2.9× to 54 ms/round at the frontier. Metal now beats the scalar oracle at all five load points (down to 0.32×); GPU/W4 stands at 2.58–3.73× and GPU/W18 at 5.38–7.13×, review clean with no code defects. The round is now three costs: FEL drain+execute (~22 ms), target merge (~17 ms), and an unattributed ~19 ms residual — rung 3's first job is attributing that residual, then attacking the dominant survivor.
T15d reclaimed the residual — and produced the ladder's first measured rejection. Attributing the ~19 ms residual recovered ~14 ms/round (backend down to 24–48 ms/round; GPU/W4 2.40–3.59×). The rung-3 role split was implemented, measured as a consistent small regression (+3.9% drain, +2.2% device), and reverted with the ablation retained as evidence — establishing that role divergence is not the drain bottleneck on Apple silicon (memory-bound FEL/state access is now the prime suspect) and queuing the mechanism for re-test on CUDA where divergence economics differ. Key reframe: sustained per-round, Metal already beats W4 (~48 vs ~79 ms/round at the frontier); the end-to-end losses on these fixtures are fixed-cost amortization over 18–36 budget-truncated rounds. T15e adds a sustained-duration fixture and honest fixed-vs-marginal reporting, then attacks the drain (calendar FEL / layout) or the merge per the profile.
T15e delivered the audited steady-state ledger — and the production backend's first sustained CPU win. Sustained fixtures (1,879 and 1,128 rounds; byte-parity verified over 1.38 billion transitions) with fixed-vs-marginal separation per engine and complete per-sample retention: at the 12,383-LP frontier, Metal (42.6 ms/round) beats W4 (58.9) sustained — 0.722×, end-to-end included — while W18 (19.1) still leads 2.22×. The drain decomposition ended in a disciplined honest stop (no mechanism cleared the evidence bar), and it killed the calendar-FEL idea empirically: the corpus's time-lattice GCD is 1 ns. One deliberate production change was disclosed and proven (paced source-queue sizing, capacity-1 parity + capacity-0 fault regression). The next rung, T15f, replaces the per-LP heap and the exchange merge with stream decomposition — per-channel monotone FIFO inboxes exploiting order the model already guarantees (the data structure F1's channel bounds point at), with the proven heap retained as fallback and ablation instrument — targeting W18 parity from the merge's 17.4 ms plus drain savings. A same-day portability audit also verified the CPU suite passes byte-identically on aarch64 and x86_64 Linux (237/0/1, zero warnings) with Apple crates fully isolated, clearing the road to CUDA.
T15f reached the bar: statistical parity with the best CPU configuration. The stream-decomposed FEL — per-channel monotone FIFO inboxes exploiting order the FIFO-link model guarantees (the data structure F1's channel bounds point at), with the proven heap retained as fallback — eliminated the exchange merge (17.34 → 0.066 ms/round), halved device time at every load point, and cut event-storage memory 82%. Sustained frontier verdict under a formalized, symmetric parity rule with per-sample evidence: Metal 18.75 vs W18 18.33 ms/round = parity; W4 beaten 4/4 paired (3.1×). The identical-binary ablation isolates the structure's contribution at 2.28×. The full T15 ladder: 164 → 48 → 18.75 ms/round, five rungs, two measured rejections, byte-identity unbroken — including over a 1.38-billion-transition sustained fixture.
T15g and the closing gate: the honest ending. The gate's fresh quiet-machine confirmation exposed that CPU baselines are contention-sensitive at the tens-of-percent level (W18's medians improved 24.2 → 17.6 ms/round across sessions purely with machine quietness) while Metal never moved (±0.05%) — so the final rung, T15g, attacked the remaining gap under the strictest protocol of the project. Every candidate measured as regression or noise and none was committed: a disciplined honest stop. The gate itself failed twice, productively — its first run caught a test-isolation defect whose root cause was an undocumented concurrency envelope, now enforced in the production API (process-wide Metal execution serialization, panic-safe, proven by an eight-executor byte-identity test); its second run enforced the formal dispersion rule against the parity claim.
P08 closed (July 30, 2026) with both framings recorded, neither alone: at the 12,383-LP sustained frontier, Metal 18.74 vs quiet-machine W18 17.74 ms/round — formally trails 1.056× (0/4 paired) under the dispersion rule; approximate parity in plain language. The decisive wins stand beside it: W4 beaten 3.1× sustained (4/4 paired), scalar beaten 34×, event-storage memory cut 82%, and byte-identity unbroken through the entire ladder including 2.05-billion-transition runs. The full ledger: 164 → 18.75 ms/round (8.8×) across five rungs — parallel execution (14.8× over serial), parallel control (−99.75%), residual reclaim (−14 ms), and the stream-decomposed FEL (merge −99.6%, device −53%) — plus three measured rejections (role-split kernels, indirect dispatch, and every T15g candidate), each reverted with its ablation retained as evidence. Methodology findings banked for the paper: quiet-machine protocol with captured machine state as the honest CPU-baseline standard, and the identical-binary streams-disabled ablation isolating the stream structure's contribution at 2.28×. The W18 rematch moved to NVIDIA hardware — where it was promptly won (see P09).
P09 — the CUDA backend
T16 answered feasibility comprehensively in one session: all eight kernels of the resident round loop ported MSL → CUDA C++ (offline nvcc behind the
cudafeature; fat binary carrying sm_121 and sm_89; transfer-explicit buffers with no unified-memory shortcuts; CUDA Graphs with device-resident completion; the Metal-mirroring execution envelope) — byte-exact against scalar on the DGX Spark, clean macOS compile-out. Its review caught an async-readback completion gap (latent corruption on discrete memory), and the fix chain's sanitizer bar delivered the cross-backend hardening dividend: compute-sanitizer racecheck exposed a real scratch-reuse race present in the shipped Metal kernels too — both backends patched, sanitizer-clean (all four modes, zero hazards) now the standing bar.T17a closed the conformance gaps (block-boundary widths, geometry independence 1→1,024 threads, order-sensitive fallback fan-in proven by a perturbation transcript, on-device
u64::MAXedges, rich checkpoints, eight fault arenas, guard panic recovery, feedback/reverse routes — the CUDA suite grew 4 → 17 tests) and caught two real production defects: au64::MAXvalidation rejection and a register-pressure cap silently limitingdays_roundto 768 threads. Evidence hardened to cryptographic provenance (tree hash +Cargo.lockdigest).T17b measured the first CUDA performance — and completed the three-device sustained trilogy at the frontier (12,383 mean active LPs, formal protocol, 4/4 paired, byte-exact): Apple M5 Metal ~parity with its best CPU; Spark GB10 CUDA 17.03 ms/round beats Grace's best (W19, 23.60) by 1.38×; RTX 4090 CUDA 11.49 ms/round beats the i7's best (W23, 32.20) by 2.80× — and 1.85× even end-to-end — all with zero NVIDIA-specific tuning, the inherited Metal ladder only. Short-ladder evidence is dual-clock by review mandate (backend clock vs end-to-end stated separately; short-fixture E2E is fixed-cost-dominated). The k64 lowering pathology was root-caused (per-flow full fat-tree re-validation, effective Θ(k⁷)) and fixed 47× (294.8 → 6.2 s), with byte identity proven by frozen image hashes including an archived historical run at the pre-optimization commit; canonical k48 (147,456 LPs) is hash-proven byte-for-byte on CUDA. In parallel, the GeDES artifact was built and characterized on the Spark: structurally TCP-only (no CBR possible — the same-traffic head-to-head waits for P10b), and its run-to-run variability traces to unseeded workload generation, sharpening our determinism claim to its precise, artifact-proof form.
T17c finished the phase's science. Both rejected Metal rungs were retested under warp economics as fair, one-per-commit ablations — and both were rejected on CUDA too (role-split +6.7%, kind clustering +1.1%, reverted with tree-hash proof), making the cross-architecture finding symmetric: retrofitted warp homogeneity loses everywhere; GeDES's version works because it is architectural, not a reordering. The CUDA phase profile shows the inherited ladder's completeness — the drain is now 91% of the round — and geometry tuning honest-stopped at the 256-thread default. The k48 wide-corpus probe (147,456 LPs, formal protocol) sharpened the device-class story: the Spark's GB10 falls back behind Grace's 19 cores at this width, while the 4090 beats its best CPU at both points (up to 2.23×) with a flat curve across a doubling of load. A review-driven sizing fix made VRAM arithmetic reproducible — and revealed the excluded k48/load90 point actually fits the 4090 (19.6 GB exact), queued for the closing gate.
P10 — scheduler breadth
T18 landed SP and exact WFQ on the scalar oracle and CPU pool. WFQ runs in exact rational arithmetic (
Ratio<BigUint>, zero floats): virtual timeV += Δt·rate/(10⁹·Σ active weights), finish tagsF = max(V,F) + 8·bytes/weight, exact ties broken by canonical arrival order. The F4 one-selection discipline is preserved — selection happens only whenTxReadyexecutes, with arrival-before-selection adversarial fixtures (red-tested against eager selection). The Cartesian matrix tripled to 55,296 comparisons; Lean instance obligations discharged (57 jobs, zero placeholders, standard axioms). Two review rounds hardened it: WFQ checkpoint validation now pins the in-service finish tag (historically red-tested at the parent commit), the Days-vs-legacy class-identity divergence is documented with a regression test (Days's canonical order-independent flow IDs ruled the intended semantics), and the Lean conflict-coverage item took a sanctioned scoping backed by a real discovery — same-class WFQ arrival/completion pairs genuinely conflict, so the conservative mapping is semantically forced and sound. Metal/CUDA reject SP/WFQ with explicit T19 capability diagnostics. T19 solved the bounded-width problem and closed the phase: the device WFQ runs 320-bit rational components with 512-bit recurrence scratch and exact 640-bit comparisons, overflow-faulting (never wrapping), behind validator-enforced width bounds — devices reject what they cannot bound, scalar/CPU keep unbounded exact rationals, identical results wherever both run. The closing gate (second run, after a one-test fix made the assertion literal) fresh-verified the four-backend byte-identical agreement on the shared adversarial fixtures across all three machines, with racecheck clean everywhere.The closing gate refused to round up — then passed everything. Run 1 halted before executing a single test, on a literal reading of the acceptance: the three shared adversarial fixtures were asserted Metal-vs-scalar and CUDA-vs-scalar, but the CPU assertion used different fixtures, so "same fixtures, all four backends" was not literally assertable (the 55,296 matrix covers scalar/CPU broadly, but not those exact three). One mirrored test function later, run 2 fresh-verified the phase across all three machines: 760 local tests including the matrix and k32 acceptance, the Lean audit (zero placeholders, standard axioms), both GPU machines racecheck-clean, the four-backend byte-identical agreement finally literal (18+24+24+24 comparisons), and device overflow-faulting proven non-wrapping. P10 closed with its ledger in evidence — and the phase-gate streak continues: every gate since P08 has caught something real at the boundary.
P10b — TCP on the executor: T23 complete
The executor now runs closed-loop TCP — Reno and CUBIC in exact integer arithmetic on scalar and CPU, byte-identically, with zero floats anywhere in the semantics (
6c65b1a+fdb3dff). CUBIC's window lives in decimal fixed point at 10⁹ nanosegments/segment with exact rational constants (β=7/10, C=2/5), integer SRTT smoothing, and an exact floor integer cube root; the certificate replays byte-exactly in Lean. The closed-loop hooks the generator contract carried since its design activated unchanged — contract-first design vindicated months later; retransmission timers became the stream-FEL fallback heap's first real clients; and the RQ9 number landed: 40-byte reverse ACKs cut the measured safe horizon ~90% (forward bound 1 ns, ACK bound 4 ns at 100 Gb/s) — the honest cost of closing the loop. The validation stack is LeanGuard-primary per the revised plan: the scoping pass ruled the legacy Float/drift-tolerant CUBIC spec would overclaim, so T23 wrote a new exact-integer spec — a 38-column Reno/CUBIC certificate with exact post-state equality on every transition, adversarial campaigns whose mutations die by transition replay, and analytic anchors that pass as exact equalities (slow-start doubling; the Reno sawtooth's closed-form peak 32 / period 16 RTTs / mean 24 on a known-buffer bottleneck). Legacy divergences are documented per the established pattern — all trace to legacy's f64 (Reno CA at ACK 128: 66,047 vs 65,535; CUBIC's first byte-floor gap only at 188.2 simulated seconds).Then the review loop earned its keep: seven rounds, findings 10 → 4 → 2 → 3 → 2 → 3 → 0 (
45720a7..cdbcf49). The trajectory tells the story: rounds 1–2 caught real execution soundness bugs (a safe-horizon violation for sub-MSS segments, retransmission reconstructing the wrong byte length, rto=0 storm acceptance, same-timestamp ACK-burst reservation unsoundness); round 3's survivors were confined to the serialization boundary (mid-stream checkpoints couldn't rebuild the segment ledger); rounds 4–6 were entirely validator exactness — first closing accepted-then-fault gaps (reverse-channel derivation skipped by an early-exit gate, u64-boundary timer arithmetic), then closing produced-then-rejected gaps (ACK sibling double-counting, dormant-timer capacity mixing, generation-blind timer matching). Round 7: CLEAN — with a closure sweep running 60-second Reno and CUBIC loss/recovery fixtures across 32 checkpoint/horizon pairs, every prefix byte-identical, every checkpoint re-validating, every suffix stitching exactly to the uninterrupted run. The validate-before-execute + closure property now holds in both directions: no accepted image faults, no reachable state rejects. Final tally: 908 tests, 0 failures (48 TCP semantics incl. the 192-comparison matrix), Lean 57 jobs zero-placeholder on the standard axioms, four clippy configs clean, frozen pre-TCP hashes untouched. Two review sessions had their final reports killed by codex's content filter (false positives on adversarial TCP probe code); both verdicts survived via the incremental verdict-file discipline adopted after the first kill.T24 ported TCP to the devices — the executor now runs closed-loop TCP on all four backends, byte-identically (
39c3669+eb7825c+4915160, review fixes824b01b+f82d05c). Metal and CUDA execute the full T23 semantic surface — exact-integer Reno/CUBIC, ACK/loss feedback, receiver ranges, the segment ledger with partial-ACK splitting, blocked-flow refill, checkpoint resume, and retransmission timers through the device FEL fallback path — with no floats anywhere: Metal in up to 224-bit limb arithmetic, CUDA in a bounded exact u128 path with proved saturation boundaries, CUDA Graphs and the sm_121+sm_89 fat binary retained. No device deferrals remain for any accepted TCP image; the only rejections left are scenario-level features that exist nowhere yet (BBR, ECN, non-default CUBIC parameters — P10c's inventory), each tested. Conformance: the literal complete-state matrix passes 192 (scalar/CPU) + 64+4 (Metal) + 64+4 (CUDA, per machine) comparisons — counts stated honestly after the review corrected a 2× overstatement in evidence; the k16 (1,024 flows) and k32 (8,192 flows) Reno/CUBIC corpora pass on every backend across all three machines; compute-sanitizer racecheck is zero-hazard on both GPUs; local aggregate 930 tests, 0 failures. The review loop closed in two rounds (5 findings → 0): the one high was a device closure gap — stale retransmission-timeout events that scalar correctly no-ops were rejected by device packing — fixed to exact no-op parity and probed across every stale/live timeout shape. RQ9's measurement machinery landed with fixed-vs-marginal separation and exact closure arithmetic; the formal ladder waits for P11's closed-loop profiles. Five CUDA execution items are explicitly deferred to the closing gate's remote run (the local host has no nvcc).P10b CLOSED — gate PASS on attempt 2. The gate streak held: attempt 1 stopped honestly on madrid when a stale-timer TCP checkpoint hit
CapacityExceededon CUDA — root-caused to the CUDA planner skippingBlockedgenerators (resumed TCP flows are Blocked-with-timer), fixed by adopting Metal's directional derivation; the scoped review of that fix then caught its over-allocation echo (Finished flows reserving phantom recovery work), fixed with a measured −40.9% event-arena tightening. Attempt 2 fresh-verified everything: local 930/0, LeanGuard campaigns both archived and freshly regenerated (5/5 baselines, 6/6 mutation kills), behavioral-parity numbers reproduced exactly, both GPU machines source-hash-verified with all five deferred CUDA probes byte-identical, k16/k32 corpora green on every backend on all three machines, both GPUs racecheck-clean, and an honest RQ9 smoke (Metal trails the CPU 6.25× at k16's 1,024 flows — small-width fixed-cost dominance, exactly as the width thesis predicts; the formal ladder is P11's). The Mechanism API v1 note — the executor↔protocol contract — was audited claim-by-claim by the gate and finalized with its corrections folded: the seven-mechanism inventory, six per-mechanism obligations, stability tiers, the no-semantic-feature-gates policy, and designs for the three P10c vocabulary gaps (RED+ECN marking, rate-based sources, PFC pause).The comparison matrix is staged and waiting. Both external baselines are built and characterized on our hardware: GeDES (built on BOTH machines — Spark and now the 4090 venue itself, zero source changes; seeded runs are byte-identical across GPU arch/ISA/CUDA version, so reference traces are machine-portable; their self-reported clock hides 80–91% of wall at published horizons on the 4090; a ~500× config trap between their Python defaults and published sweep row is documented; their memory table under-reports ~4×, leaving k=64 unproven on 24 GB) and Unison (boston; both the current tree and the ns-3.36.1
unison-evaluationsartifact that GeDES's published 33–2400× multipliers refer to — zero patches either tree). The k=32 fabric is an observed three-way match. Two cross-cutting findings shape every future table: both externals' self-reported clocks hide ~85–87% of their real cost at k=32 (setup/routing excluded — hence the mandatory clock-pairs rule), and Unison's global routing is intractable at k≥16 without nix-vector mode. Planned additions: a minimal disclosed GeDES patch adding paced-UDP load (10/30/60/90%) plus event-count instrumentation (packet-hops and stage-visits under stated definitions), enabling the open-loop three-way even before TCP comparisons mature.Legacy partition — the supersession made structural
With P10b closed, the repository was partitioned per the retirement plan (
76b7235+ four hardening commits): the Nexosim-based engine now lives in a top-levellegacy/workspace crate (days-legacy— flows process models, legacy schedulers, l2, switches, 200 tests of its own), while everything load-bearing for the executor (scenario lowering, topologies, LeanGuard harness binaries) stays current; a newdays-validationcrate holds the differential trajectory tests as the sole, dev-scoped consumer of both sides. The move is provably structural: git rename history preserved, zero logic changes, and the full suite total came through exactly (930/0/15, with an explicit per-crate identity mapping). Two CI lints now enforce the partition permanently viacargo xtask audit: a boundary audit (full resolved-graph reachability with entry-edge allow-listing — no production or build path may reach the legacy engine, and onlydays-legacyitself may live underlegacy/) and a semantic feature-gate audit (the one-canonical-binary policy:cfg(feature)in executor semantic modules is build-breaking outside an enumerated 73-gate backend allow-list). The lints themselves survived a four-round adversarial review that defeated seven successive bypass constructions (transitive paths, impostor packages, dev-edge bridges, shadow crates, trailing-comma and raw-identifier cfg spellings,cfg_if!nested attributes) — with parse-failure-is-fatal and directory-ownership as the closing principles, and one narrow residual limitation recorded honestly (cfg gates smuggled as arguments to custom attribute macros; graded low-moderate accidental plausibility).P10c opens: the vocabulary mechanisms land (T25)
T25 delivered the three protocol-vocabulary mechanisms plus the scheduler family, all in exact arithmetic (
bc96a6d+ review commitsd45dffa,0236b74,23282df,466dadc): deterministic RED and ECN threshold marking withBigUint-exact probability comparisons and validator-derived counter bounds; rate-based sources with fixed-point pacing credit and proved u128 representability; PFC with eight per-priority pause states gating eligibility only at service start, 64-byte control frames (measured horizon effect: 1,000 → 64 ns on the probe fixture), and a real design stance on deadlock — circular pause dependencies are rejected at validation by deterministic cycle detection, since the model has no pause expiry that could bound recovery; and DRR/WRR in exact integer arithmetic. VC and BBR are intentionally excluded with recorded rationale (float-tick legacy semantics; no consuming comparison arm), keeping the parity claim precise. LeanGuard grew exact-Rat WFQ and new SP campaigns — the session falsified the API note's claim that the old WFQ spec was exact (it was Float-state) and filed the API's first errata (E1–E3).The review loop ran four rounds (findings 18 → 6 → 4 → 0) and told the same story as T23's, louder: exactly one semantic defect (multiple PFC controllers sharing a pause bit on branched topologies — fixed with per-controller state and spec lockstep), with everything else validator exactness — checkpoint causal consistency for pause state, reverse/ACK routes joining the deadlock graph, reservation arithmetic honoring what traffic can still actually be produced (past-the-controller packets uncharged, blocked pacing ticks' successor timers counted, stop-time truncation tick-exact). Final aggregate: 1,094 tests, 0 failures, five mechanism campaigns green, all quality gates clean. Next: T26 (DCQCN on these mechanisms, the collective engine's parametric port, DRR/WRR device ports), then the P10c gate.
P10c closes: DCQCN, collectives, device ports, and the gate (T26 + gate)
T26 completed the protocol surface. DCQCN was respecified in exact integer arithmetic — the ppb-scaled alpha recurrence, staged FastRecovery/Additive/Hyper increases, and CNP gating, with checked u128 intermediates and a single floor per complete rational expression — and its LeanGuard campaign closed at 27/27 including a frozen executor-generated certificate byte-compared in both Rust and Lean. The one numeric divergence from legacy (1 bit/s on the fourth repeated-CNP rate, legacy's f64 rounding) is documented with its derivation. The collective layer landed as one parametric generator (RingAllReduce and AllGather as image configurations), and the scheduler family plus DCQCN's rate/ECN prerequisites were ported to Metal and CUDA with racechecks clean on both machines.
The review loop ran five rounds (7 → 5 → 3 → 2 → 0) and repeated the corpus pattern at higher resolution: the reviewer verified the DCQCN controller arithmetic independently in round 1; every finding after was validation completeness or cross-backend parity. The loop's lasting structural gains: universal lossless decimal lowering (every numeric scenario field now parses via source-spanned exact integers — the f64 corruption class is gone compiler-wide, proven by a byte-identical compatibility image), behavior-based device admission (Full-observation mode is admitted when a conservative future-work/route-reachability analysis proves the unported planes dormant, rejected otherwise — with the walk closed over descendant and resident-waiter routes), globally validated collective partitions bound to their declared totals, and a no-panic contract for validators on all accepted states.
The closing gate discharged the phase obligations. A shipped Lean audit driver now checks the full transitive closure behind the five theorems — 1,179 declarations across 31 modules, axiom union exactly {propext, Classical.choice, Quot.sound}, zero placeholders — replacing an unlocatable historical tally. The collective generator received its own exact-integer LeanGuard spec and campaign (46/46) rather than an exemption, taking the all-campaign aggregate to 170/170. The gate report records the full protocol parity table (with VC and BBR as intentional, reasoned exclusions) and the per-mechanism device matrix. The Mechanism API needed no v2 errata across both consumer tasks. Final matrix: 567/0/6.
Parity with legacy Days is now total: every protocol legacy ships runs on the executor byte-identically on serial and CPU backends, with device status stated per mechanism and every unported combination a tested capability rejection.
What comes next
P11 optimizes from measured profiles with the full protocol surface in the mix: the formal RQ9/RQ9a TCP ladder (open-loop versus closed-loop at matched width), the L1 per-LP horizon regime, and the CUDA-side retests of the rungs Metal rejected.
P12 runs the consolidated evaluation and artifact: the eight-arm regime map under honest clocks, analytic anchors and conservation-law monitors, the mutation study, the quantization-error study against GeDES, and the legacy freeze. The baseline fleet is fully staged (ASTRA-sim, HPCC fork, htsim, SimAI, vanilla ns-3 sequential+MPI, the g++-13 Unison rebuild, and the verified GeDES UDP/instrumentation patches).
🤖 Generated with Claude Code