SATCheck: SAT-directed stateless model checking for SC and TSO

3 years 11 months ago
SATCheck: SAT-directed stateless model checking for SC and TSO
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 prototy...
Brian Demsky, Patrick Lam
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Authors Brian Demsky, Patrick Lam
Comments (0)