{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T09:14:24Z","timestamp":1769073264018,"version":"3.49.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2013,6,1]],"date-time":"2013-06-01T00:00:00Z","timestamp":1370044800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100012950","name":"INRIA","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100012950","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-06-SETI-010-02"],"award-info":[{"award-number":["ANR-06-SETI-010-02"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-11-JS02-011"],"award-info":[{"award-number":["ANR-11-JS02-011"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/F036345, EP\/H005633, EP\/K008528"],"award-info":[{"award-number":["EP\/F036345, EP\/H005633, EP\/K008528"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2013,6]]},"abstract":"<jats:p>In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behavior of the hardware, the effects of compiler optimization on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified compilation both essential and challenging.<\/jats:p>\n          <jats:p>We describe ClightTSO, a concurrent extension of CompCert\u2019s Clight in which the TSO-based memory model of x86 multiprocessors is exposed for high-performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable behavior of the generated assembly code (if it does not run out of memory) is also possible in the source semantics. We also describe some verified fence-elimination optimizations, integrated into CompCertTSO.<\/jats:p>","DOI":"10.1145\/2487241.2487248","type":"journal-article","created":{"date-parts":[[2013,7,2]],"date-time":"2013-07-02T14:32:49Z","timestamp":1372775569000},"page":"1-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":113,"title":["CompCertTSO"],"prefix":"10.1145","volume":"60","author":[{"given":"Jaroslav","family":"\u0160ev\u010d\u00edk","sequence":"first","affiliation":[{"name":"Microsoft"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS"}]},{"given":"Francesco","family":"Zappa Nardelli","sequence":"additional","affiliation":[{"name":"INRIA"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge"}]}],"member":"320","published-online":{"date-parts":[[2013,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_2_1_7_1","first-page":"2011","article-title":"Programming Languages --- C++","volume":"14882","author":"Ed Pete Becker","year":"2011","unstructured":"Pete Becker Ed . 2011 . Programming Languages --- C++ , ISO\/IEC 14882 : 2011 (N3242). DOI:http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2011\/n3242.pdf. (last accessed 5\/13). (N3242 is a near-final draft standard which is available online). Pete Becker Ed. 2011. Programming Languages --- C++, ISO\/IEC 14882:2011 (N3242). DOI:http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2011\/n3242.pdf. (last accessed 5\/13). (N3242 is a near-final draft standard which is available online).","journal-title":"ISO\/IEC"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596567"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9148-3"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065042"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11970-5_7"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the IEEE International Symposium on Workload Characterization (IISWC). 35--46","author":"Minh Chi Cao","year":"2008","unstructured":"Chi Cao Minh , JaeWoong Chung , Christos Kozyrakis , and Kunle Olukotun . 2008 . STAMP: Stanford transactional applications for multi-processing . In Proceedings of the IEEE International Symposium on Workload Characterization (IISWC). 35--46 . Chi Cao Minh, JaeWoong Chung, Christos Kozyrakis, and Kunle Olukotun. 2008. STAMP: Stanford transactional applications for multi-processing. In Proceedings of the IEEE International Symposium on Workload Characterization (IISWC). 35--46."},{"key":"e_1_2_1_15_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 16th European Symposium on Programming (ESOP)","author":"Cenciarelli Pietro","unstructured":"Pietro Cenciarelli , Alexander Knapp , and Eleonora Sibilio . 2007. The Java memory model: Operationally, denotationally, axiomatically . In Proceedings of the 16th European Symposium on Programming (ESOP) . Lecture Notes in Computer Science , vol. 4421 , Springer-Verlag , Berlin , 331--346. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-71316-6_23. 10.1007\/978-3-540-71316-6_23 Pietro Cenciarelli, Alexander Knapp, and Eleonora Sibilio. 2007. The Java memory model: Operationally, denotationally, axiomatically. In Proceedings of the 16th European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 4421, Springer-Verlag, Berlin, 331--346. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-71316-6_23."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_2_1_17_1","unstructured":"Coq. 2011. The Coq proof assistant. http:\/\/coq.inria.fr\/ version 8.3pl1. Coq . 2011. The Coq proof assistant. http:\/\/coq.inria.fr\/ version 8.3pl1."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11864219_14"},{"key":"e_1_2_1_20_1","unstructured":"Georges Gonthier and Assia Mahboubi. 2007. A small scale reflection extension for the Coq system. Tech. rep. 6455. INRIA.  Georges Gonthier and Assia Mahboubi. 2007. A small scale reflection extension for the Coq system. Tech. rep. 6455. INRIA."},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the European Symposium on Programming (ESOP)","author":"Hobor Aquinas","unstructured":"Aquinas Hobor , Andrew W. Appel , and Francesco Zappa Nardelli . 2008. Oracle semantics for concurrent separation logic . In Proceedings of the European Symposium on Programming (ESOP) . Lecture Notes in Computer Science , vol. 4960 . Springer-Verlag , Berlin , 353--367. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-78739-6_27. 10.1007\/978-3-540-78739-6_27 Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. 2008. Oracle semantics for concurrent separation logic. In Proceedings of the European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 4960. Springer-Verlag, Berlin, 353--367. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-540-78739-6_27."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0041-6"},{"key":"e_1_2_1_23_1","first-page":"2011","article-title":"Programming languages --- C","volume":"9899","author":"ISO.","year":"2011","unstructured":"ISO. 2011 . Programming languages --- C , ISO\/IEC 9899 : 2011 (N1547). http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/PostBatavia.tar.bz2 (last accessed 5\/13). (N1547 is a near-final draft standard which is available online). ISO. 2011. Programming languages --- C, ISO\/IEC 9899:2011 (N1547). http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/PostBatavia.tar.bz2 (last accessed 5\/13). (N1547 is a near-final draft standard which is available online).","journal-title":"ISO\/IEC"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the Formal Methods in Computer-Aided Design (FMCAD). FMCAD Inc.","author":"Kuperstein Michael","year":"2010","unstructured":"Michael Kuperstein , Martin Vechev , and Eran Yahav . 2010 . Automatic inference of memory fences . In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD). FMCAD Inc. , Austin, TX, 111--120. DOI:http:\/\/dx.doi.org\/10.1145\/2261417.2261438. 10.1145\/2261417.2261438 Michael Kuperstein, Martin Vechev, and Eran Yahav. 2010. Automatic inference of memory fences. In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD). FMCAD Inc., Austin, TX, 111--120. DOI:http:\/\/dx.doi.org\/10.1145\/2261417.2261438."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_26_1","volume-title":"Concurrent Programming in Java","author":"Lea Doug","unstructured":"Doug Lea . 1999. Concurrent Programming in Java 2 nd Ed. Design Principles and Patterns. Addison-Wesley Longman Publishing Co. , Inc., Boston, MA. Doug Lea. 1999. Concurrent Programming in Java 2nd Ed. Design Principles and Patterns. Addison-Wesley Longman Publishing Co., Inc., Boston, MA.","edition":"2"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.947002"},{"key":"e_1_2_1_28_1","unstructured":"Xavier Leroy. 2009a. The compcert verified compiler v. 1.5. http:\/\/compcert.inria.fr\/release\/compcert-1.5.tgz (last accessed 5\/13).  Xavier Leroy. 2009a. The compcert verified compiler v. 1.5. http:\/\/compcert.inria.fr\/release\/compcert-1.5.tgz (last accessed 5\/13)."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_1_31_1","unstructured":"Xavier Leroy. 2013. The Compcert verified compiler v. 1.12.1. (2013). http:\/\/compcert.inria.fr\/release\/compcert-1.12.1.tgz (last accessed 5\/13).  Xavier Leroy. 2013. The Compcert verified compiler v. 1.12.1. (2013). http:\/\/compcert.inria.fr\/release\/compcert-1.12.1.tgz (last accessed 5\/13)."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_2_1_33_1","unstructured":"Linux. 1999. Linux Kernel mailing list thread \u201cspin_unlock optimization(i386)\u201d 119 messages Nov. 20--Dec. 7th. http:\/\/www.gossamer-threads.com\/lists\/engine?post=105365;list=linux (last accessed 5\/13).  Linux. 1999. Linux Kernel mailing list thread \u201cspin_unlock optimization(i386)\u201d 119 messages Nov. 20--Dec. 7th. http:\/\/www.gossamer-threads.com\/lists\/engine?post=105365;list=linux (last accessed 5\/13)."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_23"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_25"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993522"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"e_1_2_1_40_1","volume-title":"Communication and Concurrency","author":"Milner Robin","unstructured":"Robin Milner . 1989. Communication and Concurrency . Prentice Hall International . Robin Milner. 1989. Communication and Concurrency. Prentice Hall International."},{"key":"e_1_2_1_41_1","unstructured":"Robin Milner and R. Weyrauch. 1972. Proving compiler correctness in a mechanized logic. In Machine Intelligence 7 B. Meltzer and D. Michie Eds. American Elsevier New York 51--70.  Robin Milner and R. Weyrauch. 1972. Proving compiler correctness in a mechanized logic. In Machine Intelligence 7 B. Meltzer and D. Michie Eds. American Elsevier New York 51--70."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/359060.359069"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706313"},{"key":"e_1_2_1_44_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 24th European Conference on Object-Oriented Programming (ECOOP)","author":"Owens Scott","unstructured":"Scott Owens . 2010. Reasoning about the implementation of concurrency abstractions on x86-TSO . In Proceedings of the 24th European Conference on Object-Oriented Programming (ECOOP) . Lecture Notes in Computer Science , vol. 6183 . Springer-Verlag , Berlin , 478--503. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-14107-2_23. 10.1007\/978-3-642-14107-2_23 Scott Owens. 2010. Reasoning about the implementation of concurrency abstractions on x86-TSO. In Proceedings of the 24th European Conference on Object-Oriented Programming (ECOOP). Lecture Notes in Computer Science, vol. 6183. Springer-Verlag, Berlin, 478--503. DOI:http:\/\/dx.doi.org\/10.1007\/978-3-642-14107-2_23."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1002\/1096-9128(200005)12:6<445::AID-CPE484>3.0.CO;2-A"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_3"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926393"},{"key":"e_1_2_1_52_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 8th International Conference on Concurrency Theory (CONCUR)","author":"Sewell Peter","unstructured":"Peter Sewell . 1997. On implementations and semantics of a concurrent programming language . In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR) . Lecture Notes in Computer Science , Springer-Verlag , Berlin , 391--405. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-63141-0_27. 10.1007\/3-540-63141-0_27 Peter Sewell. 1997. On implementations and semantics of a concurrent programming language. In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, Springer-Verlag, Berlin, 391--405. DOI:http:\/\/dx.doi.org\/10.1007\/3-540-63141-0_27."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_2_1_56_1","unstructured":"SPARC International Inc. 1992. The SPARC Architecture Manual V. 8 Revision SAV080SI9308. http:\/\/www.sparc.org\/standards\/V8.pdf (last accessed 5\/13).   SPARC International Inc. 1992. The SPARC Architecture Manual V. 8 Revision SAV080SI9308. http:\/\/www.sparc.org\/standards\/V8.pdf (last accessed 5\/13)."},{"key":"e_1_2_1_57_1","unstructured":"SPARC International Inc. 1994. The SPARC Architecture Manual V. 9. http:\/\/www.sparc.com\/standards\/SPARCV9.pdf (last accessed 5\/13).   SPARC International Inc. 1994. The SPARC Architecture Manual V. 9. http:\/\/www.sparc.com\/standards\/SPARCV9.pdf (last accessed 5\/13)."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929529.1929535"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065944.1065947"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806635"},{"key":"e_1_2_1_61_1","unstructured":"R. Kent Treiber. 1986. Systems programming: Coping with parallelism. Tech. rep. TR RJ 5118. IBM.  R. Kent Treiber. 1986. Systems programming: Coping with parallelism. Tech. rep. TR RJ 5118. IBM."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041566"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2487241.2487248","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2487241.2487248","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:48:39Z","timestamp":1750236519000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2487241.2487248"}},"subtitle":["A Verified Compiler for Relaxed-Memory Concurrency"],"short-title":[],"issued":{"date-parts":[[2013,6]]},"references-count":60,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["10.1145\/2487241.2487248"],"URL":"https:\/\/doi.org\/10.1145\/2487241.2487248","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,6]]},"assertion":[{"value":"2011-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-06-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}