Model Checking the XMM Memory Model

Abstract

XMM is a newly designed multi-execution memory model that solves the out-of-thin-air exe- cutions problem, enables the most efficient compilation to all hardware platforms, and allows common compiler optimizations. Promising and Weakestmo are similar multi-execution models proposed recently. However, due to their complex semantics, they do not have an accompany- ing model checker with a proof of soundness. XMM is significantly less complex, which paved the way for implementing an XMM model checker. In our work, we present our design of a model checker algorithm for the XMM memory model called GenMC-XMM. Due to practical limitations of algorithmic time complexity, we could not design a complete model checker. However, we provide a proof of soundness. In other words, we cannot guarantee that our tool will find all possible executions of a program, but we can guarantee that the ones it finds are all XMM consistent. To our knowledge, GenMC-XMM is the first multi-execution model checker proven to be sound. We evaluated our tool against the state-of-the-art model checking tools for RC11, IMM, and Weakestmo2. We determined that GenMC-XMM explores the same or more executions than every other tool in all our tests. GenMC-XMM is only marginally slower than the other tools in real-world lock-free data- structure benchmarks. In synthetic tests designed to have thousands of data races, GenMC- XMM does not scale as well as the other tools as the number of races increases. GenMC-XMM is the next milestone in the automatic verification of multi-execution memory models. Based on our work on GenMC-XMM, other researchers may improve its performance and design a sound and complete algorithm.