The C++ relaxed memory model is very challenging. The crucial task of writing correct and efficient low-level concurrent programs for C++ under this model is known to be very challenging: the model’s complexity is such that it eludes even veteran systems programmers and requires the attention of formal semantics experts. To maintain efficiency, the programmer wants the most relaxed synchronization required to preserve correctness, and nothing more (even when it simplifies reasoning). Unfortunately, manually finding the right synchronization is extremely difficult, as it requires the programmer to reason about subtle interactions of the memory model. Our goal is to assist the programmer by automatically synthesizing the required synchronization.

We will show an algorithm that exhaustively explores the traces of an input program P under the C++ relaxed memory model, and looks for error traces — traces which do not satisfy the correctness criteria. If our algorithm finds an error trace, it searches it for instances of violation patterns, behaviors that may occur under C++ RMM but not under SC and that we know how to avoid, and then use Avoidance templates which are strategies to synthesize memory order annotations of memory instructions such as load, store, and cas.

We successfully synthesized nontrivial memory order synchronization for several challenging concurrent algorithms, including a state of the art Read-Copy-Update (RCU) algorithm.