Programming Languages Research Group

Software for Relaxed Memory Models

Software for relaxed memory models (especially the C/C++ memory model) developed by our group are available below:


CDSChecker: A Model Checker for C11 and C++11 Atomics

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).

AutoMO: A Memory Order Parameter Inference Framework for C/C++11

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: A SAT-Directed Stateless Model Checker for SC and TSO

SATCheck implements a new approach to model checking concurrent code. More details in this paper (OOPSLA'15).

CDSSpec: A Specification Checking Framework for C/C++11 Concurrent Data Structures

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).

An LLVM-Based Compiler Framework that Forbids Out-of-Thin-Air Results

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).