energy tests: the load-sensitive tick floor in proof-cascade and sandbox-meter #181

Merged

dcharlot merged 1 commit from fix/energy-tick-floor-proof-sandbox into main 2026-10-07 14:38:51 -04:00

Conversation 0 Commits 1 Files changed 7 +298 -84

2026-10-07

Transaction Science

energy tests: the load-sensitive tick floor in proof-cascade and sandbox-meter ...

#166 fixed this class of defect in `eoc-meter` and `jouleclaw-energy`: an
energy-probe test asserting a floor on thread CPU per tick, which the host's
scheduler controls, failing on the dev Mac because the dev Mac is also the
macOS runner. The same code exists in two more crates, and the same assertion
with it. CI surfaced `proof-cascade` by failing an unrelated PR; sweeping for
the pattern found `sandbox-meter` as well, rather than waiting for another
round.

A tick spins until the thread's CPU clock advances 25 ms **or** a 500 ms wall
cap passes. Both copies carried a comment asserting the opposite — "the tick
burns thread CPU time, so host load does not shorten it; only its wall-clock cap
can" — a sentence containing its own refutation, since the cap is how load
shortens a tick.

The two outcomes that matter are not separable by time: a spin the host starved
into the cap and a tick that simply slept both show a long wall span against
little CPU. I tried a per-turn CPU floor first, reasoning that a turn is fixed
work so starvation lowers turns-per-second rather than the cost of a turn.
Measuring refuted it: a turn that sleeps 1 ms costs 13.3-15.8 µs of thread CPU
against a real turn's 2.13-2.92 µs, because a blocking body's context switch is
charged to the thread. Even the direction was wrong.

So each tick reports what it did. `spin_tick` / `spin_for` return a
`TickOutcome` — the CPU it saw itself burn, and how many turns of the spin loop
it ran — and each probe collects one per tick, alongside the interval's wall
span beside its CPU span. Per tick: the loop ran at all (a tick that never span
did not burn CPU, at any load), and the tick stopped for one of its two stated
reasons rather than early. The gaps measured by the tests' own clocks still
bound it from above and keep CPU under wall.

- **proof-cascade**: three load-sensitive sites — `assert_sampling`'s
  per-interval floor, an aggregate floor over a whole scripted call, and a
  per-interval floor in the live-rail test. `ProbeRun` gains `interval_wall` and
  the per-tick outcomes; `burn_thread_cpu` reports the CPU it was already
  computing.
- **sandbox-meter**: the per-interval `PROBE_TICK / 2` floor. This crate already
  had `assert_tick` using the either-condition rule for the tick itself, so the
  interval check now matches the crate's own convention — and both are stronger
  for the spin count, since that rule alone admits a tick that slept through its
  cap. `TickOutcome` becomes public because it already appears in a public
  signature: `RaplPackages::live_in` and `counter_liveness` take a tick that
  returns it, so `sandbox-exec-microvm` has to name it and build one.

Where a scripted tick stands in for the burn — fake powercap trees, the MSR
fakes, the hardware test's own oracle — it reports a turn, with a comment saying
that this is the test declaring a real spin ran and not a figure chosen to clear
a threshold. The hardware test's tick keeps using `oracle::burn`, so the oracle
stays independent of what it checks.

Three doc comments asserting "a tick burns a full tick however loaded the
machine is" are corrected in place; leaving that beside a fixed assertion would
reinvite the mistake.

Two call sites are `cfg(target_os = "linux")` and invisible to every run on this
host: `sandbox-meter/tests/rapl_hardware.rs`, which CI's jetson-hub job caught,
and `probe::counter_liveness_tick`, reached on the Linux side through
`MsrRaplMeter::host`, which `cargo check --target aarch64-unknown-linux-gnu
--all-targets` caught. That check is a weak oracle — it runs nothing — but it is
the right shape for a type mismatch in code the host never compiles.
`CARGO_FEATURE_NO_NEON=1` is needed, or blake3's build script wants Linux C
headers. The whole sandbox workspace cannot cross-check (`zstd-sys` needs a real
cross compiler), so instead I confirmed that nothing outside these crates
references the changed entry points, which makes the per-crate checks exhaustive
for callers.

Falsified in both crates: a tick that sleeps instead of spinning, and a tick
skipped entirely. One sleep falsification first looked like a pass and was a
compile error — checked, not assumed. In proof-cascade a tick cut short of both
stopping conditions is caught too.

Verified: proof-rs 139 passed, sandbox-rs 324 passed, and the five touched
crates check clean for aarch64-unknown-linux-gnu. The two clippy warnings in
proof-cascade are in untouched code, the same pair that predates the change in
eoc-meter — these files are copies of one another, which is why the defect was
in four places.

Co-Authored-By: Claude Opus 5 <[email protected]>

f1b662078b

• View at this point in history

2026-10-07 10:03:30 -04:00