The multi-core revolution has pushed programmers and algorithm designers to build algorithms that leverage concurrency. This notoriously difficult task is futher complicated by the existence of weak architecture and language memory models. The presence of many such memory models has traditionally forced correctness proofs for lock-free concurrent algorithms to be performed on a per-model basis, resulting in a significant duplication of effort. We demonstrate that the correctness of lock-free concurrent algorithms can be proved once for implementations that can be compiled to run correctly and efficiently on all mainstream memory models.

• PDF