open-standards/proof/proof-rs/crates/proof-cascade/tests/rapl_once.rs
Transaction Science 9334ec0c21 proof-cascade: RAPL is a hardware reading only while every package counter keeps advancing
SPEC §5 says a vendor energy counter is a hardware reading only while it is
demonstrably live for the domain the figure claims. The macOS path enforces
that for IOReport's CPU rail; the Linux path did not. `hardware_meter_available`
selected RAPL whenever any `intel-rapl:<n>/energy_uj` was readable, and the
module doc admitted it: "On Linux there is no such probe." A counter that holds,
or republishes in a lump inside the busy window, would have been bracketed and
graded HwShunt.

RAPL now goes through the same probe loop and the same sustained-advance rule
as IOReport: while the probe burns 25 ms of its own thread's CPU before each
re-read, a counter is live only if it advanced in at least five sample
intervals, in at least 80% of the intervals observed, over at least 300 ms. The
domain is the package: the rule watches the zones whose `name` is
`package-<n>`, and because the figure sums all of them, EVERY package counter
must meet it (IOReport needs one CPU rail of either die; RAPL needs each
counter it adds up). A decrease (a wrap) is not an advance. `rapl_status()` is
probed once per process behind a `OnceLock` and cached; the selection and
`rapl_power_over` gate on it through `admits_counter`, which admits only
`Live`, so a counter that is readable but not live yields `None` before any
window runs and the work never runs. The new public `CounterStatus`
(`Unavailable`, `Absent`, `Frozen`, `Live`) says why, and `proof --measure`
prints `rapl_status=` beside `ioreport_status=` and gives the RAPL reason on
Linux.

The figure itself changes in one place: it sums the package zones only.
Before, every readable top-level zone was summed, and on machines that expose
`psys` (the platform zone, which covers the package) that counted the package
energy twice. `psys` is neither summed nor probed now.

To share the machinery rather than copy it: the thread CPU clock, the wall
clock and the burn tick move out of the macOS-only IOReport module into a
`probe_clock` module built on macOS and Linux (CLOCK_THREAD_CPUTIME_ID is 16
on macOS, 3 on Linux). `RailWatch` takes a `Watched` — which channels, and one
or every one — whose default is the IOReport CPU rails with "any one", so the
IOReport rule and every IOReport test are unchanged. `probe_with` is now
`probe_watching(CPU_RAILS, ..)`. The RAPL composition, `rapl_probe_with`, is
generic over its zone reader, so the tests run that very composition on
scripted zones on every platform.

Tests (all pure and scripted, run here on macOS):
- a package counter advancing at every read is Live at the twelfth 25 ms
  interval, and the rule was handed each value as read;
- constant, one-step and two-step counters are Frozen after the whole budget;
- one package advancing and one holding is Frozen — the same reads under the
  any-one-rail rule are Live, which pins what `every` decides — both advancing
  is Live, and two packages advancing in alternate intervals are Frozen;
- a moving `psys` beside a holding package is Frozen, and zones with no package
  are Absent; a wrap that then holds is Frozen;
- no readable zone is Unavailable with no read or tick, and zones readable only
  at the open give no verdict after the five-budget cap;
- the status maps one to one and only `Live` meters: declined statuses run no
  bracket and no work;
- the package name and the read: `package-<n>` only, each package counter with
  its own value, `psys` left out;
- `tests/rapl_once.rs`: eight threads asking at once see one status, and on
  Linux the production probe ran once (off Linux: Unavailable, zero runs).

Falsified, each restored through git before the next: RAPL's `every` set to
"any" fails the every-package test; reading `psys` into the sample fails the
read and psys tests; watching IOReport's CPU rails instead of the package
counters fails five tests; mapping Frozen to Live fails five; admitting every
status fails four.

`cargo test --workspace` and the proof-conformance binary pass on macOS (M5
Max, macOS 27.0.1). The Linux path is compile-checked only:
`cargo check --workspace --tests` and `cargo clippy --workspace --all-targets`
for x86_64-unknown-linux-gnu are clean. Not run on Linux here, so the real
sysfs reader and the Linux-only gate (`hardware_meter_available` and
`rapl_power_over` gating on the cached status) have no runtime test; a mutation
of that gate cannot be caught on macOS.

Co-Authored-By: Claude Opus 5.5 <[email protected]>
2026-09-30 20:39:39 -04:00

41 lines
2 KiB
Rust

//! The RAPL liveness probe behind `rapl_status()` runs once per PROCESS,
//! however many threads ask at once: a probe per call would burn about a
//! second of CPU on each caller's thread where the counters are readable, and
//! could flip the verdict mid-process.
//!
//! This file holds this one test, so that it runs in a process of its own and
//! IS the first use of the RAPL meter in that process. The counter it reads,
//! `real_rapl_probe_runs()`, counts runs of the production probe
//! (`rapl_host_status`, whose first statement it is), not lookups of the cache.
//! Off Linux there is no RAPL: the status is `Unavailable` and no probe runs.
use proof_cascade::meter::{rapl_status, real_rapl_probe_runs, CounterStatus};
use std::sync::{Arc, Barrier};
#[test]
fn the_rapl_liveness_probe_runs_once_per_process() {
assert_eq!(real_rapl_probe_runs(), 0, "the RAPL meter was used in this process before this test");
const THREADS: usize = 8;
let gate = Arc::new(Barrier::new(THREADS));
let handles: Vec<_> = (0..THREADS)
.map(|_| {
let gate = gate.clone();
std::thread::spawn(move || {
gate.wait();
(rapl_status(), rapl_status())
})
})
.collect();
let seen: Vec<_> = handles.into_iter().map(|h| h.join().expect("a probing thread panicked")).collect();
let runs = real_rapl_probe_runs();
eprintln!("rapl cache: {THREADS} threads saw {:?}; real RAPL probe runs in this process: {runs}", seen[0].0);
for (i, (status, again)) in seen.iter().enumerate() {
assert_eq!((*status, *again), (seen[0].0, seen[0].0), "thread {i} was given a different status");
}
if cfg!(target_os = "linux") {
assert_eq!(runs, 1, "the RAPL liveness probe ran {runs} times in this process ({THREADS} threads asked at once)");
} else {
assert_eq!(seen[0].0, CounterStatus::Unavailable, "RAPL off Linux");
assert_eq!(runs, 0, "a RAPL liveness probe ran off Linux");
}
}