{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:45:11Z","timestamp":1773193511180,"version":"3.50.1"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2021,6,30]],"date-time":"2021-06-30T00:00:00Z","timestamp":1625011200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2021,6,30]]},"abstract":"<jats:p>We report on the process for formal concurrency modelling at Arm. An initial formal consistency model of the Arm achitecture, written in the cat language, was published and upstreamed to the herd+diy tool suite in 2017. Since then, we have extended the original model with extra features, for example, mixed-size accesses, and produced two provably equivalent alternative formulations.<\/jats:p>\n          <jats:p>In this article, we present a comprehensive review of work done at Arm on the consistency model. Along the way, we also show that our principle for handling mixed-size accesses applies to x86: We confirm this via vast experimental campaigns. We also show that our alternative formulations are applicable to any model phrased in a style similar to the one chosen by Arm.<\/jats:p>","DOI":"10.1145\/3458926","type":"journal-article","created":{"date-parts":[[2021,7,23]],"date-time":"2021-07-23T10:55:09Z","timestamp":1627037709000},"page":"1-54","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":35,"title":["Armed Cats"],"prefix":"10.1145","volume":"43","author":[{"given":"Jade","family":"Alglave","sequence":"first","affiliation":[{"name":"Arm Ltd and University College London"}]},{"given":"Will","family":"Deacon","sequence":"additional","affiliation":[{"name":"Arm Ltd"}]},{"given":"Richard","family":"Grisenthwaite","sequence":"additional","affiliation":[{"name":"Arm Ltd"}]},{"given":"Antoine","family":"Hacquard","sequence":"additional","affiliation":[{"name":"EPITA Research and Development Laboratory"}]},{"given":"Luc","family":"Maranget","sequence":"additional","affiliation":[{"name":"INRIA"}]}],"member":"320","published-online":{"date-parts":[[2021,7,23]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Arm Ltd. 2020. Arm released cat models. https:\/\/github.com\/herd\/herdtools7\/tree\/master\/herd\/libdir\/arm-models."},{"key":"e_1_2_1_2_1","unstructured":"Richard Gooch and Pekka Enberg. 2005. Linux Kernel Virtual File System (VFS). https:\/\/www.kernel.org\/doc\/html\/latest\/filesystems\/vfs.html"},{"key":"e_1_2_1_3_1","unstructured":"RISC-V. 2019. The RISC-V Instruction Set Manual Volume I: Unprivileged ISA. https:\/\/content.riscv.org\/wp-content\/uploads\/2019\/12\/riscv-spec-20191213.pdf."},{"key":"e_1_2_1_4_1","unstructured":"Arm Ltd. 2020. Arm Memory Model. https:\/\/developer.arm.com\/architectures\/cpu-architecture\/a-profile\/memory-model-tool."},{"key":"e_1_2_1_5_1","unstructured":"Arm Ltd. 2020. Armv8 for Armv8-A architecture profile. In Arm Architecture Reference Manual Vol. ARM DDI 0487F.c. https:\/\/developer.arm.com\/docs\/ddi0487\/latest\/arm-architecture-reference-manual-armv8-for-armv8-a-architecture-profile."},{"key":"e_1_2_1_6_1","unstructured":"Jade Alglave. 2019. Retrieved from https:\/\/github.com\/herd\/herdtools7\/commit\/95785c747750be4a3b64adfab9d5f5ee0ead8240."},{"key":"e_1_2_1_7_1","unstructured":"Jade Alglave. 2020. https:\/\/github.com\/herd\/herdtools7\/blob\/master\/herd\/libdir\/x86tso-mixed.cat."},{"key":"e_1_2_1_9_1","unstructured":"Jade Alglave. 2019. Retrieved from Adding mixed-size accesses to Arm formal memory model. https:\/\/github.com\/herd\/herdtools7\/commit\/95785c747750be4a3b64adfab9d5f5ee0ead8240#diff-cc249d0a9116e1ab890d8b52586bc702."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694391"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009883"},{"key":"e_1_2_1_12_1","unstructured":"Jade Alglave Patrick Cousot and Luc Maranget. 2016. Syntax and semantics of the weak consistency model specification language cat. CoRR abs\/1608.07531. Retrieved from http:\/\/arxiv.org\/abs\/1608.07531."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_2_1_14_1","unstructured":"Jade Alglave and Luc Maranget. 2010-present. The herd+diy toolsuite. Retrieved from http:\/\/diy.inria.fr."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 23rd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS\u201918)","author":"Alglave Jade","unstructured":"Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and Alan S. Stern. 2018. Frightening small children and disconcerting grown-ups: Concurrency in the linux kernel. In Proceedings of the 23rd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS\u201918), Xipeng Shen, James Tuck, Ricardo Bianchini, and Vivek Sarkar (Eds.). ACM, 405\u2013418."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Jade Alglave Luc Maranget Susmit Sarkar and Peter Sewell. 2011. Litmus: Running tests against hardware. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201911) Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS\u201911) Parosh Aziz Abdulla and K. Rustan M. Leino (Eds.) Lecture Notes in Computer Science Vol. 6605. Springer 41\u201344.","DOI":"10.1007\/978-3-642-19835-9_5"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0135-z"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353522.1353528"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192373"},{"key":"e_1_2_1_23_1","unstructured":"Will Deacon. 2017. Formal memory model for Armv8.0 application level. Retrieved from https:\/\/github.com\/herd\/herdtools7\/commit\/daa126680b6ecba97ba47b3e05bbaa51a89f27b7#diff-0461c726950c4454a08bd97fbfd49252."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009839"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264034"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338843"},{"key":"e_1_2_1_28_1","unstructured":"Antoine Hacquard Jade Alglave and Luc Maranget. [n.d.]. Mixed-size experiments on AArch64 and x86. Retrieved from http:\/\/diy.inria.fr\/mixed\/."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428262"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304043"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314624"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360561"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Ben Simner Shaked Flur Christopher Pulte Alasdair Armstrong Jean Pichon-Pharabod Luc Maranget and Peter Sewell. 2020. ARMv8-A system semantics: Instruction fetch in relaxed architectures (extended version). (2020).","DOI":"10.1007\/978-3-030-44914-8_23"},{"key":"e_1_2_1_42_1","unstructured":"Viktor Vafeiadis. 2021. Retrieved from https:\/\/github.com\/vafeiadis\/arm-model."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385973"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3458926","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3458926","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:55Z","timestamp":1750195495000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3458926"}},"subtitle":["Formal Concurrency Modelling at Arm"],"short-title":[],"issued":{"date-parts":[[2021,6,30]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,6,30]]}},"alternative-id":["10.1145\/3458926"],"URL":"https:\/\/doi.org\/10.1145\/3458926","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,30]]},"assertion":[{"value":"2020-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-07-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}