paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations

Mix Testing:指定并测试 C/C++ 原子操作实现的 ABI 兼容性
OOPSLA 8(OOPSLA2)2024匹配度 2/10 · 论文研究 C/C++ 原子操作映射的 ABI 兼容性测试,属于并发与编译测试方向,与用户画像中 PL 与 AI/LLM 交叉、浮点程序分析、贝叶斯程序分析等核心课题无直接关联;虽具备形式化规范与工业合作,但研究问题不匹配。引用 3 inbox
Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, John Wickerson
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话:提出 mix testing 与 atomic-mixer,用于发现不同编译器原子操作映射混合链接时产生的 ABI 兼容性 bug。

复杂软件正确性依赖源码与生成二进制的正确性。编译器不仅要保持单文件语义,还要保证生成的二进制能与其他二进制组合为可执行文件;ABI 负责这种组合兼容性,但并发程序缺乏官方 ABI,不同原子操作映射虽各自正确,混合后仍可能出错。本文提出 mix testing:将 C/C++ 测试指令分别针对多个兼容架构编译再混合,以发现一类称为 mixing bug 的编译器缺陷,并实现 atomic-mixer。评估中,作者复现了一个现有非 mixing bug,表明至少达到当前并发测试工具能力;发现 LLVM/GCC 中四个未知 mixing bug,以及 JVM 拟议映射中的一个潜在 mixing bug;还与 Arm 工程师首次制定 Armv8 atomics ABI,并用 atomic-mixer 验证 LLVM 和 GCC。

问题
并发程序的 C/C++ 原子操作缺乏官方 ABI,不同编译器的 atomics 映射虽在孤立情况下正确,但混合编译后的二进制可能产生错误,因此需要发现和避免此类 ABI 兼容性问题。
方法
提出 mix testing,将测试中 C/C++ 原子指令分别编译到多个兼容架构后再混合链接,以触发并检测 mixing bug;实现工具 atomic-mixer。
评估
复现现有非 mixing 并发测试 bug,在 LLVM/GCC 发现四个未知 mixing bug 和 JVM 映射中一个潜在 bug,并用于验证 Armv8 atomics ABI 下 LLVM/GCC 的正确性。
原文摘要(Abstract)

The correctness of complex software depends on the correctness of both the source code and the compilers that generate corresponding binary code. Compilers must do more than preserve the semantics of a single source file: they must ensure that generated binaries can be composed with other binaries to form a final executable. The compatibility of composition is ensured using an Application Binary Interface (ABI), which specifies details of calling conventions, exception handling, and so on. Unfortunately, there are no official ABIs for concurrent programs, so different atomics mappings, although correct in isolation, may induce bugs when composed. Indeed, today, mixing binaries generated by different compilers can lead to an erroneous resulting binary. We present mix testing : a new technique designed to find compiler bugs when the instructions of a C/C++ test are separately compiled for multiple compatible architectures and then mixed together. We define a class of compiler bugs, coined mixing bugs , that arise when parts of a program are compiled separately using different mappings from C/C++ atomic operations to assembly sequences. To demonstrate the generality of mix testing, we have designed and implemented a tool, atomic-mixer , which we have used: (a) to reproduce one existing non-mixing bug that state-of-the-art concurrency testing tools are limited to being able to find (showing that atomic-mixer at least meets the capabilities of these tools), and (b) to find four previously-unknown mixing bugs in LLVM and GCC, and one prospective mixing bug in mappings proposed for the Java Virtual Machine. Lastly, we have worked with engineers at Arm to specify, for the first time, an atomics ABI for Armv8, and have used atomic-mixer to validate the LLVM and GCC compilers against it.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{abs-2409-01161,
  title = {Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations},
  author = {Luke Geeson and James Brotherston and Wilco Dijkstra and Alastair F. Donaldson and Lee Smith and Tyler Sorensen and John Wickerson},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {OOPSLA2},
  year = {2024},
  doi = {10.1145/3689727}
}