{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:57:09Z","timestamp":1774025829093,"version":"3.50.1"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>Very relaxed concurrency memory models, like those of the Arm-A, RISC-V, and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the 'current' state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next.<\/jats:p>\n          <jats:p>We present AxSL, a separation logic for the relaxed memory model of Arm-A, that captures the fine-grained reasoning underpinning the low-overhead synchronisation mechanisms used by high-performance systems code. In particular, AxSL allows transferring arbitrary resources using relaxed reads and writes when they induce inter-thread ordering. We mechanise AxSL in the Iris separation logic framework, illustrate it on key examples, and prove it sound with respect to the axiomatic memory model of Arm-A. Our approach is largely generic in the axiomatic model and in the instruction-set semantics, offering a potential way forward for compositional reasoning for other similar models, and for the combination of production concurrency models and full-scale ISAs.<\/jats:p>","DOI":"10.1145\/3632863","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"604-637","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9156-9240","authenticated-orcid":false,"given":"Angus","family":"Hammond","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9652-4869","authenticated-orcid":false,"given":"Zongyuan","family":"Liu","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-0005-7618","authenticated-orcid":false,"given":"Thibaut","family":"P\u00e9rami","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9352-1013","authenticated-orcid":false,"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4442-6543","authenticated-orcid":false,"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009883"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458926"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177156"},{"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\/2627752"},{"key":"e_1_2_1_6_1","unstructured":"2023. ARM Architecture Reference Manual (for A-profile architecture). ARM DDI 0487J.a (ID042523) https:\/\/developer.arm.com\/documentation\/ddi0487\/latest\/"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_14"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Mark Batty Kayvan Memarian Kyndylan Nienhuis Jean Pichon-Pharabod and Peter Sewell. 2015. The Problem of Programming Language Concurrency Semantics. In ESOP. 283\u2013307. https:\/\/doi.org\/10.1007\/978-3-662-46669-8_12 10.1007\/978-3-662-46669-8_12","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_1_11_1","first-page":"2011","article-title":"Programming Languages \u2014 C++., P. Becker (Ed.)","volume":"14882","year":"2011","unstructured":"2011. Programming Languages \u2014 C++., P. Becker (Ed.). ISO\/IEC 14882:2011. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2011\/n3242.pdf","journal-title":"ISO\/IEC"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_2_1_13_1","volume-title":"Parkinson","author":"Bornat Richard","year":"2015","unstructured":"Richard Bornat, Jade Alglave, and Matthew J. Parkinson. 2015. New Lace and Arsenic: adventures in weak memory with a program logic. CoRR, abs\/1512.01416 (2015), arXiv:1512.01416. arxiv:1512.01416"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290383"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523718"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676984"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_2_1_20_1","unstructured":"Will Deacon. 2016. The ARMv8 Application Level Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/aarch64.cat"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_1_23_1","volume-title":"Program Logic for Weak Memory Concurrency. Ph. D. Dissertation","author":"Doko Marko","unstructured":"Marko Doko. 2021. Program Logic for Weak Memory Concurrency. Ph. D. Dissertation. Kaiserslautern University of Technology, Germany. https:\/\/kluedo.ub.rptu.de\/frontdoor\/index\/index\/docId\/6679"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009839"},{"key":"e_1_2_1_29_1","volume-title":"Memory Consistency Models for Shared-Memory Multiprocessors. Ph. D. Dissertation","author":"Gharachorloo Kourosh","unstructured":"Kourosh Gharachorloo. 1995. Memory Consistency Models for Shared-Memory Multiprocessors. Ph. D. Dissertation. Stanford University."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Angus Hammond Zongyuan Liu Thibaut P\u00e9rami Peter Sewell Lars Birkedal and Jean Pichon-Pharabod. 2023. Research data for An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. https:\/\/github.com\/logsem\/AxSL","DOI":"10.1145\/3632863"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1189736.1189737"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934536"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPP.1993.15"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_25"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591279"},{"key":"e_1_2_1_45_1","volume-title":"Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR, abs\/1611.01507","author":"Manerkar Yatin A.","year":"2016","unstructured":"Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2016. Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR, abs\/1611.01507 (2016), arXiv:1611.01507. arxiv:1611.01507"},{"key":"e_1_2_1_46_1","unstructured":"Paul E. McKenney Ulrich Weigand Andrea Parri Boqun Feng and Alan Stern. 2020. Linux-Kernel Memory Model. ISO\/IEC JTC1 SC22 WG21 P0124R7. https:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2020\/p0124r7.html"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.1984.10017"},{"key":"e_1_2_1_48_1","volume-title":"Formal verification of machine-code programs. Ph. D. Dissertation","author":"Myreen Magnus O.","unstructured":"Magnus O. Myreen. 2009. Formal verification of machine-code programs. Ph. D. Dissertation. University of Cambridge."},{"key":"e_1_2_1_49_1","volume-title":"Gordon","author":"Myreen Magnus O.","year":"2007","unstructured":"Magnus O. Myreen, Anthony C. J. Fox, and Michael J. C. Gordon. 2007. Hoare Logic for ARM Machine Code. In Fundamentals of Software Engineering (FSEN), Farhad Arbab and Marjan Sirjani (Eds.). Springer, 272\u2013286."},{"key":"e_1_2_1_50_1","volume-title":"Gordon","author":"Myreen Magnus O.","year":"2007","unstructured":"Magnus O. Myreen and Michael J. C. Gordon. 2007. Hoare Logic for Realistically Modelled Machine Code. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Orna Grumberg and Michael Huth (Eds.). Springer, 568\u2013582."},{"key":"e_1_2_1_51_1","volume-title":"Formal Methods in Computer-Aided Design (FMCAD), Alessandro Cimatti and Robert B","author":"Myreen Magnus O.","unstructured":"Magnus O. Myreen, Michael J. C. Gordon, and Konrad Slind. 2008. Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. In Formal Methods in Computer-Aided Design (FMCAD), Alessandro Cimatti and Robert B. Jones (Eds.). IEEE, 1\u20138."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01966091"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.17863\/CAM.39379"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314624"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_6"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_23"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_13"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483560"},{"key":"e_1_2_1_71_1","volume-title":"Report of a Conference on High Speed Automatic Calculating Machines. Mathematical Laboratory","author":"Turing Alan M.","unstructured":"Alan M. Turing. 1949. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines. Mathematical Laboratory, Cambridge, UK, 67\u201369. https:\/\/turingarchive.kings.cam.ac.uk\/publications-lectures-and-talks-amtb\/amt-b-8"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_2_1_74_1","unstructured":"Andrew Waterman and Krste Asanovi\u0107. 2019. The RISC-V Instruction Set Manual Volume I: Unprivileged ISA Document Version 20191213. https:\/\/github.com\/riscv\/riscv-isa-manual\/releases\/download\/Ratified-IMAFDQC\/riscv-spec-20191213.pdf"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_12"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632863","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632863","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:02:57Z","timestamp":1751659377000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632863"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":75,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632863"],"URL":"https:\/\/doi.org\/10.1145\/3632863","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}