Automated concurrency bug finding using partial-orders

Thesis

Concurrent systems are ubiquitous, ranging from multi-core processors to large-scale distributed systems. Yet, the verification of concurrent systems remains a daunting task, and technological advances such as weak memory architectures greatly compound this problem. Such challenges have renewed interest in symbolic encodings of partial-order semantics of concurrency using propositional logic or decidable fragments of first-order logic. The impetus behind these partial-order encodings is the efficiency of evermore highly optimized decision procedures, such as Boolean satisfiability (SAT) and Satisfiability Modulo Theory (SMT) solvers.

While methods to effectively use SAT/SMT solvers for automatically finding bugs in sequential software through symbolic techniques, such as bounded model checking or symbolic execution, are well known, this thesis gives theoretical and experimental results that highlight a new set of challenges faced by partial-order encoding techniques. Furthermore, it shows how different solutions to these problems emerge if partial-order encodings are restructured into three separate theory-specific parts. This separation opens up a fresh and fruitful algorithmic perspective on partial-order encodings, including a new partial-order encoding that can drastically reduce the run-time of the analysis prior to calling the SAT/SMT solver, and new insights into the exponential worst-case time complexity of partial-order encodings during SAT/SMT solving. These results are significant as they propose a paradigm shift in how to harness the computational power of SAT/SMT solvers for partial-order encodings.

Authors: Horn, A

• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford