Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it

DOI10.1145/2676726.2676995zbMath1345.68087OpenAlexW2000659103MaRDI QIDQ2819807

Viktor Vafeiadis, Soham Chakraborty, Robin Morisset, Thibaut Balabonski, F. Zappa Nardelli

Publication date: 29 September 2016

Published in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://zenodo.org/record/32523

zbMATH Keywords

program transformationsconcurrencycompilersweak memory modelsC/C++

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20)

Related Items (3)

Owicki-Gries Reasoning for Weak Memory Models ⋮ A formal C memory model for separation logic ⋮ An operational happens-before memory model

Uses Software

• Coq
• CompCertTSO
• CDSChecker

This page was built for publication: Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it