Blogs (9) >>
SPLASH 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Thu 3 Nov 2016 10:55 - 11:20 at Matterhorn 1 - Concurrency Analysis and Model Checking Chair(s): Thomas Gross

Verifying concurrent programs is challenging due to the exponentially large thread interleaving space. The problem is exacerbated by relaxed memory models such as Total Store Order (TSO) and Partial Store Order (PSO) which further explode the interleaving space by reordering instructions. A recent advance, Maximal Causality Reduction (MCR), has shown great promise to improve verification effectiveness by maximally reducing redundant explorations. However, the original MCR only works for the Sequential Consistency (SC) memory model, but not for TSO and PSO. In this paper, we develop novel extensions to MCR by solving two key problems under TSO and PSO: 1) generating interleavings that can reach new states by encoding the operational semantics of TSO and PSO with first-order logical constraints and solving them with SMT solvers, and 2) enforcing TSO and PSO interleavings by developing novel replay algorithms that allow executions out of the program order. We show that our approach successfully enables MCR to effectively explore TSO and PSO interleavings. We have compared our approach with a recent Dynamic Partial Order Reduction (DPOR) algorithm for TSO and PSO and a SAT-based stateless model checking approach. Our results show that our approach is much more effective than the other approaches for both state-space exploration and bug finding – on average it explores 5-10X fewer executions and finds many bugs that the other tools cannot find.

Thu 3 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Concurrency Analysis and Model CheckingOOPSLA at Matterhorn 1
Chair(s): Thomas Gross ETH Zurich
10:30
25m
Talk
Directed Synthesis of Failing Concurrent Executions
OOPSLA
Malavika Samak Indian Institute of Science, Bangalore, Omer Tripp IBM Research, USA, Murali Krishna Ramanathan Indian Institute of Science, Bangalore
DOI Media Attached
10:55
25m
Talk
Maximal Causality Reduction for TSO and PSO
OOPSLA
Shiyou Huang Texas A&M University, Jeff Huang Texas A&M University
DOI
11:20
25m
Talk
Stateless Model Checking with Data-Race Preemption Points
OOPSLA
Ben Blum Carnegie Mellon University, Garth Gibson Carnegie Mellon University
DOI Pre-print Media Attached
11:45
25m
Talk
Precise and Maximal Race Detection from Incomplete Traces
OOPSLA
Jeff Huang Texas A&M University, Arun Krishnakumar Rajagopalan Texas A&M University
DOI Media Attached