open-standards/proof/proof-rs
Repository files (latest commit first)
Filename Latest commit message Latest commit date
Transaction Science 5da0fe2806 proof-cascade: an interval long past the tick is no evidence that a rail is live
The liveness rule counts intervals and never looked at how long one lasted. A
rail that steps twice a second steps in every interval once sampling slows to
that cadence, and a contended host slows it just so. On an M3 Ultra the same
rail, burned and sampled by the same code in one quiet process, was Frozen in 17
of 17 probes ticking at 25, 100 or 250 ms and Live in 12 of 12 at 500 or 800 ms.
With four test binaries sampling at once, 6 of 20 runs cached Live for the
process, on a rail every other crate on that host called Frozen, and in CI the
status selected the counter.

An IOReport interval now counts only within MAX_INTERVAL_TICKS (3) of the tick
the probe asked for. A longer one shows which rails exist, and is otherwise no
evidence either way: not its advances, not the interval, not its time. So the
300 ms window is 300 ms of intervals that count, or a burst beside one long
interval would fill it. A probe that cannot sample near its cadence ends Frozen
and falls back to its estimator: estimated, never over-claimed.

Three, from interval streams recorded on real hosts and replayed under each cap.
That rail under contention: Live in 57 of 80 streams with no cap, 13 at eight
ticks, 9 at five, 2 at four, none at three. A RAPL counter that is live: Live in
10 of 10 on a quiet host, 9 of 10 with a spinning thread for every core, 2 of 10
with twice as many.

Only IOReport's rails have the cap. RAPL, NVML and a process's counter publish
at least as often as their probes tick, so sampling slowed by contention shows
nothing a quiet probe would not. Capping them too made the tests that hold a
process's counter to Live fail under load: 5 of 27 runs on an M5 Max with four
busy threads a core, four of them on the counter's status.

Each Watched source says the tick its probe asks for: PROBE_TICK for CPU_RAILS,
and no cap for RAPL's packages or a process's counter.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
2026-11-07 03:17:48 -05:00
..
crates proof-cascade: an interval long past the tick is no evidence that a rail is live 2026-11-07 03:17:48 -05:00
Cargo.lock proof-solvers: read each resident z3 decision off z3's own process tree 2026-10-10 18:11:21 -04:00
Cargo.toml Cargo: no minimum-supported-version floor, because the policy is latest stable 2026-11-03 17:42:20 -05:00