proof-cascade: RAPL reads each package's energy-status MSR where powercap lists none #626

Merged

dcharlot merged 2 commits from proof-cascade/rapl-msr into main 2026-11-05 04:52:51 -05:00

Conversation 0 Commits 2 Files changed 4 +867 -59

2026-11-04

Transaction Science

proof-cascade: RAPL MSR domains are per die on Intel, per package on AMD ...

Linux scopes Intel's RAPL energy-status MSRs per die: its RAPL PMU treats
the package counter as package-scope only on AMD and Hygon
(rapl_pkg_pmu_is_pkg_scope(), arch/x86/events/rapl.c: "AMD/HYGON platforms
have a per-PKG package energy counter", "CLX-AP is multi-die and its RAPL
MSRs are die-scope"), and its powercap driver names a zone
package-<p>-die-<d> where the MSRs are not package-scope and a package holds
more than one die (intel_rapl_common.c). The MSR fallback grouped CPUs by
physical_package_id alone, so on a multi-die Intel package it read one die
and missed the rest: an under-count, the unsafe direction at a ceiling.

MSR fallback: on Intel family 6 a domain is (physical_package_id, die_id),
die 0 where the kernel lists no die_id; on AMD Zen and Hygon it stays the
package, whatever die_id says. Each domain is read on its lowest-numbered
CPU and is a package zone of its own, indexed in (package, die) order, so
each die is a rail of its own in the liveness rule and every die is summed.
All-or-nothing, the zero unit, the wrap and powercap preferred are as
before. (MsrPackage is now MsrDomain.)

Powercap: is_package_name also accepts package-<digits>-die-<digits>, and
nothing looser, so a multi-die host's per-die zones are its packages:
powercap lists a package (the MSRs are not read), and both die zones are
summed. Before, such a host listed no package and fell to the MSRs, as root
only.

The RAPL hardware test's oracle follows the same rules with its own code.

Tests (fake files): two Intel packages of two dies each, four domains each
read on its own die's first CPU and summed; an AMD package whose CPUs carry
two die_ids, one domain; an Intel host with no die_id files, per package; a
two-die powercap tree summing both die zones and not psys; and the name rule
(package-0-die-0 yes; package-0-die-, package-0-die, package--die-0,
package-0-die-x, package-0-core-0 no). proof-cascade and proof-cli tests pass
on Linux, proof-cascade on macOS (with its ioreport liveness grep); clippy
is clean with -D warnings on Linux (proof-cascade, proof-cli) and macOS
(proof-cascade, proof-solvers).

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

974a8ebece

• View at this point in history

2026-11-04 21:19:50 -05:00

Transaction Science

proof-cascade: RAPL reads each package's energy-status MSR where powercap lists none ...

Some kernels ship without the powercap RAPL driver (Ubuntu without
linux-modules-extra, as on some bare-metal servers), so /sys/class/powercap
lists no package while the counters are there, and the meter's RAPL source
was Unavailable on hosts that can measure. Where powercap lists no package,
the meter now reads the same counters directly: each package's
MSR_PKG_ENERGY_STATUS (0x611, Intel family 6; 0xC001029B, AMD Zen and Hygon)
through /dev/cpu/<first cpu of the package>/msr, the 32-bit count converted
at the package's own unit (bits 12:8 of the power-unit MSR), so it wraps at
2^32 counts in microjoules and resolves one count (61 uJ at 2^-14 J). A
power-unit MSR that reads zero is no counter (KVM guests read zeros). Each
MSR package is a package zone to the rest of the meter, so the liveness
rule, the busy-against-idle bracket and the wrap arithmetic are unchanged.
Powercap is still preferred; a host that lists only psys and reads no MSR
is still Absent. The same reading as jouleclaw-energy's, ported here so the
standard keeps no dependency on another.

The status text says why an MSR host reads nothing without privilege
(proof --measure: the msr module and CAP_SYS_RAWIO), and the RAPL hardware
test's oracle reads the MSRs with its own reader where powercap lists no
package, so it judges those hosts too.

On two bare-metal servers with no powercap zone, as root: a Xeon E-2278G,
RAPL Live, the all-core burn metered 117.2 J over its calls inside the
oracle's 121.8 J package-only bracket, proof --measure 64.7 mJ a proof,
HwShunt; two Xeon Silver 4215R sockets, both live, 141.3 J inside 192.9 J,
69.0 mJ a proof. As an unprivileged user the status is Unavailable on both,
agreeing with the oracle, and proof --measure gives the reason.

Tests: fake device files (a register's bytes at its offset) cover a
two-socket host read on each package's first CPU, the 32-bit wrap, AMD's
registers, a zero unit, an unknown CPU, a missing or vanished device,
powercap preferred (and a listed but unreadable package left to powercap),
and the production probe composition over MSR packages. proof-cascade and
proof-cli tests pass on Linux and macOS; clippy is clean with -D warnings
on Linux (proof-cascade, proof-cli) and macOS (proof-cascade,
proof-solvers).

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

2f170ca75f

• View at this point in history

2026-11-04 20:59:49 -05:00