Optimal Exploration of Sequentially Consistent Executions of Concurrent Programs under View Equivalence

Abstract

Modern software - from avionics controllers to smartphone apps - runs on increasingly parallel hardware. Yet concurrency bugs remain notoriously difficult to uncover. A concurrent program can execute in exponentially many different ways, depending on how its threads are interleaved. If even a single interleaving triggers a fault, it may eventually occur, potentially causing catastrophic consequences. A standard approach to verify the absence of concurrency errors in a program is Stateless Model Checking (SMC), which systematically explores the space of possible interleavings (or a representative subset thereof) by repeatedly executing the program from the initial state to termination under different scheduling scenarios. A key opportunity lies in redundancy: many interleavings yield identical program behavior and therefore need not all be explored. However, even the most refined variants of SMC (based on happens-before, observers, or reads-from equivalence) still explore multiple times interleavings where all threads read the same values. This thesis investigates view equivalence, the coarsest known equivalence relation for the Sequential Consistency (SC) memory model: two executions are equivalent if and only if every read returns the same value, irrespective of which write produced it. We introduce ViewXplore, the first sound and optimal algorithm for exploring concurrent executions under view equivalence. ViewXplore identifies all the possible values of each read and explores one relevant interleaving per combination of values, executing exactly one execution per view equivalence class. To achieve this, ViewXplore requires an algorithm to construct sequentially consistent executions. We introduce the ConstructWitness algorithm, which performs this construction in polynomial time for nearly all inputs, despite the problem being NP-complete. An implementation targeting C/Pthreads programs is built through integration with the LLVM-based Nidhugg stateless model checker. In addition, we prove that the decision problem of determining whether any SC execution violates a safety property is NP-complete. This establishes a lower complexity bound that holds independently of any equivalence strategy.