{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:28Z","timestamp":1780994488013,"version":"3.54.1"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/M027317\/1"],"award-info":[{"award-number":["EP\/M027317\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K008528\/1"],"award-info":[{"award-number":["EP\/K008528\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>\n            ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits. In particular, the model was originally\n            <jats:italic>non-multicopy-atomic<\/jats:italic>\n            : writes could become visible to some other threads before becoming visible to all \u2014 but this has not been exploited in production implementations, the corresponding potential hardware optimisations are thought to have insufficient benefits in the ARM context, and it gives rise to subtle complications when combined with other ARMv8 features. The ARMv8 architecture has therefore been revised: it now has a multicopy-atomic model. It has also been simplified in other respects, including more straightforward notions of dependency, and the architecture now includes a formal concurrency model.\n          <\/jats:p>\n          <jats:p>In this paper we detail these changes and discuss their motivation. We define two formal concurrency models: an operational one, simplifying the Flowing model of Flur et al., and the axiomatic model of the revised ARMv8 specification. The models were developed by an academic group and by ARM staff, respectively, and this extended collaboration partly motivated the above changes. We prove the equivalence of the two models. The operational model is integrated into an executable exploration tool with new web interface, demonstrated by exhaustively checking the possible behaviours of a loop-unrolled version of a Linux kernel lock implementation, a previously known bug due to unprevented speculation, and a fixed version.<\/jats:p>","DOI":"10.1145\/3158107","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":105,"title":["Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8"],"prefix":"10.1145","volume":"2","author":[{"given":"Christopher","family":"Pulte","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shaked","family":"Flur","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Will","family":"Deacon","sequence":"additional","affiliation":[{"name":"ARM, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jon","family":"French","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Susmit","family":"Sarkar","sequence":"additional","affiliation":[{"name":"University of St. Andrews, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_2_2_3_1","volume-title":"Proc. DAMP","author":"Alglave Jade","year":"2009"},{"key":"e_1_2_2_4_1","volume-title":"http:\/\/diy.inria.fr\/doc\/index.html . (April","author":"Alglave Jade","year":"2017"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_5"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_2_8_1","volume-title":"ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile)","author":"Ltd ARM"},{"key":"e_1_2_2_9_1","volume-title":"ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile)","author":"Ltd ARM"},{"key":"e_1_2_2_10_1","unstructured":"ARM Ltd. 2017. ARM Processor Cortex-A53 MPCore Product Revision r0 Software Developers Errata Notice. http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.epm048406\/Cortex_A53_MPCore_Software_Developers_Errata_ Notice.pdf . (May 2017).  ARM Ltd. 2017. ARM Processor Cortex-A53 MPCore Product Revision r0 Software Developers Errata Notice. http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.epm048406\/Cortex_A53_MPCore_Software_Developers_Errata_ Notice.pdf . (May 2017)."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1150019.1136489"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_2_14_1","first-page":"2011","article-title":"Programming Languages \u2014 C++","volume":"14882","author":"Ed Pete Becker","year":"2011","journal-title":"ISO\/IEC"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062353"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353522.1353528"},{"key":"e_1_2_2_18_1","volume-title":"Reasoning about parallel architectures","author":"Collier William W."},{"key":"e_1_2_2_19_1","volume-title":"Technical Report RC18638. IBM.","author":"Corella F.","year":"1993"},{"key":"e_1_2_2_20_1","unstructured":"Mike Daines. 2017. Viz.js a hack to put Graphviz on the web. https:\/\/github.com\/mdaines\/viz.js\/ . (2017).  Mike Daines. 2017. Viz.js a hack to put Graphviz on the web. https:\/\/github.com\/mdaines\/viz.js\/ . (2017)."},{"key":"e_1_2_2_21_1","unstructured":"Will Deacon. 2015. Linux commit \u2018arm64: spinlock: serialise spin_unlock_wait against concurrent lockers\u2019. https:\/\/git.kernel. org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=d86b8da04dfa . (2015).  Will Deacon. 2015. Linux commit \u2018arm64: spinlock: serialise spin_unlock_wait against concurrent lockers\u2019. https:\/\/git.kernel. org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=d86b8da04dfa . (2015)."},{"key":"e_1_2_2_22_1","unstructured":"Will Deacon. 2016. The ARMv8 Application Level Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/ libdir\/aarch64.cat . (2016).  Will Deacon. 2016. The ARMv8 Application Level Memory Model. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/ libdir\/aarch64.cat . (2016)."},{"key":"e_1_2_2_23_1","volume-title":"The Flowing and POP Models (supplementary material for Modelling the ARMv8 Architecture","author":"Flur Shaked","year":"2016"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1002\/1097-024X(200009)30:11%3C1203::AID-SPE338%3E3.0.CO;2-N"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830775"},{"key":"e_1_2_2_29_1","unstructured":"David Howells Paul E. McKenney Will Deacon and Peter Zijlstra. 2016. Documentation\/memory-barriers.txt. https: \/\/www.kernel.org\/doc\/Documentation\/memory- barriers.txt . (2016).  David Howells Paul E. McKenney Will Deacon and Peter Zijlstra. 2016. Documentation\/memory-barriers.txt. https: \/\/www.kernel.org\/doc\/Documentation\/memory- barriers.txt . (2016)."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_2_2_31_1","unstructured":"Linux contributors. 2014. Documentation\/locking\/spinlocks.txt. https:\/\/www.kernel.org\/doc\/Documentation\/locking\/ spinlocks.txt . (2014).  Linux contributors. 2014. Documentation\/locking\/spinlocks.txt. https:\/\/www.kernel.org\/doc\/Documentation\/locking\/ spinlocks.txt . (2014)."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037723"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_26"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830772.2830782"},{"key":"e_1_2_2_36_1","unstructured":"Luc Maranget Susmit Sarkar and Peter Sewell. 2012. A Tutorial Introduction to the ARM and POWER Relaxed Memory Models. Draft available from http:\/\/www.cl.cam.ac.uk\/~pes20\/ppc- supplemental\/test7.pdf . (2012).  Luc Maranget Susmit Sarkar and Peter Sewell. 2012. A Tutorial Introduction to the ARM and POWER Relaxed Memory Models. Draft available from http:\/\/www.cl.cam.ac.uk\/~pes20\/ppc- supplemental\/test7.pdf . (2012)."},{"key":"e_1_2_2_37_1","volume-title":"Remove spin_unlock_wait(). (Jun","author":"McKenney Paul E","year":"2017"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480929"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.2187"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048147.2048224"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158107","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158107","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158107"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":45,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158107"],"URL":"https:\/\/doi.org\/10.1145\/3158107","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}