paperbot · PL 论文追踪

全部论文 待读 收藏

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

面向 AMD Zen 架构的稀疏性能计数器可解释端口映射推断
ASPLOS Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 32024匹配度 2/10 · 论文属于计算机体系结构/微架构性能建模,核心是用SMT与反例引导推断AMD Zen的端口映射,虽然涉及形式化方法和约束求解,但与用户关注的PL/AI、静态分析、Agentic程序、浮点程序分析及贝叶斯程序分析等方向没有直接关联。引用 1 inbox
Fabian Ritter, Sebastian Hack
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:修改 uops.info 的端口映射推断算法,使其仅依赖稀疏性能计数器,并用 SMT 驱动的反例引导方法推断 AMD Zen 的端口映射。

乱序 x86-64 CPU 的性能模型需要指令到端口的映射,但 Intel 公开了相关映射,AMD 则缺少信息;标准精确推断方法又依赖 AMD 未提供的硬件性能计数器。本文修改 uops.info 的端口映射推断算法,使其不再依赖 Intel 计数器,而是基于形式化端口映射模型,采用 SMT 求解器驱动的反例引导算法,在稀疏性能计数器下推断映射。作者在 AMD Zen 架构上评估该方法,分析 AMD 处理器对该模型的符合程度,并指出哪些意外性能特征会阻碍准确端口映射。结果为 CPU 性能模型构建者和希望在近期 AMD CPU 上达到峰值性能的开发者提供了洞见。

问题
如何在不依赖 AMD 未提供的硬件性能计数器、仅有稀疏计数器的情况下,为 AMD Zen 等乱序 x86-64 CPU 推断精确的指令到端口映射,以支撑性能模型。
方法
修改 uops.info 的推断算法,建立形式化端口映射模型,并用 SMT 求解器驱动的反例引导算法在稀疏性能计数器约束下搜索映射。
评估
在 AMD Zen 处理器上运行推断并检验其与形式化模型的符合程度,分析导致映射不准确的异常性能特征,讨论对性能建模与软件优化的启示。
原文摘要(Abstract)

Performance models are instrumental for optimizing performance-sensitive code. When modeling the use of functional units of out-of-order x86-64 CPUs, data availability varies by the manufacturer: Instruction-to-port mappings for Intel's processors are available, whereas information for AMD's designs are lacking. The reason for this disparity is that standard techniques to infer exact port mappings require hardware performance counters that AMD does not provide. In this work, we modify the port mapping inference algorithm of the widely used uops.info project to not rely on Intel's performance counters. The modifications are based on a formal port mapping model with a counter-example-guided algorithm powered by an SMT solver. We investigate in how far AMD's processors comply with this model and where unexpected performance characteristics prevent an accurate port mapping. Our results provide valuable insights for creators of CPU performance models as well as for software developers who want to achieve peak performance on recent AMD CPUs.

链接与引用

DOI 原文 · arXiv · DBLP

BibTeX
@inproceedings{0002H24,
  title = {Explainable Port Mapping Inference with Sparse Performance Counters for AMD's Zen Architectures},
  author = {Fabian Ritter and Sebastian Hack},
  booktitle = {ASPLOS},
  year = {2024},
  doi = {10.1145/3620666.3651363}
}