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

Displayed time zone: Eastern Time (US & Canada) change

10:30 - 12:00
1. Model CheckingOOPSLA at Grand Station 1
Chair(s): Julian Dolby IBM Research
10:30
22m
Talk
Detecting Redundant CSS Rules in HTML5 Applications: A Tree Rewriting ApproachOOPSLA Artifact
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
22m
Talk
SATCheck: SAT-Directed Stateless Model Checking for SC and TSOOOPSLA Artifact
OOPSLA
Brian Demsky University of California at Irvine, USA, Patrick Lam University of Waterloo, Canada
Link to publication
11:15
22m
Talk
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
22m
Talk
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