{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T12:59:53Z","timestamp":1779886793015,"version":"3.53.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/V519625\/1"],"award-info":[{"award-number":["EP\/V519625\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"epsrc","doi-asserted-by":"crossref","award":["EP\/R006865\/1"],"award-info":[{"award-number":["EP\/R006865\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>The correctness of complex software depends on the correctness of both the source code and the compilers that generate corresponding binary code. Compilers must do more than preserve the semantics of a single source file: they must ensure that generated binaries can be composed with other binaries to form a final executable. The compatibility of composition is ensured using an Application Binary Interface (ABI), which specifies details of calling conventions, exception handling, and so on. Unfortunately, there are no official ABIs for concurrent programs, so different atomics mappings, although correct in isolation, may induce bugs when composed. Indeed, today, mixing binaries generated by different compilers can lead to an erroneous resulting binary.<\/jats:p>\n                  <jats:p>\n                    We present\n                    <jats:italic toggle=\"yes\">mix testing<\/jats:italic>\n                    : a new technique designed to find compiler bugs when the instructions of a C\/C++ test are separately compiled for multiple compatible architectures and then mixed together. We define a class of compiler bugs, coined\n                    <jats:italic toggle=\"yes\">mixing bugs<\/jats:italic>\n                    , that arise when parts of a program are compiled separately using different mappings from C\/C++ atomic operations to assembly sequences. To demonstrate the generality of mix testing, we have designed and implemented a tool,\n                    <jats:monospace>atomic-mixer<\/jats:monospace>\n                    , which we have used: (a) to reproduce one existing non-mixing bug that state-of-the-art concurrency testing tools are limited to being able to find (showing that\n                    <jats:monospace>atomic-mixer<\/jats:monospace>\n                    at least meets the capabilities of these tools), and (b) to find four previously-unknown mixing bugs in LLVM and GCC, and one prospective mixing bug in mappings proposed for the Java Virtual Machine. Lastly, we have worked with engineers at Arm to specify, for the first time, an atomics ABI for Armv8, and have used\n                    <jats:monospace>atomic-mixer<\/jats:monospace>\n                    to validate the LLVM and GCC compilers against it.\n                  <\/jats:p>","DOI":"10.1145\/3689727","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"442-467","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Mix Testing: Specifying and Testing ABI Compatibility of C\/C++ Atomics Implementations"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-6748-5028","authenticated-orcid":false,"given":"Luke","family":"Geeson","sequence":"first","affiliation":[{"name":"University College London - Arm Ltd, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7536-4496","authenticated-orcid":false,"given":"James","family":"Brotherston","sequence":"additional","affiliation":[{"name":"University College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3429-6967","authenticated-orcid":false,"given":"Wilco","family":"Dijkstra","sequence":"additional","affiliation":[{"name":"Arm Ltd, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7448-7961","authenticated-orcid":false,"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-3864-3662","authenticated-orcid":false,"given":"Lee","family":"Smith","sequence":"additional","affiliation":[{"name":"Arm Ltd, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1646-7935","authenticated-orcid":false,"given":"Tyler","family":"Sorensen","sequence":"additional","affiliation":[{"name":"University of California at Santa Cruz, Santa Cruz, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6735-5533","authenticated-orcid":false,"given":"John","family":"Wickerson","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"Jade Alglave and Luc Maranget. 2021. herdtools7. https:\/\/github.com\/herd\/herdtools7. Accessed: 2019-10-06."},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0135-z"},{"key":"e_1_3_1_4_2","unstructured":"Arm-Limited. 2021. Armv8 AArch64 Memory Model.https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/aarch64.cat."},{"key":"e_1_3_1_5_2","unstructured":"Arm-Limited. 2024. https:\/\/github.com\/ARM-software\/abi-aa\/issues. Accessed: 2024-14-02."},{"key":"e_1_3_1_6_2","volume-title":"Arm Architecture Reference Manual","author":"Arm-Limited","year":"2024","unstructured":"Arm-Limited. 2024. Arm Architecture Reference Manual. Arm-Limited, Cambridge, UK. https:\/\/developer.arm.com\/documentation\/ddi0487\/latest\/"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1150019.1136489"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_3_1_9_2","volume-title":"The C11 and C++11 Concurrency Model","author":"Batty Mark John","year":"2014","unstructured":"Mark John Batty. 2014. The C11 and C++11 Concurrency Model. Ph. D. Dissertation. University of Cambridge."},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2854038.2854051"},{"key":"e_1_3_1_12_2","unstructured":"Simon Colin. 2022. RC11 Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/rc11.cat."},{"key":"e_1_3_1_13_2","unstructured":"Will Deacon. 2014. arm64: atomics: fix use of acquire\u2009+\u2009release for full barrier semantics. http:\/\/lists.infradead.org\/pipermail\/linux-arm-kernel\/2014-February\/229588.html."},{"key":"e_1_3_1_14_2","unstructured":"Wilco Dijkstra. 2024. Alignment of _Atomic structs incompatible between GCC and LLVM. https:\/\/gcc.gnu.org\/bugzilla\/show_bug.cgi?id=115954."},{"key":"e_1_3_1_15_2","unstructured":"Luke Geeson. 2023. [AArch64]: Atomic Exchange Allows Reordering past Acquire Fence. https:\/\/github.com\/llvm\/llvm-project\/issues\/68428."},{"key":"e_1_3_1_16_2","unstructured":"Luke Geeson. 2023. Add (__)(u)int128(_t) parsing to CType. https:\/\/github.com\/herd\/herdtools7\/pull\/520."},{"key":"e_1_3_1_17_2","unstructured":"Luke Geeson. 2023. [lib\/gen]: fixed __int128 parsing. https:\/\/github.com\/herd\/herdtools7\/pull\/553."},{"key":"e_1_3_1_18_2","unstructured":"Luke Geeson. 2024. [AArch64]: 128-bit Sequentially Consistent load allows reordering before prior store when armv8 and armv8.4 implementations are Mixed. https:\/\/github.com\/llvm\/llvm-project\/issues\/81978."},{"key":"e_1_3_1_19_2","unstructured":"Luke Geeson. 2024. [Armv7-a]: Sequentially Consistent Load Allows Reordering of Prior Store when Implementations are Mixed. https:\/\/github.com\/llvm\/llvm-project\/issues\/65541#issuecomment-1709229837."},{"key":"e_1_3_1_20_2","unstructured":"Luke Geeson. 2024. [Armv7\/v8 Mixing Bug]: 64-bit Sequentially Consistent Load can be Reordered before Store of RMW when v7 and v8 Implementations are Mixed. https:\/\/gcc.gnu.org\/bugzilla\/show_bug.cgi?id=111416."},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Luke Geeson. 2024. Weak Memory Demands Model-based Compiler Testing. https:\/\/doi.org\/10.48550\/arXiv.2401.09474 10.48550\/arXiv.2401.09474 arXiv:2401.09474[cs.PL]","DOI":"10.48550\/arXiv.2401.09474"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Luke Geeson James Brotherston James Dijkstra Alastair F. Donaldson Lee Smith Tyler Sorensen and John Wickerson. 2024. Artifact for \u201cMix Testing: Specifying and Testing ABI Compatibility Of C\/C++ Atomics Implementations\u201d. https:\/\/doi.org\/10.5281\/zenodo.13625822 10.5281\/zenodo.13625822","DOI":"10.5281\/zenodo.13625822"},{"key":"e_1_3_1_23_2","unstructured":"Luke Geeson and Wilco Dijkstra. 2024. C\/C++ Atomics Application Binary Interface Standard for the Arm\u00ae 64-bit Architecture. https:\/\/github.com\/ARM-software\/abi-aa\/releases\/tag\/2024Q3."},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","unstructured":"Luke Geeson and Lee Smith. 2024. Compiler Testing with Relaxed Memory Models. In 2024 IEEE\/ACM International Symposium on Code Generation and Optimization (CGO). 334\u2013348. https:\/\/doi.org\/10.1109\/CGO57630.2024.10444836 10.1109\/CGO57630.2024.10444836","DOI":"10.1109\/CGO57630.2024.10444836"},{"key":"e_1_3_1_25_2","unstructured":"Open ISO-C-Std. 2022. ISO\/IEC 9899:201x. https:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n2912.pdf."},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","unstructured":"Ori Lahav Viktor Vafeiadis Jeehoon Kang Chung-Kil Hur and Derek Dreyer. 2017. Repairing Sequential Consistency in C\/C++11 (PLDI 2017). ACM New York NY USA 618\u2013632. https:\/\/doi.org\/10.1145\/3062341.3062352 10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594334"},{"key":"e_1_3_1_29_2","unstructured":"Sung-Hwan Lee. 2023. A miscompilation bug in LICMPass (concurrency). https:\/\/github.com\/llvm\/llvm-project\/issues\/64188."},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_31_2","unstructured":"LLVM-Phabricator. 2023. [AArch64] Codegen for FEAT_LRCPC3. https:\/\/reviews.llvm.org\/D141429#inline-1378324."},{"key":"e_1_3_1_32_2","unstructured":"LLVM-Phabricator. 2023. [WoA] Use fences for sequentially consistent stores\/writes. https:\/\/reviews.llvm.org\/D141748."},{"key":"e_1_3_1_33_2","unstructured":"Arm Ltd. 2022. AArch32 Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/aarch32.cat."},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/4372.4375"},{"key":"e_1_3_1_35_2","unstructured":"Luc Maranget. 2022. RISC-V Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/riscv.cat."},{"key":"e_1_3_1_36_2","unstructured":"Luc Maranget and Jade Alglave. 2022. ARM Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/arm.cat."},{"key":"e_1_3_1_37_2","unstructured":"Luc Maranget and Jade Alglave. 2022. IBM PowerPC Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/ppc.cat."},{"key":"e_1_3_1_38_2","unstructured":"Luc Maranget and Jade Alglave. 2023. MIPS Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/mips.cat."},{"key":"e_1_3_1_39_2","unstructured":"Luc Maranget and Jade Alglave. 2023. x86-64 Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/x86tso-mixed.cat."},{"key":"e_1_3_1_40_2","unstructured":"Microsoft. 2024. ELF x86-64-ABI psABI. https:\/\/gitlab.com\/x86-psABIs\/x86-64-ABI. Accessed: 2024-02-07."},{"key":"e_1_3_1_41_2","unstructured":"Microsoft. 2024. Overview of x64 ABI conventions. https:\/\/learn.microsoft.com\/en-us\/cpp\/build\/x64-software-conventions?view=msvc-170. Accessed: 2024-02-07."},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Robin Morisset Pankaj Pawan and Francesco Zappa Nardelli. 2013. Compiler Testing via a Theory of Sound Opti-misations in the C11\/C++11 Memory Model. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (Seattle Washington USA) (PLDI \u201813). ACM New York NY USA 187\u2013196. https:\/\/doi.org\/10.1145\/2491956.2491967 10.1145\/2491956.2491967","DOI":"10.1145\/2491956.2491967"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_8"},{"key":"e_1_3_1_44_2","unstructured":"programmerjake. 2023. x86-32 -mno-x87 64-bit atomic load miscompilation. https:\/\/github.com\/llvm\/llvm-project\/issues\/64969."},{"key":"e_1_3_1_45_2","unstructured":"Mono Project. 2024. The Mono Project atomic source code. https:\/\/github.com\/mono\/mono\/blob\/44e6226c31d8ffcae58f81350d71a728edecfe22\/mono\/utils\/atomic.h#L209. Accessed: 2024-02-29."},{"key":"e_1_3_1_46_2","unstructured":"Peter Sewell and Jaroslav Sevcik. 2014. C\/C++11 mappings to processors. https:\/\/www.cl.cam.ac.uk\/~pes20\/cpp\/cpp0xmappings.html."},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","unstructured":"Ole Tange. 2023. GNU Parallel 20230222. https:\/\/doi.org\/10.5281\/zenodo.7668338 10.5281\/zenodo.7668338 GNU Parallel is a general parallelizer to run multiple serial command line programs in parallel without changing them..","DOI":"10.5281\/zenodo.7668338"},{"key":"e_1_3_1_48_2","unstructured":"Kyrylo Tkachov. 2024. Enabling the LDAPR instructions for C\/C++ compilers. https:\/\/community.arm.com\/arm-community-blogs\/b\/tools-software-ides-blog\/posts\/enabling-rcpc-in-gcc-and-llvm."},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993534"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","unstructured":"John Wickerson Mark Batty Tyler Sorensen and George A. Constantinides. 2017. Automatically Comparing Memory Consistency Models (POPL 2017). ACM New York NY USA 190\u2013204. https:\/\/doi.org\/10.1145\/3009837.3009838 10.1145\/3009837.3009838","DOI":"10.1145\/3009837.3009838"},{"key":"e_1_3_1_52_2","unstructured":"Wikipedia. 2024. Internal Compiler Errors. https:\/\/en.wikipedia.org\/wiki\/Compilation_error#Internal_Compiler_Errors."},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3460319.3469079"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689727","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689727","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:05:02Z","timestamp":1770195902000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689727"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":53,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689727"],"URL":"https:\/\/doi.org\/10.1145\/3689727","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}