Writing low-level concurrent code is well known to be challenging and error prone. The widespread deployment of multi-core hardware and the shift towards using low-level concurrent data structures has moved the problem into the mainstream. Finding bugs in such code may require finding a specific bug-revealing thread interleaving out of a huge space of parallel executions. Model-checking is a powerful technique for exhaustively testing code. However, scaling model checking presents a significant challenge. In this paper we present a new and more scalable technique for model checking concurrent code, based on concrete execution. Our technique observes concrete behaviors, builds a model of these behaviors, encodes the model in SAT, and leverages SAT solver technology to find executions that reveal new behaviors. It then runs the new execution, incorporates the newly observed behavior, and repeats the process until it has explored all reachable behaviors. We have implemented a prototype of our approach in the SATCheck tool. Our tool supports both the Total Store Ordering (TSO) and Sequentially Consistent (SC) memory models. We evaulate SATCheck by testing several concurrent data structure implementations and comparing its performance to the original DPOR stateless model checking algorithm implemented in CDSChecker, the source DPOR algorithm implemented in Nidhugg, and CheckFence. Our experiments show that SATCheck scales better than previous approaches while at the same time operating on concrete executions.
Wed 28 OctDisplayed time zone: Eastern Time (US & Canada) change
10:30 - 12:00 | |||
10:30 22mTalk | Detecting Redundant CSS Rules in HTML5 Applications: A Tree Rewriting Approach OOPSLA Anthony Widjaja Lin Yale-NUS College, Singapore, Matthew Hague Royal Holloway University of London, UK, C.-H. Luke Ong University of Oxford, UK Link to publication | ||
10:52 22mTalk | SATCheck: SAT-Directed Stateless Model Checking for SC and TSO OOPSLA Link to publication | ||
11:15 22mTalk | Programming with Enumerable Sets of Structures OOPSLA Ivan Kuraj Massachusetts Institute of Technology, USA, Viktor Kunčak EPFL, Switzerland, Daniel Jackson Massachusetts Institute of Technology, USA DOI | ||
11:37 22mTalk | Stateless Model Checking of Event-Driven Applications OOPSLA Casper Svenning Jensen Aarhus University, Denmark, Anders Møller Aarhus University, Veselin Raychev ETH Zurich, Switzerland, Dimitar Dimitrov ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Switzerland DOI |