Explainable Port Mapping Inference with Sparse Performance Counters for AMD's Zen Architectures

To predict how fast a CPU will run code, tools need a "port mapping" — a chart of how each instruction breaks into tiny micro-operations and which execution ports can run them — but the standard way to reverse-engineer it needs special per-port counters that Intel chips have and AMD's Zen chips do not, so accurate models for AMD were missing; this paper (Saarland University — Fabian Ritter, Sebastian Hack) infers the port mapping using only a total micro-op count and throughput measurements, driven by an SMT solver that keeps proposing distinguishing experiments until one mapping survives, producing the first explainable port mapping for AMD's Zen+.

The argument in one glance

Problem

Predicting CPU speed needs a port mapping, but AMD hides the counters to find it

To optimize code for peak speed, compilers and performance tools need a model of how a processor executes instructions. A key part of that model is the port mapping. Modern out-of-order CPUs do not run instructions whole; they decode each instruction into one or more tiny operations called micro-ops, and a scheduler sends each micro-op to one of the processor's execution ports (an integer unit, a vector unit, a memory port, and so on), running many in parallel. The port mapping is the chart that says, for every instruction, which micro-ops it becomes and which ports each micro-op can use. Compiler backends and instruction-throughput predictors rely on this chart to estimate how fast a block of code will run. Manufacturers rarely publish port mappings, so researchers infer them by running tiny microbenchmarks and measuring what the chip does. The catch is that the standard, accurate technique — used by the well-known uops.info project for Intel chips — depends on special hardware performance counters that report how many micro-ops each individual port executed. Intel exposes these per-port counters; AMD's Zen processors do not. So the one measurement the standard method leans on is simply unavailable on AMD, which is why accurate, trustworthy port mappings existed for Intel but not for AMD's widely-used Zen designs.
What people did

Reuse the counter-based method, or fall back to counter-free heuristics

There are two roads. One is the uops.info approach: flood specific ports with "blocking" instructions and use per-port counters to see how many of an instruction's micro-ops land on those ports, building an exact, witnessed mapping. The other is counter-free methods that need only timing: PMEvo uses an evolutionary algorithm to fit a mapping to a set of benchmarks, and Palmed infers a resource model that predicts throughput well.
Why it fell short

The counter method fails on AMD, and the counter-free ones are untrustworthy or ill-fitting

Neither road reaches an accurate, usable AMD port mapping. The uops.info method cannot run at all on Zen, because it fundamentally requires the per-port micro-op counters that AMD does not provide — remove those counters and its core step, seeing how many micro-ops executed on a chosen set of ports, has no measurement to read. The counter-free alternatives avoid that dependency but pay for it in ways that matter for real tools. PMEvo's evolutionary search produces mappings that rarely coincide with the actual microarchitecture and, crucially, cannot offer any explanatory microbenchmark to justify why an entry is what it is — so there is no way to build confidence in the result or debug it. Palmed infers a different kind of resource model that predicts throughput well but does not map directly onto the microarchitecture's ports, so it does not fit into existing compilers and throughput predictors that expect a port mapping. What was missing was a method that produces a real, port-level mapping with explanatory microbenchmarks — the trustworthy, tool-compatible output of the counter-based approach — but without needing the per-port counters that AMD withholds.
This paper's idea

Infer the mapping from total micro-op count and throughput, guided by an SMT solver

The paper presents a port-mapping inference algorithm that needs no per-port counters, so it works on architectures uops.info cannot handle. Its key insight is that the parts of the uops.info algorithm that required per-port counts can be recovered without them, as long as you assume the processor obeys a formal port mapping model — a precise mathematical description relating a port mapping to the throughput of instruction sequences. Under that assumption, two things suffice: ordinary throughput (timing) measurements, and a single, common performance counter that reports the total number of micro-ops a microbenchmark executed (not per port). The engine that turns these sparse measurements into a mapping is a counter-example-guided loop powered by a satisfiability-modulo-theories (SMT) solver. At each step, the solver proposes a candidate port mapping consistent with every experiment run so far; then it is asked to find a second, different mapping that is also consistent, together with an experiment (a mix of instructions) whose throughput the two mappings predict differently. That distinguishing experiment is run on the real chip, its measured throughput is added to the constraints, and it rules out at least one candidate. The loop repeats until no two distinct mappings can fit the data, and because every experiment is a concrete microbenchmark, each entry of the final mapping is witnessed and explainable. Applied to AMD's Zen+, the method produces the first explainable port mapping for over 1,000 instruction schemes that were out of reach before, beats the state of the art on throughput-prediction accuracy for those instructions, and uncovers numerous previously undocumented or misdocumented details of the microarchitecture.

Why this problem is worth solving

Accurate port mappings underlie the tools that make code fast, so their absence for AMD leaves a large, widely-used platform poorly modeled.

