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

dcharlot commented 2026-11-04 21:02:21 -05:00

Owner

Copy link

Some kernels ship without the powercap RAPL driver (Ubuntu without linux-modules-extra, as on some rented bare-metal servers). On those hosts /sys/class/powercap lists no package even though the counters are there. This ports the MSR fallback from #618 (jouleclaw-energy) into this meter, with no dependency added: the standards do not depend on one another.

Where powercap lists no package, each package's MSR_PKG_ENERGY_STATUS is read on that package's first CPU through /dev/cpu/<n>/msr:

• Registers: 0x606 and 0x611 on Intel family 6; 0xC0010299 and 0xC001029B on AMD Zen and Hygon.
• Count: the 32-bit count is converted at the package's own unit (bits 12:8 of the power-unit MSR) and wraps at 2^32 counts.
• Zero unit: a unit that reads zero means no counter.
• Unchanged: powercap is still preferred, and the liveness rule is the same: every package readable and live, or no figure.

proof-cascade specifics

• Package zones: each MSR package becomes one more package zone, so the liveness rule, the busy-vs-idle bracket and the wrap maths are unchanged.
• Powercap preferred: decided by the zone's name, so a listed but root-only package stays with powercap. A host that lists only psys and has no readable MSR still reads as Absent.
• proof --measure: names the msr module and CAP_SYS_RAWIO in its Unavailable reason and mentions the MSRs in its Absent reason. The README line is updated.
• tests/rapl_hardware.rs: gains its own MSR oracle where powercap lists no package.
• Unit tests on fake MSR files: two-socket host, 32-bit wrap (1,953 µJ), AMD registers, zero unit, unknown CPU, missing or vanished device, powercap preferred, and the production probe (Live, and Frozen when one package holds).

Verified

• Linux x86_64: cargo test -p proof-cascade and -p proof-cli pass; cargo check --workspace --all-targets is clean; clippy on proof-cascade and proof-cli is clean.
• macOS (CI steps): cargo test -p proof-cascade passes and the ioreport liveness: grep matches. Clippy on proof-cascade and proof-solvers is clean.
• Two bare-metal servers with no powercap zone, as root:
  • Xeon E-2278G: Live; an all-core burn read 117.2 J, inside the oracle's 121.8 J package-only bracket; proof --measure gives 64,676 µJ per proof, HwShunt.
  • Two Xeon Silver 4215R sockets: both Live; 141.3 J, inside 192.9 J.
• Same servers, unprivileged: Unavailable, agreeing with the oracle, and --measure declines with the new reason.

Second commit: die scope

Linux scopes Intel's RAPL MSRs per die and AMD's and Hygon's per package. arch/x86/events/rapl.c says "AMD/HYGON platforms have a per-PKG package energy counter" and "CLX-AP is multi-die and its RAPL MSRs are die-scope". The powercap driver names a multi-die Intel package's zones package-<p>-die-<d>, one top-level zone per die.

• MSR fallback: reading each package on its first CPU counted one die of a multi-die Intel package, an under-count. A domain is now (physical_package_id, die_id) on Intel and the package on AMD and Hygon. Each domain is read on its own first CPU and they are summed. Single-die parts are unchanged.
• Powercap names: the rule now also accepts package-<n>-die-<m>, so a multi-die host's die zones count as packages. It accepts nothing looser.
• Hardware test oracle: scopes MSR domains the same way, using its own code.

New unit tests: a two-die Intel package is two domains, summed; an AMD package whose CPUs list several die_ids is one domain; a two-die powercap tree sums both die zones; and the name rule's accepted names and near misses. Tests and clippy pass as before on Linux and macOS.

🤖 Generated with Claude Code

