一句话:提出 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。
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
@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}
}