Skip to Main content Skip to Navigation
New interface
Journal articles

Atomicity Refinement for Verified Compilation

Suresh Jagannathan 1 Vincent Laporte 2 Gustavo Petri 1 David Pichardie 2 Jan Vitek 1 
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We consider the verified compilation of high-level managed languages like Java or C# whose intermediate representations provide support for shared-memory synchronization and automatic memory management. Our development is framed in the context of the Total Store Order relaxed memory model. Ensuring com-plier correctness is challenging because high-level actions are translated into sequences of non-atomic ac-tions with compiler-injected snippets of racy code; the behavior of this code depends not only on the actions of other threads, but also on out-of-order executions performed by the processor. A naïve proof of correctness would require reasoning over all possible thread interleavings. In this paper we propose a refinement-based proof methodology that precisely relates concurrent code expressed at different abstraction levels, cognizant throughout of the relaxed memory semantics of the underlying processor. Our technique allows the compiler writer to reason compositionally about the atomicity of low-level concurrent code used to implement man-aged services. We illustrate our approach with examples taken from the verification of a concurrent garbage collector.
Document type :
Journal articles
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : David Pichardie Connect in order to contact the contributor
Submitted on : Wednesday, January 28, 2015 - 11:46:12 PM
Last modification on : Friday, November 18, 2022 - 9:24:30 AM


  • HAL Id : hal-01102435, version 1


Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, Jan Vitek. Atomicity Refinement for Verified Compilation. ACM Transactions on Programming Languages and Systems (TOPLAS), 2014, pp.30. ⟨hal-01102435⟩



Record views