{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:51:16Z","timestamp":1750308676393,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1216613 and 1318227"],"award-info":[{"award-number":["1216613 and 1318227"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:p>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\u00efve 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.<\/jats:p>","DOI":"10.1145\/2601339","type":"journal-article","created":{"date-parts":[[2014,7,11]],"date-time":"2014-07-11T12:09:41Z","timestamp":1405080581000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Atomicity Refinement for Verified Compilation"],"prefix":"10.1145","volume":"36","author":[{"given":"Suresh","family":"Jagannathan","sequence":"first","affiliation":[{"name":"Purdue University, IN. USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"Laporte","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Rennes 1 \/IRISA, Rennes Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gustavo","family":"Petri","sequence":"additional","affiliation":[{"name":"Purdue University, IN. USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[{"name":"ENS Rennes \/IRISA \/INRIA, Rennes Cedex, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Vitek","sequence":"additional","affiliation":[{"name":"Purdue University, IN. USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Jade Alglave Daniel Kroening Vincent Nimal and Michael Tautschnig. 2013. Software verification for weak memory via program transformation. In ESOP. 512--532. 10.1007\/978-3-642-37036-6_28","DOI":"10.1007\/978-3-642-37036-6_28"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Mark Batty Scott Owens Susmit Sarkar Peter Sewell and Tjark Weber. 2011. Mathematizing C&plus;&plus; concurrency. In POPL. 55--66. 10.1145\/1926385.1926394","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","unstructured":"Ahmed Bouajjani Egor Derevenetc and Roland Meyer. 2013. Checking and enforcing robustness against TSO. In ESOP. 533--553. 10.1007\/978-3-642-37036-6_29","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_2_1_5_1","unstructured":"Stephen D. Brookes. 1993. Full Abstraction for a Shared Variable Parallel Language. In LICS. 98--109."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","unstructured":"Sebastian Burckhardt Alexey Gotsman Madanlal Musuvathi and Hongseok Yang. 2012. Concurrent library correctness on the TSO memory model. In ESOP. 87--107. 10.1007\/978-3-642-28869-2_5","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Mike Dodds Xinyu Feng Matthew J. Parkinson and Viktor Vafeiadis. 2009. Deny-guarantee reasoning. In ESOP. 363--377. 10.1007\/978-3-642-00590-9_26","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Damien Doligez and Georges Gonthier. 1994. Portable unobtrusive garbage collection for multiprocessor systems. In POPL. 70--83. 10.1145\/174675.174673","DOI":"10.1145\/174675.174673"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"Damien Doligez and Xavier Leroy. 1993. A concurrent generational garbage collector for a multithreaded implementation of ML. In POPL. 113--123. 10.1145\/158511.158611","DOI":"10.1145\/158511.158611"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Tamar Domani Elliot K. Kolodner Ethan Lewis Eliot E. Salant Katherine Barabash Itai Lahan Yossi Levanoni Erez Petrank and Igor Yanover. 2000. Implementing an on-the-fly garbage collector for Java. In ISMM. 155--166. 10.1145\/362422.362484","DOI":"10.1145\/362422.362484"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","unstructured":"Tayfun Elmas Shaz Qadeer Ali Sezgin Omer Subasi and Serdar Tasiran. 2010. Simplifying linearizability proofs with reduction and abstraction. In TACAS. 296--311. 10.1007\/978-3-642-12002-2_25","DOI":"10.1007\/978-3-642-12002-2_25"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Tayfun Elmas Shaz Qadeer and Serdar Tasiran. 2009. A calculus of atomic actions. In POPL. 2--15. 10.1145\/1480881.1480885","DOI":"10.1145\/1480881.1480885"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Xinyu Feng. 2009. Local rely-guarantee reasoning. In POPL. 315--327. 10.1145\/1480881.1480922","DOI":"10.1145\/1480881.1480922"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Aquinas Hobor Andrew W. Appel and Francesco Zappa Nardelli. 2008. Oracle semantics for concurrent separation logic. In ESOP. 353--367.","DOI":"10.5555\/1792878.1792914"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Hongjin Liang Xinyu Feng and Ming Fu. 2012a. A rely-guarantee-based simulation for verifying concurrent program transformations. In POPL. 455--468. 10.1145\/2103656.2103711","DOI":"10.1145\/2103656.2103711"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Andreas Lochbihler. 2010. Verifying a compiler for Java threads. In ESOP. 427--447. 10.1007\/978-3-642-11957-6_23","DOI":"10.1007\/978-3-642-11957-6_23"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863584"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Tom Ridge. 2010. A rely-guarantee proof system for x86-TSO. In VSTTE. 55--70.","DOI":"10.5555\/1884866.1884873"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"Susmit Sarkar Peter Sewell Jade Alglave Luc Maranget and Derek Williams. 2011. Understanding POWER multiprocessors. In PLDI. 175--186. 10.1145\/1993498.1993520","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926393"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/174556"},{"key":"e_1_2_1_29_1","volume-title":"Systems Programming: Coping with Parallelism - RJ 5118. Technical Report","author":"Treiber R. Kent","year":"1986","unstructured":"R. Kent Treiber. 1986. Systems Programming: Coping with Parallelism - RJ 5118. Technical Report. IBM Almaden Research Center."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Aaron Joseph Turon and Mitchell Wand. 2011. A separation logic for refining concurrent objects. In POPL. 247--258. 10.1145\/1926385.1926415","DOI":"10.1145\/1926385.1926415"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392200.2392220"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2601339","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2601339","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:00:53Z","timestamp":1750276853000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2601339"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1145\/2601339"],"URL":"https:\/\/doi.org\/10.1145\/2601339","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2014,7]]},"assertion":[{"value":"2013-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}