Days Executor: exact safe-horizon CPU/GPU execution - #104
Open
baochunli wants to merge 141 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
Summary: - Derive required channel lookahead from live TCP data and executable generator states while retaining static route bounds for dormant channels. - Enforce reachable timer, recovery, and ledger invariants before execution. - Preserve scheduled sends across ACK processing while retaining required fast and partial retransmissions. - Add reconstructed regressions and adversarial checkpoint-closure coverage. Rationale: - Accepted images must not fault for validation-checkable reasons, and every runtime-produced continuation must validate again. - Scalar and CPU must retain exact byte identity and sound safe horizons. Tests: - cargo test -p days-executor -- --show-output - cargo test --features test -- --show-output - cargo test -p days-executor --features metal-spike -- --show-output - cargo test --features test,metal-spike -- --show-output - cargo clippy with default, metal-spike, and test feature coverage - cargo fmt --all -- --check - lake build, placeholder scan, and axiom audit
Summary: - Reserve finite-run TCP timer-generation capacity during validation. - Reject image RTOs that cannot form a deadline through the stop time. - Cover exact rejection, maximum legal values, parity, and closure. Rationale: - Accepted Scalar and CPU images must not fault on validation-checkable timer counter or deadline overflow. - Runtime checked arithmetic remains as defense in depth. Tests: - Four default and metal-spike suites: 904 passed, 0 failed. - TCP semantics: 46 passed; Cartesian matrix: 192 comparisons. - Frozen hashes, Lean audit, four clippy configs, fmt, and diff checks.
Summary: - Count only sender-delivered ACK arrivals in TCP capacity bounds. - Ignore dormant beyond-stop events when anchoring service headroom. - Accept stale same-identity timer events while requiring a live match. - Add Scalar/CPU checkpoint-closure regressions for all three findings. Rationale: - Reachable checkpoints must revalidate without weakening conservative overflow reservations or changing the serialized event format. Tests: - 908 aggregate tests passed across default and Metal-spike suites. - 48 TCP semantics tests and the 192-comparison matrix passed. - Frozen hashes, Lean audits, four clippy configs, and rustfmt passed.
Summary: - port exact Reno and CUBIC transitions, ACK feedback, receiver state, ledgers, blocked refill, and heap-class retransmission timers to Metal and CUDA - extend the device ABI, sizing, readback, and byte-identity tests for complete TCP state Rationale: - close the P10b device capability gap with integer-only transitions that preserve the scalar oracle on all supported backends - retain exact checkpoint and timer semantics across device FEL fallback Tests: - cargo test -p days-executor -- --show-output - cargo test -p days-executor --features metal-spike -- --show-output - CUDA executor suites on madrid and boston - compute-sanitizer racecheck on madrid and boston
Summary: - lower exact TCP Reno and CUBIC scenarios into executor images with precise diagnostics for unsupported variants - add k16 and k32 TCP conformance corpora plus TCP-aware sustained RQ9 sampling with retained fixed and marginal observations Rationale: - exercise one-flow-per-host fat-tree workloads at canonical host scale before the formal benchmark ladder - keep fixed-cost separation explicit for closed-loop TCP measurements Tests: - cargo test --features test -- --show-output - cargo test --features test,metal-spike -- --show-output - T24_CORPUS=all cargo test --features test,metal-spike --test t24_tcp_corpora -- --ignored --show-output - RQ9 TCP smoke on local Metal
Summary: - update two equivalent iterator expressions for current Rust Clippy Rationale: - keep the required deny-warnings gate green on the newer remote CUDA toolchains without changing simulator behavior Tests: - cargo clippy --features test -- -D warnings - cargo clippy --features test,metal-spike -- -D warnings - cargo clippy --features test,cuda -- -D warnings on madrid and boston
Summary: - pack stale timeout events for Metal and CUDA as guarded no-ops - add cross-backend stale-timer, partial-ACK, and timer-bound probes Rationale: - preserve validate-before-execute and checkpoint closure on devices - cover TCP semantics absent from the shared device matrix Tests: - cargo test -p days-executor --test tcp_semantics -- --show-output - cargo test -p days-executor --features metal-spike --test tcp_semantics -- --show-output - cargo test -p days-executor -- --show-output - cargo test -p days-executor --features metal-spike -- --show-output - cargo clippy -p days-executor -- -D warnings - cargo clippy -p days-executor --features metal-spike -- -D warnings CUDA execution is deferred to the P10b remote gate because local nvcc is unavailable.
Summary: - cover starts-before and starts-after lowering rejections - cover source-routing and explicit-path lowering rejections Rationale: - keep retained scenario capability boundaries executable and diagnostic - prevent unsupported flow options from silently losing coverage Tests: - cargo test --features test --test scenario_lowering -- --show-output - cargo test --features test -- --show-output - cargo test --features test,metal-spike -- --show-output - cargo clippy --features test,metal-spike -- -D warnings
Summary: - derive CUDA data and feedback bounds with the established Metal logic - reserve retransmission and refill work for blocked TCP checkpoints - exclude ledger-only TCP seeds while retaining explicit capacity faults Rationale: - CUDA skipped blocked generators before its TCP capacity calculation - live timeout work could therefore exhaust an under-sized observation log - stale nonmatching timeouts remain guarded, observation-silent no-ops Tests: - 930 local default and Metal tests; 15 ignored - madrid CUDA TCP semantics: 52 passed, including 68 comparisons - madrid compute-sanitizer racecheck: 0 errors, warnings, or hazards - frozen hashes, Lean, four Clippy configs, fmt, and diff checks pass
Summary: - Skip future attempt capacity for Finished TCP generators on Metal and CUDA. - Assert the exact tightened device arena plan for a completed checkpoint. Rationale: - Finished flows have no unsent or in-flight bytes, so the recovery allowance reserved phantom data and ACK work across downstream device arenas. - Preserve the conservative Scheduled and Blocked TCP bounds and the existing TCP-before-constant generator ordering. Tests: - Four local default/Metal suites: 930 passed, 0 failed, 15 ignored. - TCP semantics: 51 default, 53 Metal, and 52 CUDA on madrid. - Frozen hashes, Lean build/axioms, four Clippy configs, and fmt passed.
Summary: - Move the Nexosim engine, examples, and owned tests into days-legacy. - Keep lowering, topology configuration, and harness utilities shared. - Isolate cross-engine tests in days-validation with dev-only edges. - Add workspace boundary and semantic feature-gate audits to CI. Rationale: - Make the legacy/current ownership boundary explicit without changing simulator behavior or retiring the legacy surface. - Mechanically prevent production reverse dependencies and semantic feature gates from eroding that boundary. Tests: - Default and Metal matrices: 930 passed, 0 failed, 15 ignored. - Frozen pre-TCP gate: 2 passed with all five hashes unchanged. - Legacy all-feature suite: 211 passed, 0 failed, 0 ignored. - cargo xtask audit; cargo test -p xtask; cargo fmt --all -- --check. - Six Clippy configurations with -D warnings; lake build and axiom audit.
Summary: - Traverse Cargo's full resolved normal/build graph to the real legacy package ID. - Resolve the validation dev exception by exact source and target IDs. - Detect qualified cfg macros and restore both partition surface slips. - Add reviewer-exact regression tests for all demonstrated bypasses. Rationale: - Direct dependency declarations and package names were bypassable via transitive paths and same-named impostors. - Preserve the legacy public API and correct shared-module ownership documentation. Tests: - cargo test -p xtask -- --show-output - cargo xtask audit - Default and Metal matrices: 930 passed, 0 failed, 15 ignored - Frozen preoptimization hashes: 2 passed, 0 failed - lake build and 19-declaration axiom audit - Required and new-crate Clippy configurations with -D warnings - cargo fmt --all -- --check; git diff --check
Summary: - Audit workspace entry edges whose resolved paths reach the legacy package. - Match only exact standard/core cfg macro paths and add regressions. Rationale: - Prevent dev dependencies from bypassing the boundary through a bridge. - Avoid inventorying unrelated third-party cfg macros. Tests: - cargo test -p xtask -- --show-output - cargo xtask audit - Default and Metal matrices: 930 passed, 0 failed, 15 ignored. - Frozen hash gate, Lake/axiom audit, Clippy, and rustfmt.
Summary: - make recognized cfg parsing tolerant of trailing commas and fatal on errors - normalize raw identifiers and scan nested macro token streams - enforce exclusive legacy directory ownership and reachability - add regressions for the reviewer probes and adversarial variants Rationale: - prevent valid Rust syntax from escaping the semantic gate inventory - prevent shadow crates from adding code outside the legacy boundary Tests: - cargo test -p xtask -- --show-output - cargo xtask audit - full default and Metal matrices (930 passed, 0 failed, 15 ignored) - frozen image tests, lake build, axiom audit, Clippy, and fmt
Summary: - scan cfg and cfg_attr attributes through every opaque macro token group - fail on uncaptured feature keys in cfg-shaped and cfg_attr residual tokens - add compiling cfg-if, nested attribute, residual, and backstop regressions Rationale: - prevent macro expansion syntax from hiding semantic feature gates - preserve exact allow-list accounting and fatal recognized parse failures Tests: - cargo test -p xtask -- --show-output (33 passed) - cargo xtask audit - default and Metal matrices (930 passed, 0 failed, 15 ignored) - frozen image tests, lake build, axiom audit, Clippy, and fmt
Summary: - add exact RED/ECN, paced rate sources, PFC, DRR, and WRR - add validator closure rules, capability rejections, and lowering - add Lean instances and exact LeanGuard campaigns for P10c and SP Rationale: - open the finalized mechanism vocabulary for T26 protocols - preserve exact scalar/CPU semantics and reject unsupported devices Tests: - default and Metal-equivalent suites: 1000 passed, 15 ignored - lake build and LeanGuard P10c, SP, and WFQ campaigns - cargo xtask audit, the Clippy matrix, and cargo fmt
Replace shared PFC pause bits with controller-scoped state and close the rate, scheduler, RED, PFC, and time-capacity representability gaps found in review. Add exact Rust-connected replay certificates for rate, PFC, DRR, WRR, and continuous AQM trajectories, with matching LeanGuard campaigns. Keep legacy flow-ID allocation deterministic across its documented matrix and preserve the frozen pre-TCP lowering hashes. Tests: cargo fmt --all -- --check Tests: cargo xtask audit Tests: cargo clippy (all four required configurations, -D warnings) Tests: focused T25 mechanism, lowering, legacy, and frozen-hash suites Tests: lake build and P10c mechanism/AQM replay campaigns Tests: full default and metal-spike package matrix (running at commit time)
Close the remaining PFC lane, controller, hysteresis, ACK sizing, and capability boundaries found by the post-fix audit. Count blocked rate tokens exactly once and make DRR reachability and trace bounds explicit. Reject unrepresentable byte occupancy for every queue policy, preserve RED transition order, and replay the new boundary rows in Lean. Raise the WRR replay fuel to cover a full wrapped scan. Tests: - focused executor and lowering regressions: 72 passed - LeanGuard mechanism campaign: 11/11 - LeanGuard AQM campaign: 8/8 - lake build: 58 jobs - all four Clippy configurations - cargo xtask audit - frozen pre-optimization hashes: 2/2
Summary: - Reconcile checkpoint pause membership with monitor state and pending control frames, and include reverse routes in PFC deadlock analysis. - Bound PFC work by resident packet position and count rate work only through the inclusive simulation stop. - Add probe-derived regressions and live checkpoint closure guards. Rationale: - Reject orphaned pause states and reverse-route cycles before execution. - Avoid boundary false rejections for completed route prefixes and dormant rate timers without weakening upstream or stop-equality reservations. Tests: - Default matrix: 510 passed, 0 failed, 6 ignored. - Metal matrix: 572 passed, 0 failed, 9 ignored. - Frozen hashes, xtask audit, fmt, four Clippy configs, Lean build, axiom audit, and the 11/11 P10c campaign passed.
Summary: - Count executable Rate packets, successor timers, and payloads exactly. - Bound partial Rate frames by bytes that can still be produced. - Add stop-boundary, sequence-capacity, and PFC frame regressions. Rationale: - Prevent accepted images from exhausting origin sequence space at runtime. - Avoid rejecting legal checkpoints whose later pacing ticks exceed stop. Tests: - Full default and Metal matrix: 1,094 passed, 0 failed, 15 ignored. - Four Clippy configurations, rustfmt, xtask audit, and frozen hashes. - P10c campaign 11/11; Lean build and axiom audit.
Summary: - Add a parametric collective generator with ring all-reduce and all-gather configurations. - Add exact fixed-point DCQCN with ECN/CNP feedback, rate control, staged recovery, timers, and capacity closure. - Port rate pacing, ECN persistence, DRR, and WRR to Metal and CUDA. Rationale: - Keep collectives image-driven and CCL-agnostic while preserving internal dependency causality. - Replace floating-point DCQCN behavior with replayable integer semantics and explicit device capability boundaries. - Enforce API v1 state, representability, and bidirectional closure obligations at legal maxima. Tests: - Default and Metal matrices: 1,164 passed, 0 failed, 15 ignored. - Madrid and Boston CUDA: 263 passed, 0 failed, 3 ignored each; Rate, ECN, and DRR/WRR racecheck clean on both. - Four Clippy surfaces, fmt, xtask audit, and frozen hashes pass.
Summary: - Add exact integer DCQCN semantics and an event-log checker. - Add an executor-generated trace fixture and mutation campaign. - Remove the legacy native_decide dummy and register the campaign. Rationale: - Prove executor recurrence and state continuity without floats. - Keep axioms within the sanctioned union and avoid native_decide. Tests: - lake build (58 jobs) - DCQCN campaign (27/27); all LeanGuard campaigns pass - Axiom and proof-placeholder audits
Summary: - Parse DCQCN scenario decimals directly into exact scaled integers. - Validate collective partitions and every DCQCN packet-plane owner. - Reject marked non-data and reserve blocked DCQCN pacing only once. - Keep device ECN marking data-only and reject unsupported Full planes. - Add exact-boundary, one-past, closure, and backend regressions. Rationale: - Close accepted-image faults, false rejections, and cross-backend drift. - Claim untouched Summary parity where device transition planes are absent. - Frozen image gate stayed 2/2; no frozen hash changed. Tests: - cargo fmt --all -- --check - four warnings-denied Clippy surfaces - cargo xtask audit (both audits pass) - focused default executor 166/166; focused Metal 139/139 - DCQCN 16/16; collectives 11/11; frozen images 2/2 - default package matrix 554/0/6 - lake build; DCQCN LeanGuard campaign 27/27 - Madrid and Boston CUDA focused suites 119/119 each - two fresh racechecks per CUDA host: 0 errors/warnings/hazards
Make every executor scenario numeric lowering path exact, bind collective partitions to their declared totals, and scope collective no-op rules by algorithm. Admit device Full observations only when static future-work analysis proves omitted transition planes dormant. Add boundary and false-rejection regressions for all review findings.
Summary: - Close Full-mode dormancy analysis over resident service waiters and alternating TCP descendant routes. - Normalize exact decimal zero before bounded exponent conversion while preserving nonzero range diagnostics. Rationale: - Prevent device admission from accepting runs that later populate omitted AQM, DRR, or WRR transition planes. - Treat zero according to its exact value regardless of the decimal exponent. Tests: - Default matrix: 563 passed; 0 failed; 6 ignored. - Focused Metal: 143 passed; decimal and DCQCN: 21 passed. - Formatting, four Clippy surfaces, audits, frozen hashes, Lean, and DCQCN.
Summary: - Accept scalar checkpoints whose stale RTO has no packet descriptor. - Bound generator delays with exact reachable sizes and add regressions. Rationale: - Device validators must handle every valid checkpoint without panic. - Existing device timer packing already treats reclaimed RTOs as no-ops. Tests: - Full default matrix: 566 passed, 0 failed, 6 ignored. - Focused Metal: 147 passed; fmt, Clippy, audits, and Lean gates pass.
Summary: - Traverse every DaysExecutor declaration behind the five proof roots. - Reject unapproved axioms and forbidden proof escape hatches. - Run the reproducible audit in the existing LeanGuard workflow. Rationale: - Replace the unsupported historical declaration count with a checked source. - Keep the paper trust-base claim reproducible as the proof tree evolves. Tests: - lean/scripts/audit-days-executor-axioms.sh - cargo fmt --all -- --check - git diff --check
Summary: - Emit exact scalar progress records for every collective prerequisite edge. - Replay stage continuity, packet arrivals, activation, and chunk recurrence. - Add four scalar fixtures and a 46-case adversarial campaign. Rationale: - Discharge the collective LeanGuard obligation instead of taking an exemption. - Cover ordinary, partial-zero, inbound-triggered, and local-triggered stages. Tests: - cargo test -p days --test t26_collective_lowering -- --show-output - bash lean/scripts/run-p10c-collective-campaign.sh - cargo fmt --all -- --check - git diff --check
Summary: - Group collective certificate context into one explicit value. - Preserve the exact progress record and activation behavior. Rationale: - Keep the helper below the warnings-denied argument-count limit. - Close the first fresh-gate finding without suppressing the lint. Tests: - cargo clippy -p days-executor -- -D warnings - cargo test -p days --test t26_collective_lowering -- --show-output - cargo fmt --all -- --check - git diff --check
Summary: - Split the feature-gated full-load runtime loop into five named fixture tests so nextest launches one process per fixture. - Add `cargo xtask t13f-full-load` and document the debug-only, read-only-fixture contract. - Declare suite-structure change: the T13f all-feature count is 4 -> 8 (+4), with one runtime test becoming five. Rationale: - Keep overflow panics and debug assertions active while recovering wall time through process parallelism. - Leave T15e unchanged because its sustained runtime checks are ignored, feature-gated, and materially asymmetric. Tests: - `cargo xtask t13f-full-load` (5/5 passed, 4568.42 s wall) - Recorded ~4 h serial precedent cited; serial variant not rerun - `cargo fmt --all -- --check` - `cargo test -p xtask` - `cargo xtask audit` (both audits passed) - Standard Clippy surfaces plus targeted xtask/validation Clippy - Width-via-load fixture SHA-256 values unchanged
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