Compositional verification of compiler optimisations on relaxed memory

DOI10.1007/978-3-319-89884-1_36MaRDI QIDQ2324020zbMATH OpenOpenAlexFDO

Authors Mike Dodds, Mark Batty, Alexey Gotsman

Publication date 13 September 2019

Full work available at URL https://arxiv.org/abs/1802.05918, https://kar.kent.ac.uk/66630/1/main.pdf

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: A valid compiler optimisation transforms a block in a program without introducing new observable behaviours to the program as a whole. Deciding which optimisations are valid can be difficult, and depends closely on the semantic model of the programming language. Axiomatic relaxed models, such as C++11, present particular challenges for determining validity, because such models allow subtle effects of a block transformation to be observed by the rest of the program. In this paper we present a denotational theory that captures optimisation validity on an axiomatic model corresponding to a fragment of C++11. Our theory allows verifying an optimisation compositionally, by considering only the block it transforms instead of the whole program. Using this property, we realise the theory in the first push-button tool that can verify real-world optimisations under an axiomatic memory model.

Recommendations

• Common compiler optimisations are invalid in the C11 memory model and what we can do about it
• Verifying optimizations for concurrent programs
• Relaxed-memory concurrency and verified compilation
• CompCertTSO
• Verified Compilation for Shared-Memory C

Cited in

(10)

• Explaining relaxed memory models with program transformations
• \textsc{CompCertS}: a memory-aware verified C compiler using a pointer as integer semantics
• Common compiler optimisations are invalid in the C11 memory model and what we can do about it
• Modular relaxed dependencies in weak memory concurrency
• Verifying optimizations for concurrent programs
• A verifiable SSA program representation for aggressive compiler optimization
• CompCertTSO
• Computer Algebra in Scientific Computing
• A Framework for Formal Verification of Compiler Optimizations
• Two-sorted algebraic decompositions of Brookes's shared-state denotational semantics

This page was built for publication: Compositional verification of compiler optimisations on relaxed memory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2324020)