Wed 23 Oct 2024 14:00 - 14:20 at IBR West - Performance Analysis and Optimisation 1 Chair(s): Manu Sridharan

The correctness of complex software depends on both the correctness of 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, and different atomics mappings, although correct in isolation, may induce bugs when composed. Indeed, mixing binaries generated by today’s compilers can lead to erroneous binaries.

We present mix testing: a new technique designed to find compiler bugs when the components 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 tool, atomic-mixer, which we have used: (a) to reproduce existing non-mixing bugs 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.

Wed 23 Oct

Displayed time zone: Pacific Time (US & Canada) change

13:40 - 15:20
Performance Analysis and Optimisation 1OOPSLA 2024 at IBR West
Chair(s): Manu Sridharan University of California at Riverside
13:40
20m
Talk
Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning
OOPSLA 2024
Gabriel Ryan Columbia University, Burcu Cetin Columbia University, Christian Yongwhan Lim Columbia University, Suman Jana Columbia University
DOI
14:00
20m
Talk
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations
OOPSLA 2024
Luke Geeson University College London, James Brotherston , Wilco Dijkstra Arm Ltd, Alastair F. Donaldson Imperial College London, Lee Smith Arm, Tyler Sorensen University of California at Santa Cruz, John Wickerson Imperial College London
DOI Media Attached
14:20
20m
Talk
Practical Verification Of Smart Contracts Using Memory Splitting
OOPSLA 2024
Shelly Grossman Tel Aviv University, Alexander Bakst Certora, Sameer Arora Certora Inc., John Toman Certora, inc., Chandrakana Nandi Certora, Mooly Sagiv Tel Aviv University
DOI
14:40
20m
Talk
Fast and Optimal Extraction for Sparse Equality GraphsOOPSLA 2024 Distinguished Paper Award
OOPSLA 2024
Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Chun Kit Lam Hong Kong University of Science and Technology, Lionel Parreaux HKUST (The Hong Kong University of Science and Technology)
DOI
15:00
20m
Talk
HybridSA: GPU Acceleration of Multi-Pattern Regex Matching using Bit Parallelism
OOPSLA 2024
Alexis Le Glaunec Rice University, Lingkun Kong Rice University, Konstantinos Mamouras Rice University
DOI