Software for Relaxed Memory Models
Software for relaxed memory models (especially the C/C++ memory model) developed by our group are available below:
C11Tester is a testing framework for C11/C++11 which explores the behaviors of the C/C++ memory model. It is designed to handle much larger executions, but is not exhaustive in its exploration.
CDSChecker is a model checker for C11/C++11 which exhaustively explores the behaviors of code under the C/C++ memory model. More details in this paper (OOPSLA'13).
AuotMO is tool framework that can infer memory order parameters for C/C++11 concurrent programs such that the programs only exhibit SC behaviors for the test cases provided by developers. More details in this paper (OOPSLA'15).
SATCheck implements a new approach to model checking concurrent code. More details in this paper (OOPSLA'15).
CDSSpec allows developers to specify C/C++11 concurrent data structures and check their implementations against the specifications. More details in this paper (PPoPP'17).
This includes variants of compiler implementations that forbid OOTA results in C/C++ by preserving syntactic dependencies or atomic load-store ordering. More details in this paper (OOPSLA'18).