Name
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 complier correctness is challenging because high-level actions are translated into sequences of nonatomic actions 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 article, 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 managed services. We illustrate our approach with examples taken from the verification of a concurrent garbage collector. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2601339 | ACM Trans. Program. Lang. Syst. |
Keywords | DocType | Volume |
verified compilation,compiler-injected code snippet,concurrent garbage collector,security,processors,mechanized proof assistant,specifying and verifying and reasoning about programs,concurrent programming,low-level concurrent code,verification,software/program verification,concurrent code,automatic memory management,garbage collection,languages,memory semantics,concurrency,allocation fast path,high-level managed language,garbage collector,reliability,toplas paper,refinement,compiler transformations and optimizations,atomicity,atomicity refinement,managed languages | Conference | 36 |
Issue | ISSN | Citations |
2 | 0164-0925 | 5 |
PageRank | References | Authors |
0.42 | 21 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Suresh Jagannathan | 1 | 287 | 20.35 |
| Gustavo Petri | 2 | 44 | 8.58 |
| Jan Vitek | 3 | 2259 | 165.75 |
| david pichardie | 4 | 488 | 33.73 |
| Vincent Laporte | 5 | 81 | 3.61 |