CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency

Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, Peter Sewell. CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. Journal of the ACM, 60(3):22, 2013. [doi]

Abstract

Abstract is missing.