{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:58Z","timestamp":1776305338553,"version":"3.50.1"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:p>We propose an axiomatic generic framework for modelling weak memory. We show how to instantiate this framework for Sequential Consistency (SC), Total Store Order (TSO), C++ restricted to release-acquire atomics, and Power. For Power, we compare our model to a preceding operational model in which we found a flaw. To do so, we define an operational model that we show equivalent to our axiomatic model.<\/jats:p>\n          <jats:p>We also propose a model for ARM. Our testing on this architecture revealed a behaviour later acknowledged as a bug by ARM, and more recently, 31 additional anomalies.<\/jats:p>\n          <jats:p>We offer a new simulation tool, called herd, which allows the user to specify the model of his choice in a concise way. Given a specification of a model, the tool becomes a simulator for that model. The tool relies on an axiomatic description; this choice allows us to outperform all previous simulation tools. Additionally, we confirm that verification time is vastly improved, in the case of bounded model checking.<\/jats:p>\n          <jats:p>Finally, we put our models in perspective, in the light of empirical data obtained by analysing the C and C++ code of a Debian Linux distribution. We present our new analysis tool, called mole, which explores a piece of code to find the weak memory idioms that it uses.<\/jats:p>","DOI":"10.1145\/2627752","type":"journal-article","created":{"date-parts":[[2014,7,11]],"date-time":"2014-07-11T12:09:41Z","timestamp":1405080581000},"page":"1-74","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":276,"title":["Herding Cats"],"prefix":"10.1145","volume":"36","author":[{"given":"Jade","family":"Alglave","sequence":"first","affiliation":[{"name":"University College London, Gower Street, London, United Kingdom"}]},{"given":"Luc","family":"Maranget","sequence":"additional","affiliation":[{"name":"INRIA, France"}]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[{"name":"Queen Mary University of London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2014,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_15"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_37"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1787234.1787255"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0161-5"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25318-8_21"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_28"},{"key":"e_1_2_1_11_1","volume-title":"Partial orders for efficient bounded model checking of concurrent software","author":"Alglave Jade","unstructured":"Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013b. Partial orders for efficient bounded model checking of concurrent software. In Proceedings of CAV. Springer-Verlag, Berlin, Heidelberg, 141--157."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032311"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987389.1987395"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0135-z"},{"key":"e_1_2_1_16_1","volume-title":"ARM Architecture Reference Manual: ARMv7-A and ARMv7-R Edition","author":"Ltd ARM","unstructured":"ARM Ltd. 2010. ARM Architecture Reference Manual: ARMv7-A and ARMv7-R Edition. ARM Ltd."},{"key":"e_1_2_1_17_1","volume-title":"Read-after-Read Hazards","author":"Ltd ARM","unstructured":"ARM Ltd. 2011. Cortex-A9 MPCore, Programmer Advice Notice, Read-after-Read Hazards. ARM Ltd."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2006.26"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706303"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_2"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032314"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429099"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/993954"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2076450.2076465"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_29"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/2027223.2027267"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480930"},{"key":"e_1_2_1_30_1","volume-title":"Serpette","author":"Boudol G\u00e9rard","year":"2012","unstructured":"G\u00e9rard Boudol, Gustavo Petri, and Bernard P. Serpette. 2012. Relaxed operational semantics of concurrent programming languages. In Proceedings of EXPRESS\/SOS. 19--33."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the Workshop on Exploiting Concurrency Efficiently and Correctly (EC)2.","author":"Burckhardt Sebastian","year":"2008","unstructured":"Sebastian Burckhardt and Madan Musuvathi. 2008. Memory Model Safety of Programs. In Proceedings of the Workshop on Exploiting Concurrency Efficiently and Correctly (EC)2."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762206"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353522.1353528"},{"key":"e_1_2_1_37_1","volume-title":"A tool for checking ANSI-C programs","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In Proceedings of TACAS. Springer-Verlag, Berlin, Heidelberg, 168--176."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/129082"},{"key":"e_1_2_1_39_1","volume-title":"Alpha Architecture Reference Manual","author":"Compaq Computer Corp. 2002.","unstructured":"Compaq Computer Corp. 2002. Alpha Architecture Reference Manual. Compaq Computer Corp."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325102"},{"key":"e_1_2_1_42_1","volume-title":"QB or not QB: An efficient execution verification tool for memory orderings","author":"Gopalakrishnan Ganesh","unstructured":"Ganesh Gopalakrishnan, Yue Yang, and Hemanthkumar Sivaraj. 2004. QB or not QB: An efficient execution verification tool for memory orderings. In Proceedings of CAV. Springer-Verlag, Berlin, Heidelberg, 401--413."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/45.1.27"},{"key":"e_1_2_1_44_1","volume-title":"ARM Barrier Litmus Tests and Cookbook","author":"Grisenthwaite Richard","unstructured":"Richard Grisenthwaite. 2009. ARM Barrier Litmus Tests and Cookbook. ARM Ltd."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/998680.1006710"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264034"},{"key":"e_1_2_1_47_1","volume-title":"Linux Kernel Memory Barriers, 2013","author":"Howells David","year":"2014","unstructured":"David Howells and Paul E. MacKenney. 2013. Linux Kernel Memory Barriers, 2013 version. Retrieved May 29, 2014, from https:\/\/www.kernel.org\/doc\/Documentation\/memory-barriers.txt."},{"key":"e_1_2_1_48_1","volume-title":"Power ISA Version 2.06","author":"IBM Corp. 2009.","unstructured":"IBM Corp. 2009. Power ISA Version 2.06. IBM Corp."},{"key":"e_1_2_1_49_1","volume-title":"A Formal Specification of Intel Itanium Processor Family Memory Ordering","author":"Intel Corp. 2002.","unstructured":"Intel Corp. 2002. A Formal Specification of Intel Itanium Processor Family Memory Ordering. Intel Corp."},{"key":"e_1_2_1_50_1","volume-title":"Intel 64 and IA-32 Architectures Software Developer\u2019s Manual","author":"Intel Corp. 2009.","unstructured":"Intel Corp. 2009. Intel 64 and IA-32 Architectures Software Developer\u2019s Manual. Intel Corp."},{"key":"e_1_2_1_51_1","unstructured":"ISO. 2011. ISO\/IEC 9899:2011 Information technology \u2014 Programming languages \u2014 C. International Organization for Standardization."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770386"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.5555\/1998496.1998518"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993521"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254115"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_26"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_2_1_62_1","volume-title":"McKenney and Jonathan Walpole","author":"Paul","year":"2007","unstructured":"Paul E. McKenney and Jonathan Walpole. 2007. What is RCU, fundamentally&quest; Retrieved May 29, 2014, from http:\/\/lwn.net\/Articles\/262464\/."},{"key":"e_1_2_1_63_1","volume-title":"Tutorial and Workshop on Formal Specification and Verification Methods for Shared Memory Systems.","author":"Neiger Gil","year":"2000","unstructured":"Gil Neiger. 2000. A taxonomy of multiprocessor memory-ordering models. In Tutorial and Workshop on Formal Specification and Verification Methods for Shared Memory Systems."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.5555\/2033939.2033970"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.5555\/121026"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.5555\/174556"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017460.1017464"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1137\/0202017"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.461.0005"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806635"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2004.1302944"},{"key":"e_1_2_1_77_1","volume-title":"Proceedings of the Workshop on Exploiting Concurrency Efficiently and Correctly (EC)2.","author":"Nardelli Francesco Zappa","year":"2009","unstructured":"Francesco Zappa Nardelli, Peter Sewell, Jaroslav Sevcik, Susmit Sarkar, Scott Owens, Luc Maranget, Mark Batty, and Jade Alglave. 2009. Relaxed memory models must be rigorous. In Proceedings of the Workshop on Exploiting Concurrency Efficiently and Correctly (EC)2."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2627752","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2627752","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:01:36Z","timestamp":1750230096000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2627752"}},"subtitle":["Modelling, Simulation, Testing, and Data Mining for Weak Memory"],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":73,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1145\/2627752"],"URL":"https:\/\/doi.org\/10.1145\/2627752","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7]]},"assertion":[{"value":"2013-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}