A port mapping is not an academic curiosity; it is a working component inside the software people use to optimize performance. Compiler backends consult a model of how instructions use the execution ports to decide how to schedule and select instructions, and instruction-throughput predictors use the same information to estimate how many cycles a basic block will take without running it. When that model is accurate, these tools make good decisions and give reliable estimates; when it is wrong or missing, they mispredict and misoptimize. For Intel processors, accurate port mappings from projects like uops.info have made such tools trustworthy. For AMD’s Zen family — which powers a huge share of servers, desktops, and cloud instances — no comparable, accurate, explainable mapping existed, precisely because the standard inference method could not run without the counters AMD omits. That gap means a major, popular architecture is modeled worse than its competitor, so code tuned with these tools is tuned less well on AMD. Filling the gap improves the models that a lot of real optimization depends on.

The difficulty is that the missing counter is exactly the measurement the standard method is built around, so you must reconstruct that information indirectly.

The elegance of the counter-based method is that it reads the answer almost directly: flood a chosen set of ports with blocking instructions, then a per-port counter tells you exactly how many of the instruction-under-test’s micro-ops were forced onto those ports. Take that counter away and you lose the direct readout — you can still measure how long a microbenchmark takes and how many micro-ops it executed in total, but not where those micro-ops went. The problem is to recover the per-port information from these coarser, aggregate signals. The leverage is the formal model: if you assume the processor behaves according to a precise port mapping model, then the throughput of a given instruction mix is a mathematical function of the (unknown) mapping, so different candidate mappings predict different throughputs for cleverly chosen instruction mixes. That turns inference into a search: find the mapping consistent with all the throughputs you have measured, and keep measuring mixes that separate the remaining candidates until only one survives. The catch is that this search must be driven intelligently — you cannot enumerate all mappings, and you want each measurement to actually distinguish candidates — which is where a solver-guided, counter-example approach earns its keep, while still producing the concrete witnessing microbenchmarks that make the result trustworthy.

What people did before, and where it broke

Use uops.info with per-port counters. Flood ports with blocking instructions and count per-port micro-ops to build a witnessed mapping. Where it broke. AMD’s Zen processors do not provide per-port micro-op counters, so the method’s core measurement is unavailable and it cannot run.
Fit a mapping with an evolutionary algorithm (PMEvo). Use only timing to evolve a mapping that matches a benchmark set. Where it broke. The results rarely match the real microarchitecture and come with no explanatory microbenchmarks, so there is no way to justify or trust individual entries.
Infer a resource model (Palmed). Learn a conjunctive resource model that predicts throughput well. Where it broke. It does not map onto the microarchitecture’s actual ports, so it does not fit compilers and throughput predictors that expect a port mapping.
Just read AMD’s documentation. Rely on published instruction tables and manuals. Where it broke. The paper finds numerous undocumented and even misdocumented cases on Zen+, so the documentation is incomplete and sometimes wrong.
The gap. No method produced an accurate, port-level, explainable mapping for AMD without the per-port counters the standard technique requires.

How the inference works

Recovering a port mapping from sparse measurements with a solver

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Recover a hidden hardware model from the coarse signals you are allowed to measure. The whole method is an act of inference: the chip will not tell you where its micro-ops go, so you deduce the port mapping from aggregate throughput and a total micro-op count, reconstructing what the missing per-port counter would have revealed. Working out a processor’s hidden internal behavior from the limited measurements it does expose, rather than from privileged counters, is the same undertaking the work on using hardware event counters to refute and refine microarchitectural assumptions (CounterPoint) covered elsewhere on this site pursues, turning indirect measurements into a model of the microarchitecture. This paper does it for the port mapping specifically, and precisely for the case where the ideal counter is absent.

Search for the model with a solver that keeps generating distinguishing experiments. The engine is a counter-example-guided loop: propose a candidate mapping, have the solver find another mapping that also fits plus an experiment that separates them, run it, and refine. Synthesizing a correct model by repeatedly asking a solver for a candidate and a counter-example that refutes wrong candidates is the same principle the work on code synthesis for memory translation (VeloSiRaptor) covered elsewhere on this site is built on, letting an SMT solver drive the search toward the unique consistent answer. Here the counter-examples are microbenchmarks to run on real silicon, and each one prunes the space of possible port mappings.

Make the result explainable, with a witness for every entry. A port mapping is only useful to engineers if they can trust and inspect it, so the method keeps, for each inferred entry, the concrete microbenchmark that justifies it — unlike a black-box fit whose numbers have no tangible justification. Producing not just an answer but human-inspectable evidence for why the answer holds is the same idea the work on agile and explainable exploration of efficient hardware-software designs (Explainable DSE) covered elsewhere on this site develops, valuing explanations alongside results. The paper’s explanatory microbenchmarks are what separate its mapping from PMEvo’s opaque evolutionary output and let it be trusted in real tools.

