Doctoral thesis defence, Sarbojit Das: "Practical Adaptations and Improvements of Stateless Model Checking"

Opponent: Prof. Keijo Heljanko, Helsinki University

Grading Committee:

• Prof. Gerardo Schneider, Chalmers
• Docent Ahmed Rezine, Linköping University
• Prof. Cristina Seceleanu, Mälardalen University
• Deputy: Docent Johannes Borgström, Uppsala University

Chairman: Prof. Stefanos Kaxiras,

Supervisors: Mohamed Faouzi Atig, Bengt Jonsson

Abstract [en]Concurrent softwares are running on every computer. They are essential for harnessing the full potential of modern multicore processors. Finding bugs in concurrent software is challenging and time-consuming because of the scheduling non-determinism. Stateless model checking is one of the most effective and practical techniques in finding all concurrency bugs in concurrent software for a fixed input. However, the exponential number of thread interleavings resulting the exponential number of executions makes the SMC challenging. Dynamic Partial Order Reduction (DPOR) is an effective SMC technique for mitigating this problem by avoiding equivalent execution exploration. This thesis presents three contributions to the world of DPOR algorithms.

The first contribution is the Event-DPOR algorithm for event-driven concurrency. Event-DPOR is based on the Optimal-DPOR (ODPOR) algorithm, the first DPOR algoritm that is optimal (explores only non-equivalent executions). Event-driven concurrency can be found in distributed systems, high-performance servers, smartphone applications, and many other domains. Event-DPOR significantly reduces the number of explored executions over other state-of-the-art algorithms, and guarantees optimality for programs with non-branching messages, i.e., the set of shared variable accesses does not change in messages across executions. We also proved the NP-completeness of event-driven consistency check, a key component in preventing redundant exploration. We addressed it with a series of inexpensive tests sufficient for the programs we tried. Our implementation in Nidhugg shows significant runtime improvement over other state-of-the-art tools.

The second contribution is POP, an optimal DPOR algorithm for shared memory concurrent programs under sequential consistency with threads doing reads and writes. ODPOR has problems with wasted reversal attempts of the same race multiple times, creating unnecessarily long schedules, and storing an exponential number of schedules in the worst-case. POP resolves them with parsimonious race reversal, shorter schedules, eager race reversal, and parsimonious sleep set characterization and reduces the space complexity to polynomial. Our POP implementation in Nidhugg is significantly faster than the ODPOR implementation in Nidhugg with much lower memory consumption.

The third contribution contains two more variants of the POP, Lazy POP (LPOP) and Eager POP (EPOP). POP's polynomial space complexity comes at the expense of complex parsimonious sleep handling. POP's simpler sleep set management improves average-case runtime over POP at the expense of worst-case exponential space complexity. The experimental results confirm that a simpler sleep set is a better choice when designing DPOR algorithms as they are faster and have similar memory consumption for average programs.

Link to Diva