Fast and Effective Approaches for Verifying and Debugging Concurrent Programs

Concurrent programs are ubiquitous, from the high-end servers to personal machines, due to the fact of multi-core hardware. Unfortunately, it is difficult to write correct concurrent programs. Stateless Model Checking (SMT) and Deterministic Replay are powerful techniques for systematic testing and reproducing concurrent failures. However, it is challenging to develop efficient and practical SMT and bug reproduction systems due to the exponentially large thread interleaving space which can be exacerbated when it comes to relaxed memory models. In this work, I introduce my research efforts to address the challenges in developing fast and effective SMT and deterministic replay techniques. I present a new model checking technique based on maximal causality reduction for verifying concurrent programs under different memory models. I also optimize the model checker by using static dependency analysis to reduce the constraints size and introducing a new equivalence for checking the seed interleavings, which I call switch equivalence to further reduce the redundant exploration. To debug heisenbugs more efficiently, I presents a new concurrency failure reproduction technique, H3, that enables reproducing concurrency bugs in production runs on commercial off-the-shelf hardware for the first time. H3 integrates the hardware control flow tracing capability provided in recent Intel processors, Processor Tracing (PT), with symbolic constraint analysis. Compared to a state-of-the-art solution, CLAP, this integration allows H3 to reproduce failures with much lower runtime overhead and much more compact control-flow trace. Moreover, it allows us to develop a highly effective core-based constraint reduction technique that reduces the complexity of the generated symbolic constraints from exponential in the trace size to exponential in the number of cores