TY - GEN
T1 - Verifying fence elimination optimisations
AU - Vafeiadis, Viktor
AU - Zappa Nardelli, Francesco
PY - 2011/9/28
Y1 - 2011/9/28
N2 - We consider simple compiler optimisations for removing redundant memory fences in programs running on top of the x86-TSO relaxed memory model. While the optimisations are performed using standard thread-local control flow analyses, their correctness is subtle and relies on a non-standard global simulation argument. The implementation and the proof of correctness are programmed in Coq as part of CompCertTSO, a fully-fledged certified compiler from a concurrent extension of a C-like language to x86 assembler. In this article, we describe the soundness proof of the optimisations and evaluate their effectiveness.
AB - We consider simple compiler optimisations for removing redundant memory fences in programs running on top of the x86-TSO relaxed memory model. While the optimisations are performed using standard thread-local control flow analyses, their correctness is subtle and relies on a non-standard global simulation argument. The implementation and the proof of correctness are programmed in Coq as part of CompCertTSO, a fully-fledged certified compiler from a concurrent extension of a C-like language to x86 assembler. In this article, we describe the soundness proof of the optimisations and evaluate their effectiveness.
UR - https://www.scopus.com/pages/publications/80053096806
U2 - 10.1007/978-3-642-23702-7_14
DO - 10.1007/978-3-642-23702-7_14
M3 - Conference contribution
AN - SCOPUS:80053096806
SN - 9783642237010
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 146
EP - 162
BT - Static Analysis - 18th International Symposium, SAS 2011, Proceedings
T2 - 18th International Static Analysis Symposium, SAS 2011
Y2 - 14 September 2010 through 16 September 2010
ER -