Robustness against the C/C++11 Memory Model

Concurrency is extremely useful, however reasoning about the correctness of concurrent programs is more difficult than ever. Sequential consistency (SC) semantics provide the ability to reason about correctness, however these come at a high synchronization cost. C11 introduced a memory model that was supposed to help with these problems, attempting to provide balance between performance and reasoning. However, this model was much more complicated than expected, proving to be a challenge even for domain experts. We propose a method that enables the programmer to reason about correctness with SC semantics without compromising performance. By proving robustness of a program it can only exhibit SC behaviors and can thus be reasoned about with SC semantics.