proof-cascade: measure CPU work with the per-process energy counter, which macOS 27 keeps live #120
Loading…
Reference in a new issue
No description provided.
Delete branch "proof-cascade/process-energy"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
On macOS 27 an unprivileged process sees IOReport's CPU energy rails republished only in rare lumps, so #115 makes proof-cascade's
--measuredecline there. The kernel has another counter it keeps per process,ri_energy_njfromproc_pid_rusage(getpid(), RUSAGE_INFO_V6). That counter is live. It is a public libproc call, with no entitlement and no privilege.What it measures
measure_marginal_ujuses it.workalready runs on every spare core in-process, so the counter is read before the workers start and again after they are joined. No idle subtraction is needed, and other processes are excluded by construction.firstand stays ModelBased.Measured (debug builds, macOS 27.0.1)
Live(35/35 oracle reads changed)Live(29/29)proof --measureTests and mutations
ri_energy_njat byte 336;Not covered
Updates
PROCESS_COUNTERdropped the removedeveryfield.🤖 Generated with Claude Code
On both Macs that run this suite (macOS 27.0.1, an M5 Max and an M3 Ultra) IOReport's CPU energy rail is frozen for an unprivileged reader, so the meter has correctly declined and `proof --measure` has never printed a figure there. The kernel keeps a live counter of its own: `proc_pid_rusage(getpid(), RUSAGE_INFO_V6)`'s `ri_energy_nj`, the cumulative CPU energy it attributes to this process's threads, in nanojoules. It is public libproc API and needs no privilege. On the M5 Max it changes every ~0.5-0.7 ms under load, holds near 1-2 mJ/s idle, and keeps the energy of threads that have exited; on both Macs the probe below calls it Live. Design. `measure_marginal` (new; `measure_marginal_uj` is now its figure) runs `work` on every spare core and meters it with the first live source, in order: on macOS this process's counter, then IOReport; on Linux RAPL. For the process counter there is no bracket and no idle subtraction: the counter is read before the workers start and after every one has been joined, and the figure is its advance ÷ every call that completed, so it covers exactly the calls counted, and other processes are excluded by construction. What the figure claims, `MeterSource::domain`, says so: this process's CPU energy as the kernel attributes it to its threads — not other processes, not child processes, not GPU, ANE or DRAM — and everything this process burns in the window, so a caller must not run other work in the process while it meters. It is graded HwShunt (`MeterSource::provenance`; the owner's decision: a kernel reading of the CPU's own energy counters), and `Measurement::energy()` builds the schema reading from it. The counter is used only while it is live, by the same sustained-advance rule as IOReport and RAPL: through the same probe loop, it must advance in at least five sample intervals, in at least 80% of them, over at least 300 ms, while the probe burns 25 ms of thread CPU before each re-read. `process_energy_status` probes once per process and caches it; `meter_source` admits only `Live`, and the process rung has its own gate on the cached status besides. The bracket paths keep their own gates whatever ranks above them: `power_over` now gates on IOReport's own status and `rapl_power_over` on RAPL's, not on the overall selection, so a live process counter can never unlock a frozen IOReport rail. IOReport is not probed by the selection when the process counter is live. `proof --measure` prints the decision it acted on (`source=`, `process_energy_status=`, `ioreport_status=`, `rapl_status=`), why each source not used was not used, the figure with its source and provenance, and its domain. On this M5 Max, verbatim: --measure: hardware meter available=true · source=ProcessEnergy · process_energy_status=Live · ioreport_status=CpuRailFrozen · rapl_status=Unavailable measured: 20819 uj / proof · provenance HwShunt (measured_uj present, the schema's strongest tier) · source ProcessEnergy receipt: closed at T0:automation · 215 uj · provenance ModelBased · spec Ungrounded · verified true The receipt is unchanged: still sealed from `first`, the cascade's own ModelBased figure for the first goal. The CLI's old line "the standard's headline is now a real hardware reading" is gone: the per-goal figures stay ModelBased, and it now says so. Tests. Hardware tests check the meter against an independent oracle — the tests' own binding of `proc_pid_rusage`, their own `getpid`, a raw 464-byte buffer read at byte 336, their own loop and literals — and every branch asserts: - the FFI pin: three production reads each lie between two oracle reads, and advance across 50 ms burns; the struct is 464 bytes with `ri_energy_nj` at 336, the macOS 27.0 SDK header's numbers; - `tests/process_energy.rs` (serialized): the probe is Live exactly when the oracle sees the counter keep moving, and then it is selected first; a fixed cheap closure meters as a non-zero HwShunt figure three times within 3x; a closure that sleeps 2 ms meters at under a tenth of one that computes for 2 ms, also while four busy child processes burn CPU beside it; - `tests/process_energy_frozen.rs` drives the whole chain with the counter held (`simulate_frozen_process_energy`, a hook that can only turn the meter off): Frozen, never selected, no figure, the work never runs, one probe run; - `proof --measure` (proof-cli test): the source is the first live one in order, every printed reason is its printed status's own, the receipt equals the first goal's row and stays ModelBased, and where the test process's own counter keeps moving the CLI must have printed a non-zero HwShunt ProcessEnergy figure with its domain; - pure, on every platform: the probe composition on scripted counters (live at the twelfth 25 ms interval; constant, one-, two- and four-step counters Frozen; unreadable Unavailable), the measurement's arithmetic and read order on a scripted counter each call raises by exactly 7,000 nJ (exactly 7 uJ; it holds only if the counter is read before the first call and after the join), rounding, a falling or unreadable counter giving no figure and an unreadable one never running the work, the macOS order (IOReport not even asked when the process counter is live), and the grading and domain of every source. The IOReport tests now assert on IOReport's own gate (`bracket_admitted`, `bracket_marginal_uj`), and `ioreport_once.rs` / `ioreport_unopenable.rs` cover both probes (each runs once per process; with no Energy Model group and the counter held, every meter declines). Measured, verbatim from the test logs (debug builds, macOS 27.0.1): - M5 Max: `process liveness: status=Live source=Some(ProcessEnergy) oracle=Oracle { moved: true, reads: 35, changes: 35, advanced_nj: 1061927078 }`; cheap closure, three calls: 355, 355, 360 uJ; compute 2 ms = 2732 uJ, sleep 2 ms = 7 uJ, sleep 2 ms beside 4 busy children = 6 uJ. - M3 Ultra (the lib and process_energy test binaries and `proof`, built from this commit's code before its last doc-comment and README edits, copied to /tmp on 10.10.10.2, run once with --nocapture, deleted): `process liveness: status=Live source=Some(ProcessEnergy) oracle=Oracle { moved: true, reads: 29, changes: 29, advanced_nj: 5293659397 }`; cheap closure 671, 676, 685 uJ; compute 2 ms = 6520 uJ, sleep 2 ms = 2 uJ, beside 4 busy children = 9 uJ; `measured: 44537 uj / proof · provenance HwShunt · source ProcessEnergy`; 88/88 lib tests and 3/3 process_energy tests passed; IOReport there `CpuRailFrozen` as before. Falsified, each restored through git before the next (proof-cascade and proof-cli test suites): - reading the parent's pid: the FFI pin fails ("round 1: the production read 177161340 is outside the oracle's [897071438, 897071438]"), and so do the liveness test ("the probe says Frozen; the oracle saw the counter change at 35 of 35 reads"), both metering tests and the CLI test ("this test's own process counter changed at 24 of 24 reads, yet the CLI metered with none"); - a constant counter: the same five tests ("the production read 123456789 is outside the oracle's [...]"); - liveness ignored at the selection (the counter chosen whenever it reads): the frozen-chain test ("a held process counter was selected"), the unopenable test and the pure ordering test fail; - the probe run but its verdict discarded (always Live): the frozen-chain and unopenable tests fail ("a held counter was called Live"). `cargo test --workspace` and the proof-conformance binary pass; `cargo check --workspace --tests` and `cargo clippy --workspace --all-targets` for x86_64-unknown-linux-gnu are clean; clippy on macOS reports only the two IOReport FFI lints the README already lists. Not done: the counter's accuracy is the kernel's; nothing here checks it against an external meter. Its domain is CPU only, so GPU-bound work would meter low, and a caller that runs other threads in the process while it meters is charged for them. The process figure resolves 1 uJ per call; `Some(0)` from it means under half a microjoule, and the CLI says so. Co-Authored-By: Claude Opus 5.5 <[email protected]>af42bdb8b10e9e3c8f6d