Some kernels ship without the powercap RAPL driver (Ubuntu without `linux-modules-extra`, as on some rented bare-metal servers). On those hosts `/sys/class/powercap` lists no package even though the counters are there. This ports the MSR fallback from #618 (`jouleclaw-energy`) into this meter, with no dependency added: the standards do not depend on one another. Where powercap lists no package, each package's `MSR_PKG_ENERGY_STATUS` is read on that package's first CPU through `/dev/cpu/<n>/msr`: - **Registers:** 0x606 and 0x611 on Intel family 6; 0xC0010299 and 0xC001029B on AMD Zen and Hygon. - **Count:** the 32-bit count is converted at the package's own unit (bits 12:8 of the power-unit MSR) and wraps at 2^32 counts. - **Zero unit:** a unit that reads zero means no counter. - **Unchanged:** powercap is still preferred, and the liveness rule is the same: every package readable and live, or no figure. ## proof-cascade specifics - **Package zones:** each MSR package becomes one more package zone, so the liveness rule, the busy-vs-idle bracket and the wrap maths are unchanged. - **Powercap preferred:** decided by the zone's name, so a listed but root-only package stays with powercap. A host that lists only `psys` and has no readable MSR still reads as Absent. - **`proof --measure`:** names the `msr` module and `CAP_SYS_RAWIO` in its Unavailable reason and mentions the MSRs in its Absent reason. The README line is updated. - **`tests/rapl_hardware.rs`:** gains its own MSR oracle where powercap lists no package. - **Unit tests on fake MSR files:** two-socket host, 32-bit wrap (1,953 µJ), AMD registers, zero unit, unknown CPU, missing or vanished device, powercap preferred, and the production probe (Live, and Frozen when one package holds). ## Verified - **Linux x86_64:** `cargo test -p proof-cascade` and `-p proof-cli` pass; `cargo check --workspace --all-targets` is clean; clippy on `proof-cascade` and `proof-cli` is clean. - **macOS (CI steps):** `cargo test -p proof-cascade` passes and the `ioreport liveness:` grep matches. Clippy on `proof-cascade` and `proof-solvers` is clean. - **Two bare-metal servers with no powercap zone, as root:** - Xeon E-2278G: Live; an all-core burn read 117.2 J, inside the oracle's 121.8 J package-only bracket; `proof --measure` gives 64,676 µJ per proof, HwShunt. - Two Xeon Silver 4215R sockets: both Live; 141.3 J, inside 192.9 J. - **Same servers, unprivileged:** Unavailable, agreeing with the oracle, and `--measure` declines with the new reason. ## Second commit: die scope Linux scopes Intel's RAPL MSRs per die and AMD's and Hygon's per package. `arch/x86/events/rapl.c` says "AMD/HYGON platforms have a per-PKG package energy counter" and "CLX-AP is multi-die and its RAPL MSRs are die-scope". The powercap driver names a multi-die Intel package's zones `package-<p>-die-<d>`, one top-level zone per die. - **MSR fallback:** reading each package on its first CPU counted one die of a multi-die Intel package, an under-count. A domain is now (`physical_package_id`, `die_id`) on Intel and the package on AMD and Hygon. Each domain is read on its own first CPU and they are summed. Single-die parts are unchanged. - **Powercap names:** the rule now also accepts `package-<n>-die-<m>`, so a multi-die host's die zones count as packages. It accepts nothing looser. - **Hardware test oracle:** scopes MSR domains the same way, using its own code. New unit tests: a two-die Intel package is two domains, summed; an AMD package whose CPUs list several `die_id`s is one domain; a two-die powercap tree sums both die zones; and the name rule's accepted names and near misses. Tests and clippy pass as before on Linux and macOS. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

dcharlot added 1 commit 2026-11-04 21:02:22 -05:00

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

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

dcharlot added 1 commit 2026-11-04 21:20:32 -05:00

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

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

dcharlot merged commit 6bc1171904 into main 2026-11-05 04:52:50 -05:00

dcharlot referenced this pull request from a commit 2026-11-05 04:52:51 -05:00

Merge pull request 'proof-cascade: RAPL reads each package's energy-status MSR where powercap lists none' (#626) from proof-cascade/rapl-msr into main

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!626

No description provided.