SATCheck: SAT-Directed Stateless Model Checking for SC and TSO
SATCheck implements a new approach to model checking concurrent code. The key insight is to leverage SAT solving technology to more effectively perform partial order reduction on concrete executions. The model checking algorithm is described in more detail in this paper (published in OOPSLA ’15):
Getting Started
The easiest option is to grab a copy of our prepackaged vagrant VM. You can obtain it using the following command:
git clone https://github.com/patricklam/satcheck-vagrant.git
Then follow the directions in the artifact-getting-started.md file.
Getting The Code
If you want to build the code outside of the VM, you can get the code via our repository. Use the vagrant bootstrap.sh file as a guide of how to compile and setup the repositories.
If you haven’t done so already, you may download SATCheck using git:
git clone git://plrg.eecs.uci.edu/satcheck.git
You will also need our SAT Solver library. You can get this with the following command:
git clone git://plrg.eecs.uci.edu/satlib.gitUseful Options
-h
Prints out help.
-b
Only attempts to explore all branches.
-Y
Turns on yield support.
-v
Verbose: show extra information.
See Also
The SATcheck source and accompanying SATlib source on Gitweb:
Acknowledgments
This material is based upon work supported by the National Science Foundation under Grant Nos CCF-0846195, CCF-1217854, CNS-1228995, and CCF-1319786.
Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.
Copyright
The SATCheck backend is Copyright © 2013 Regents of the University of California. All rights reserved.
The SATCheck backend is distributed under the GPL v2. See the LICENSE file for details.
Contact
Please feel free to contact us for more information. Bug reports are welcome, and we are happy to hear from our users.
Contact Brian Demsky at bdemsky@uci.edu for questions about the SATCheck backend or Patrick Lam at patrick.lam@uwaterloo.ca for questions about the Clang frontend.