Following the inference loop

Pinning down the true port mapping, one distinguishing experiment at a time

A trace, drawn from the paper, of the counter-example-guided inference loop.

Step 1 of 5

Start from the formal model and no experiments

The method assumes the chip obeys a port mapping model in which any port mapping determines the throughput of a dependency-free instruction mix. It begins with an empty set of experiments and seeks the one true mapping.

The model turns "which mapping is real?" into a constraint-solving problem.

Why it works

The formal model replaces the missing per-port counter. uops.info reads per-port counts AMD does not provide → but if the chip obeys the port mapping model, throughput plus a total micro-op count determine the mapping → so the per-port information is recovered indirectly.
Different mappings predict different throughputs, so experiments discriminate. Two candidate mappings can look identical on the data so far → but the model makes them predict different throughput for some instruction mix → so running that mix reveals which candidate is real.
The counter-example loop converges without enumerating mappings. There are far too many possible mappings to try → but each round has the solver find a distinguishing experiment that rejects at least one candidate → so the search narrows efficiently to the unique answer.
Witnessing microbenchmarks make the result explainable. A black-box fit gives numbers with no justification → but every entry here is backed by a concrete microbenchmark that forced it → so engineers can trust and inspect the mapping, and it fits real tools.
Guaranteed termination bounds the process. An open-ended search might never stop → but each iteration rejects at least one candidate and the mappings are finite → so the loop is guaranteed to halt with a definite mapping.

What it costs (trade-offs and scope)

It assumes the processor follows the port mapping model. Where Zen+ deviates — throughput bottlenecks in parts of the processor beyond the ports, complex micro-coded or non-pipelined instructions — the assumption breaks and an accurate mapping cannot be inferred; the paper documents such cases rather than hiding them.
Coverage is broad but not total. The method produces an explainable mapping for over 1,000 instruction schemes on Zen+, a large share, but some instructions remain out of reach, and misdocumented or missing performance counters and irregular behavior hinder others.
Inference is computationally heavy. The solver-driven loop with real microbenchmarks takes on the order of 20 to 28 hours to characterize the architecture, since it repeatedly runs experiments and solves constraint systems.
It depends on measurement quality. Throughput measurements carry noise and error, handled with a tolerance in the constraints, but noisy or erroneous measurements remain a hazard; the method also needs suitable “blocking” instructions to exist for the relevant port sets.
It models the ports, one piece of performance. A port mapping captures how instructions use the execution ports; other performance effects (front-end decoding limits, the memory system) are outside it, and the results are a case study on Zen+ specifically rather than a universal guarantee.

The evaluation

Inferring a port mapping for AMD's Zen+

Property	uops.info (counter-based)	PMEvo / Palmed (counter-free)	This work
Runs on AMD Zen (no per-port counters)
Maps onto real ports
Explainable (witnessed entries)
Fits compilers and predictors
Result on Zen+

A comparison of port-mapping inference approaches for AMD's Zen+. By assuming a formal port mapping model and driving a counter-example-guided SMT search with only throughput and a total micro-op counter, the paper produces a real, explainable, tool-compatible port mapping without the per-port counters AMD omits — the most comprehensive explainable mapping for Zen+ to date, outperforming the state of the art on throughput-prediction accuracy for the supported instructions.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This explainer is based on the paper’s full text (the authors’ arXiv copy of the ASPLOS 2024 paper). The method described is the paper’s: it modifies the uops.info port-mapping inference algorithm to not rely on Intel’s per-port hardware performance counters, so it can target AMD’s Zen architectures. It builds on a formal port mapping model (a tripartite graph relating instruction schemes to micro-ops to execution ports, with the model determining the throughput of dependency-free instruction sequences) and uses only throughput measurements plus a single counter for the total number of executed micro-ops. The core is a counter-example-guided algorithm powered by an SMT solver (the paper uses z3): it repeatedly finds a candidate mapping consistent with the experiments so far, seeks a second consistent-but-different mapping and a distinguishing experiment, runs that experiment on the real chip, and adds the measurement, terminating when only one mapping remains; every entry is witnessed by a concrete microbenchmark. In a case study on AMD’s Zen+, the paper reports inferring the first explainable port mapping for over 1,000 instruction schemes previously out of scope, outperforming the state of the art on throughput-prediction accuracy for the supported instructions, and documenting numerous previously undocumented or misdocumented aspects of Zen+ (including irregular performance characteristics, misdocumented counters, and complex micro-coded or non-pipelined instructions), with total inference taking roughly 20 to 28 hours. Exact model definitions, the SMT encoding, accuracy metrics, and full results should be read from the paper.

Background

