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

dcharlot commented 2026-10-07 10:05:06 -04:00

Owner

Copy link

Follow-on to #166, not a duplicate of it. #166 fixed this class of defect in
eoc-meter and jouleclaw-energy; its versions are untouched here. The same
code exists in two more crates, with the same assertion.

The defect

A probe tick spins until the thread's CPU clock advances 25 ms or a 500 ms
wall cap passes. Both copies asserted a floor on thread CPU per tick, and both
carried a comment asserting the opposite:

The tick burns thread CPU time, so host load does not shorten it; only its
500 ms wall-clock cap can

The sentence contains its own refutation — the wall cap is how load shortens a
tick. CI surfaced proof-cascade by failing an unrelated PR (#177); sweeping
for the pattern found sandbox-meter too, rather than waiting for another
round.

Why not a threshold

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 — a turn is fixed work, so starvation should
lower turns-per-second rather than the cost of a turn. Measuring refuted it:

tick body	thread CPU per turn
real spin, idle host	2.13–2.51 µs
real spin, 18 competing busy loops	2.70–2.92 µs
turn that sleeps 1 ms	13.3–15.8 µs

A blocking body's context switch is charged to the thread, so it costs more
per turn than arithmetic. Even the direction was wrong.

What they assert now

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, with the interval's wall span recorded 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 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 get stronger
  for the spin count: 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 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 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 Linux-gated sites this host cannot see

• sandbox-meter/tests/rapl_hardware.rs is #![cfg(target_os = "linux")]. CI's
  jetson-hub job caught it.
• probe::counter_liveness_tick, reached on the Linux side through
  MsrRaplMeter::host. cargo check --target aarch64-unknown-linux-gnu --all-targets caught it.

That cross-check is a weak oracle — it runs nothing — but it is exactly the
shape for a type mismatch in code the host platform never compiles.
CARGO_FEATURE_NO_NEON=1 is required, 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 nothing outside these crates references
the changed entry points, which makes the per-crate checks exhaustive for
callers.

Verification

proof-rs 139 passed, sandbox-rs 324 passed. All 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 being copies of one another, which is why the defect
was in four places.

Falsifications:

reverted	caught by
tick sleeps instead of spinning	spins > 0, both crates. Not caught by the weaker intermediate version I tried — which is how I found that version was wrong
tick skipped entirely	spins > 0
tick cut short of both stopping conditions	the either-condition bound (proof-cascade)

One sleep falsification initially looked like a pass and turned out to be a
compile error. Checked, not assumed.

🤖 Generated with Claude Code

**Follow-on to #166, not a duplicate of it.** #166 fixed this class of defect in `eoc-meter` and `jouleclaw-energy`; its versions are untouched here. The same code exists in two more crates, with the same assertion. ## The defect A probe tick spins until the thread's CPU clock advances 25 ms **or** a 500 ms wall cap passes. Both copies asserted a floor on thread CPU per tick, and both carried a comment asserting the opposite: > The tick burns thread CPU time, so host load does not shorten it; only its > 500 ms wall-clock cap can The sentence contains its own refutation — the wall cap *is* how load shortens a tick. CI surfaced `proof-cascade` by failing an unrelated PR (#177); sweeping for the pattern found `sandbox-meter` too, rather than waiting for another round. ## Why not a threshold 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 — a turn is fixed work, so starvation should lower turns-per-second rather than the cost of a turn. Measuring refuted it: | tick body | thread CPU per turn | |---|---| | real spin, idle host | 2.13–2.51 µs | | real spin, 18 competing busy loops | 2.70–2.92 µs | | **turn that sleeps 1 ms** | **13.3–15.8 µs** | A blocking body's context switch is charged to the thread, so it costs *more* per turn than arithmetic. Even the direction was wrong. ## What they assert now 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, with the interval's wall span recorded 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 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 get stronger for the spin count: 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 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 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 Linux-gated sites this host cannot see - `sandbox-meter/tests/rapl_hardware.rs` is `#![cfg(target_os = "linux")]`. CI's jetson-hub job caught it. - `probe::counter_liveness_tick`, reached on the Linux side through `MsrRaplMeter::host`. `cargo check --target aarch64-unknown-linux-gnu --all-targets` caught it. That cross-check is a weak oracle — it runs nothing — but it is exactly the shape for a type mismatch in code the host platform never compiles. `CARGO_FEATURE_NO_NEON=1` is required, 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 nothing outside these crates references the changed entry points, which makes the per-crate checks exhaustive for callers. ## Verification `proof-rs` 139 passed, `sandbox-rs` 324 passed. All 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 being copies of one another, which is why the defect was in four places. Falsifications: | reverted | caught by | |---|---| | tick sleeps instead of spinning | `spins > 0`, both crates. **Not** caught by the weaker intermediate version I tried — which is how I found that version was wrong | | tick skipped entirely | `spins > 0` | | tick cut short of both stopping conditions | the either-condition bound (proof-cascade) | One sleep falsification initially looked like a pass and turned out to be a compile error. Checked, not assumed. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 1 commit 2026-10-07 10:05:06 -04:00

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

#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]>

dcharlot referenced this pull request 2026-10-07 10:05:26 -04:00

[superseded by #181] energy tests: assert what the probe reports, not what the host's scheduler allows #178

dcharlot merged commit 271573c21b into main 2026-10-07 14:38:51 -04:00

dcharlot referenced this pull request from a commit 2026-10-07 14:38:53 -04:00

Merge pull request 'energy tests: the load-sensitive tick floor in proof-cascade and sandbox-meter' (#181) from fix/energy-tick-floor-proof-sandbox into main

dcharlot referenced this pull request from a commit 2026-10-08 14:36:23 -04:00

wai: a from-rest burst asserted a 2 ms race, and linux-arm64 called it

dcharlot referenced this pull request 2026-10-08 14:37:59 -04:00

wai: a from-rest burst asserted a 2 ms race, and linux-arm64 called it #192

Sign in to join this conversation.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

Transaction-Science/open-standards!181

No description provided.