Wed 28 Oct 2015 10:52 - 11:15 at Grand Station 1 - 1. Model Checking Chair(s): Julian Dolby

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 Oct

oopsla2015
10:30 - 12:00: OOPSLA - 1. Model Checking at Grand Station 1
Chair(s): Julian DolbyIBM Research
oopsla201510:30 - 10:52
Talk
Anthony Widjaja LinYale-NUS College, Singapore, Matthew HagueRoyal Holloway University of London, UK, C.-H. Luke OngUniversity of Oxford, UK
Link to publication
oopsla201510:52 - 11:15
Talk
Brian DemskyUniversity of California at Irvine, USA, Patrick LamUniversity of Waterloo, Canada
Link to publication
oopsla201511:15 - 11:37
Talk
Ivan KurajMassachusetts Institute of Technology, USA, Viktor KuncakEPFL, Switzerland, Daniel JacksonMassachusetts Institute of Technology, USA
DOI
oopsla201511:37 - 12:00
Talk
Casper Svenning JensenAarhus University, Denmark, Anders MøllerAarhus University, Veselin RaychevETH Zurich, Switzerland, Dimitar DimitrovETH Zurich, Switzerland, Martin VechevETH Zurich, Switzerland
DOI