Why understanding a processor from the outside keeps mattering

It helps to see this work within a long effort to understand processors that their makers only partially document. A modern CPU is a bundle of clever, interacting mechanisms — out-of-order execution, multiple ports, micro-op decomposition — whose exact behavior determines how fast real code runs, yet manufacturers publish only fragments, and sometimes those fragments are wrong. The people who must reason about performance — compiler writers, performance engineers, authors of throughput predictors — are therefore perpetually reverse-engineering the chip from the outside, running crafted microbenchmarks and inferring models from what they can measure. The recurring obstacle is that the most convenient measurements are not always available: a vendor may expose the perfect counter on one product line and omit it on another, as Intel does with per-port micro-op counters and AMD does not. Progress then comes from reformulating the inference so it needs only the measurements that are universally available, and from insisting the results be explainable, because a model you cannot justify is a model you cannot trust or fix. This mirrors the broader craft of extracting reliable understanding from a black box using formal reasoning and careful experiments. The wider effort to search for and justify better implementations of computation using formal, solver-driven exploration is the same terrain the work on a super-optimization explorer for high-level synthesis (Seer) covered elsewhere on this site occupies, letting rigorous search and cost reasoning find and validate results. This paper contributes a solver-guided, explainable way to recover a processor’s port mapping even when the ideal counter is missing, closing a real gap between how well Intel and AMD chips could be modeled.

If you remember only three things

1. A port mapping — the chart of how each instruction decomposes into micro-ops and which execution ports can run them — is a core input to compiler backends and instruction-throughput predictors. The standard, accurate way to infer it (used by uops.info for Intel) floods ports with blocking instructions and reads per-port micro-op counters. AMD's Zen processors do not provide those counters, so the method cannot run, and counter-free alternatives either fail to match the real microarchitecture (PMEvo) or do not map onto the actual ports (Palmed), leaving AMD without an accurate, explainable, tool-compatible port mapping.
2. The paper infers the mapping using only throughput measurements and a single total-micro-op counter, by assuming the processor obeys a formal port mapping model in which the mapping determines the throughput of instruction mixes. A counter-example-guided loop driven by an SMT solver repeatedly proposes a candidate mapping consistent with all experiments so far, finds a second consistent-but-different mapping plus a distinguishing instruction mix, runs that microbenchmark on the real chip, and adds the measurement — which rejects at least one candidate — until only one mapping survives. Because every constraint is a concrete microbenchmark, each entry is witnessed and explainable, unlike a black-box evolutionary fit.
3. Applied to AMD's Zen+, the method infers the first explainable port mapping for over 1,000 instruction schemes previously out of scope, beats the state of the art on throughput-prediction accuracy for those instructions, and documents numerous previously undocumented or misdocumented aspects of the microarchitecture. The trade-offs: it assumes the chip follows the port mapping model (failing where it does not, e.g. micro-coded or non-pipelined instructions), does not cover every instruction, takes on the order of 20 to 28 hours, depends on measurement quality, and models the ports rather than every performance effect.

Check yourself

Check your understanding

1. What is a port mapping, and why does it matter for optimizing code?
2. Why can the standard uops.info inference method not be used on AMD's Zen processors?
3. How does the paper's counter-example-guided algorithm infer the mapping without per-port counters?
4. Why does the paper emphasize that its inferred mapping is "explainable," and how does that differ from PMEvo?

Sources

The paper is “Explainable Port Mapping Inference with Sparse Performance Counters for AMD’s Zen Architectures” by Fabian Ritter and Sebastian Hack (Saarland University, Saarland Informatics Campus), published at ASPLOS 2024, DOI 10.1145/3620666.3651363. An author copy is available at arXiv:2403.16063.

This explainer is written from the paper’s full text (the authors’ arXiv copy). Port mappings — how instructions decompose into micro-ops executed on a processor’s ports — are essential to compiler cost models and throughput predictors, but the standard inference method (uops.info) relies on Intel’s per-port hardware performance counters, which AMD’s Zen processors do not provide. The paper modifies the uops.info algorithm to not require per-port counters: it builds on a formal port mapping model and uses only throughput measurements and a single counter for the total number of executed micro-ops. Its core is a counter-example-guided algorithm powered by an SMT solver that finds a candidate mapping consistent with the experiments so far, seeks a distinguishing experiment separating it from another consistent mapping, runs that experiment, and refines until one mapping remains — yielding explanatory microbenchmarks for each entry. In a case study on AMD’s Zen+, the paper reports inferring the first explainable port mapping for over 1,000 instruction schemes out of scope for prior work, outperforming the state of the art on throughput-prediction accuracy for the supported instructions, and documenting numerous previously undocumented or misdocumented aspects of Zen+. Numbers are the paper’s own; exact models, encodings, and full results should be confirmed in the paper.