{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T01:47:23Z","timestamp":1768873643859,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":68,"publisher":"ACM","funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/Z000580\/1"],"award-info":[{"award-number":["EP\/Z000580\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002739","name":"Aarhus Universitets Forskningsfond","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002739","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["789108,101189371"],"award-info":[{"award-number":["789108,101189371"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"publisher","award":["EP\/Y035976\/1"],"award-info":[{"award-number":["EP\/Y035976\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"publisher","award":["qbs4safety"],"award-info":[{"award-number":["qbs4safety"]}],"id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006041","name":"Innovate UK","doi-asserted-by":"publisher","award":["105694"],"award-info":[{"award-number":["105694"]}],"id":[{"id":"10.13039\/501100006041","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,6,21]]},"DOI":"10.1145\/3695053.3731102","type":"proceedings-article","created":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T16:46:17Z","timestamp":1750437977000},"page":"211-224","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Precise exceptions in relaxed architectures"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-8431-9577","authenticated-orcid":false,"given":"Ben","family":"Simner","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2910-0764","authenticated-orcid":false,"given":"Alasdair","family":"Armstrong","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9607-8942","authenticated-orcid":false,"given":"Thomas","family":"Bauereiss","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6941-5034","authenticated-orcid":false,"given":"Brian","family":"Campbell","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2071-0929","authenticated-orcid":false,"given":"Ohad","family":"Kammar","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4442-6543","authenticated-orcid":false,"given":"Jean","family":"Pichon-Pharabod","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9352-1013","authenticated-orcid":false,"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2025,6,20]]},"reference":[{"key":"e_1_3_3_1_2_2","doi-asserted-by":"publisher","unstructured":"A. Adir H. Attiya and G. Shurek. 2003. Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture. IEEE Trans. Parallel Distrib. Syst. 14 5 (2003) 502\u2013515. 10.1109\/TPDS.2003.1199067","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"e_1_3_3_1_3_2","unstructured":"Jade Alglave. 2010. A Shared Memory Poetics. Ph.\u00a0D. Dissertation. Universit\u00e9 Paris 7 \u2013 Denis Diderot."},{"key":"e_1_3_3_1_4_2","doi-asserted-by":"publisher","unstructured":"Jade Alglave Will Deacon Richard Grisenthwaite Antoine Hacquard and Luc Maranget. 2021. Armed Cats: Formal Concurrency Modelling at Arm. ACM Trans. Program. Lang. Syst. 43 2 (2021) 8:1\u20138:54. 10.1145\/3458926","DOI":"10.1145\/3458926"},{"key":"e_1_3_3_1_5_2","doi-asserted-by":"crossref","unstructured":"Jade Alglave Richard Grisenthwaite Artem Khyzha Luc Maranget and Nikos Nikoleris. 2024. Puss In Boots: on formalising Arm\u2019s Virtual Memory System Architecture (extended version). (May 2024). https:\/\/inria.hal.science\/hal-04567296 working paper or preprint.","DOI":"10.1109\/MM.2024.3422668"},{"key":"e_1_3_3_1_6_2","unstructured":"Jade Alglave and Luc Maranget. [n. d.]. The herdtools7 tool suite. diy.inria.fr https:\/\/github.com\/herd\/herdtools7\/. Accessed 2023-08-30."},{"key":"e_1_3_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177156"},{"key":"e_1_3_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_3_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-95"},{"key":"e_1_3_3_1_10_2","doi-asserted-by":"publisher","unstructured":"Jade Alglave Luc Maranget and Michael Tautschnig. 2014. Herding Cats: Modelling Simulation Testing and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. 36 2 (2014) 7:1\u20137:74. 10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"e_1_3_3_1_11_2","unstructured":"Arm. 2024. Arm Architecture Reference Manual: for A-profile architecture. https:\/\/developer.arm.com\/documentation\/ddi0487\/latest. Accessed 2024-05-11. Issue K.a. 14777 pages.."},{"key":"e_1_3_3_1_12_2","volume-title":"Arm Generic Interrupt Controller Architecture Specification, GIC architecture version 3 and version 4","year":"2024","unstructured":"Arm. 2024. Arm Generic Interrupt Controller Architecture Specification, GIC architecture version 3 and version 4. Technical Report. Arm. IHI 0069H.b (ID041224)."},{"key":"e_1_3_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_14"},{"key":"e_1_3_3_1_15_2","doi-asserted-by":"publisher","unstructured":"Ellen Arvidsson Elias Castegren Sylvan Clebsch Sophia Drossopoulou James Noble Matthew\u00a0J. Parkinson and Tobias Wrigstad. 2023. Reference Capabilities for Flexible Memory Management. Proc. ACM Program. Lang. 7 OOPSLA2 (2023) 1363\u20131393. 10.1145\/3622846","DOI":"10.1145\/3622846"},{"key":"e_1_3_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_3_3_1_17_2","unstructured":"Mark\u00a0John Batty. 2015. The C11 and C++11 concurrency model. Ph.\u00a0D. Dissertation. University of Cambridge UK. https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.708458"},{"key":"e_1_3_3_1_18_2","unstructured":"Thomas Bauereiss Brian Campbell Alasdair Armstrong Alastair Reid Kathryn\u00a0E. Gray Anthony Fox Peter Sewell and Arm Limited. 2024. Sail Armv9.4-A instruction-set architecture (ISA) model. https:\/\/github.com\/rems-project\/sail-arm. Accessed 2024-05-11.."},{"key":"e_1_3_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-21821-17"},{"key":"e_1_3_3_1_20_2","unstructured":"Soham Chakraborty. 2019. Correct Compilation of Relaxed Memory Concurrency. Ph.\u00a0D. Dissertation. Kaiserslautern University of Technology Germany. https:\/\/kluedo.ub.rptu.de\/frontdoor\/index\/index\/docId\/5697"},{"key":"e_1_3_3_1_21_2","doi-asserted-by":"crossref","unstructured":"Luke Cheeseman Matthew\u00a0J. Parkinson Sylvan Clebsch Marios Kogias Sophia Drossopoulou David Chisnall Tobias Wrigstad and Paul Li\u00e9tar. 2023. When Concurrency Matters: Behaviour-Oriented Concurrency. Proc. ACM Program. Lang. 7 OOPSLA2 (October 2023). https:\/\/www.microsoft.com\/en-us\/research\/publication\/when-concurrency-matters-behaviour-oriented-concurrency\/","DOI":"10.1145\/3622852"},{"key":"e_1_3_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.5555\/129082"},{"key":"e_1_3_3_1_23_2","unstructured":"Mingyao\u00a0Yang Dave\u00a0Dice Hui\u00a0Huang. 2001. Asymmetric Dekker Synchronization. http:\/\/web.archive.org\/web\/20070214114205http:\/\/blogs.sun.com\/dave\/resource\/Asymmetric-Dekker-Synchronization.txt"},{"key":"e_1_3_3_1_24_2","unstructured":"Hern\u00e1n\u00a0Ponce de Le\u00f3n and Johannes Kinder. 2021. Cats vs. Spectre: An Axiomatic Approach to Modeling Speculative Execution Attacks. CoRR abs\/2108.13818 (2021). arXiv:https:\/\/arXiv.org\/abs\/2108.13818https:\/\/arxiv.org\/abs\/2108.13818"},{"key":"e_1_3_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833774"},{"key":"e_1_3_3_1_26_2","unstructured":"Will Deacon Jade Alglave Nikos Nikoleris and Artem Khyzha. 2023. The ARMv8 Application Level Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/aarch64.cat (accessed 2019-07-01). Accessed 2024-11-19."},{"key":"e_1_3_3_1_27_2","unstructured":"Dave Dice. 2006. Biased Locking in Hotspot. Oracle Blog Wayback Machine. http:\/\/web.archive.org\/web\/20150320095550\/https:\/\/blogs.oracle.com\/dave\/entry\/biased_locking_in_hotspot"},{"key":"e_1_3_3_1_28_2","unstructured":"David Dice Mark\u00a0S. Moir and William N.\u00a0Scherer III. 2010. United States Patent US 7814488B1 Quickly Reacquirable Locks. United Statess Patent Office."},{"key":"e_1_3_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_3_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009839"},{"key":"e_1_3_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/238171"},{"key":"e_1_3_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325102"},{"key":"e_1_3_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_3_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3579371.3589087"},{"key":"e_1_3_3_1_35_2","volume-title":"Computer Architecture: A Quantitative Approach (5 ed.)","author":"Hennessy John\u00a0L.","year":"2012","unstructured":"John\u00a0L. Hennessy and David\u00a0A. Patterson. 2012. Computer Architecture: A Quantitative Approach (5 ed.). Morgan Kaufmann, Amsterdam."},{"key":"e_1_3_3_1_36_2","unstructured":"Naorin Hossain Caroline Trippel and Margaret Martonosi. 2020. TransForm: Formally Specifying Transistency Models and Synthesizing Enhanced Litmus Tests. CoRR abs\/2008.03578 (2020). arXiv:https:\/\/arXiv.org\/abs\/2008.03578https:\/\/arxiv.org\/abs\/2008.03578"},{"key":"e_1_3_3_1_37_2","unstructured":"Luc\u00a0Maranget. 2024. Personal communication."},{"key":"e_1_3_3_1_38_2","unstructured":"Intel. 2002. A Formal Specification of Intel Itanium Processor Family Memory Ordering. developer.intel.com\/design\/itanium\/downloads\/251429.htm."},{"key":"e_1_3_3_1_39_2","doi-asserted-by":"publisher","unstructured":"Radha Jagadeesan Alan Jeffrey and James Riely. 2020. Pomsets with preconditions: a simple model of relaxed memory. Proc. ACM Program. Lang. 4 OOPSLA (2020) 194:1\u2013194:30. 10.1145\/3428262","DOI":"10.1145\/3428262"},{"key":"e_1_3_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_3_1_41_2","unstructured":"Kiyokuni Kawachiya. 2005. Java Locks: Analysis and Acceleration. Ph.\u00a0D. Dissertation. Keio University."},{"key":"e_1_3_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/582419.582433"},{"key":"e_1_3_3_1_43_2","doi-asserted-by":"publisher","unstructured":"Michalis Kokologiannakis Ori Lahav Konstantinos Sagonas and Viktor Vafeiadis. 2017. Effective stateless model checking for C\/C++ concurrency. Proc. ACM Program. Lang. 2 POPL Article 17 (dec 2017) 32\u00a0pages. 10.1145\/3158105","DOI":"10.1145\/3158105"},{"key":"e_1_3_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-820"},{"key":"e_1_3_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2015.0360"},{"key":"e_1_3_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_3_1_48_2","doi-asserted-by":"publisher","unstructured":"Lihao Liang Tom Melham Daniel Kroening Peter Schrammel and Michael Tautschnig. 2017. Effective Verification for Low-Level Software with Competing Interrupts. ACM Transactions on Embedded Computing Systems 17 2 (December 2017) 36:1\u201336:26. 10.1145\/3147432","DOI":"10.1145\/3147432"},{"key":"e_1_3_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872399"},{"key":"e_1_3_3_1_50_2","unstructured":"Patricio\u00a0Chilano Mateo. 2021. JEP 374: Deprecate and Disable Biased Locking. JDK Enhancement Proposal. https:\/\/openjdk.org\/jeps\/374"},{"key":"e_1_3_3_1_51_2","volume-title":"Is Parallel Programming Hard, And, If So, What Can You Do About It?","author":"McKenney Paul\u00a0E.","year":"2023","unstructured":"Paul\u00a0E. McKenney. 2023. Is Parallel Programming Hard, And, If So, What Can You Do About It?https:\/\/mirrors.edge.kernel.org\/pub\/linux\/kernel\/people\/paulmck\/perfbook\/perfbook.html"},{"key":"e_1_3_3_1_52_2","unstructured":"Paul\u00a0E. McKenney. 2024. RCU Concepts. https:\/\/www.kernel.org\/doc\/Documentation\/RCU\/rcu.txt Accessed 2024-11-19."},{"key":"e_1_3_3_1_53_2","first-page":"509","volume-title":"Parallel and Distributed Computing and Systems","author":"McKenney Paul\u00a0E","year":"1998","unstructured":"Paul\u00a0E McKenney and John\u00a0D Slingwine. 1998. Read-copy update: Using execution history to solve concurrency problems. In Parallel and Distributed Computing and Systems, Vol.\u00a0509518. 509\u2013518."},{"key":"e_1_3_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3470496.3527412"},{"key":"e_1_3_3_1_55_2","unstructured":"Matthew\u00a0J. Parkinson. 2024. Some things I wish I hadn\u2019t seen. presented at The Future of Weak Memory 2024."},{"key":"e_1_3_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_3_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/304065.304106"},{"key":"e_1_3_3_1_58_2","unstructured":"Christopher Pulte. 2018. The Semantics of Multicopy Atomic ARMv8 and RISC-V. Ph.\u00a0D. Dissertation. University of Cambridge. https:\/\/www.repository.cam.ac.uk\/handle\/1810\/292229."},{"key":"e_1_3_3_1_59_2","doi-asserted-by":"publisher","unstructured":"Christopher Pulte Shaked Flur Will Deacon Jon French Susmit Sarkar and Peter Sewell. 2018. Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. Proc. ACM Program. Lang. 2 POPL (2018) 19:1\u201319:29. 10.1145\/3158107","DOI":"10.1145\/3158107"},{"key":"e_1_3_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/1167473.1167496"},{"key":"e_1_3_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_3_3_1_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_3_1_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_3_3_1_64_2","unstructured":"Peter Sewell Christopher Pulte Shaked Flur Mark Batty Luc Maranget and Alasdair Armstrong. 2022. Multicore Semantics: Making Sense of Relaxed Memory (MPhil slides). https:\/\/www.cl.cam.ac.uk\/\u00a0pes20\/slides-acs-2022.pdf"},{"key":"e_1_3_3_1_65_2","doi-asserted-by":"publisher","unstructured":"P. Sewell S. Sarkar S. Owens F. Zappa\u00a0Nardelli and M.\u00a0O. Myreen. 2010. x86-TSO: A Rigorous and Usable Programmer\u2019s Model for x86 Multiprocessors. Commun. ACM 53 7 (July 2010) 89\u201397. 10.1145\/1785414.1785443","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_3_1_66_2","doi-asserted-by":"publisher","unstructured":"Ben Simner Alasdair Armstrong Thomas Bauereiss Brian Campbell Ohad Kammar Jean Pichon-Pharabod and Peter Sewell. 2024. Relaxed exception semantics for Arm-A (extended version). CoRR abs\/2412.15140 (2024). 10.48550\/ARXIV.2412.15140 arXiv:https:\/\/arXiv.org\/abs\/2412.15140","DOI":"10.48550\/ARXIV.2412.15140"},{"key":"e_1_3_3_1_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_6"},{"key":"e_1_3_3_1_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_23"},{"key":"e_1_3_3_1_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3604-82"}],"event":{"name":"ISCA '25: Proceedings of the 52nd Annual International Symposium on Computer Architecture","location":"Tokyo Japan","acronym":"SIGARCH '25","sponsor":["SIGARCH ACM Special Interest Group on Computer Architecture"]},"container-title":["Proceedings of the 52nd Annual International Symposium on Computer Architecture"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3695053.3731102","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T11:02:42Z","timestamp":1750503762000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3695053.3731102"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,20]]},"references-count":68,"alternative-id":["10.1145\/3695053.3731102","10.1145\/3695053"],"URL":"https:\/\/doi.org\/10.1145\/3695053.3731102","relation":{},"subject":[],"published":{"date-parts":[[2025,6,20]]},"assertion":[{"value":"2025-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}