{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:06Z","timestamp":1775873406939,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T00:00:00Z","timestamp":1232409600000},"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":[],"published-print":{"date-parts":[[2009,1,20]]},"DOI":"10.1145\/1481839.1481842","type":"proceedings-article","created":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T14:41:38Z","timestamp":1232462498000},"page":"13-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":65,"title":["The semantics of power and ARM multiprocessor machine code"],"prefix":"10.1145","author":[{"given":"Jade","family":"Alglave","sequence":"first","affiliation":[{"name":"INRIA, Rocquencourt, France"}]},{"given":"Anthony","family":"Fox","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"given":"Samin","family":"Ishtiaq","sequence":"additional","affiliation":[{"name":"Microsoft Research Cambridge, Cambridge, United Kingdom"}]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"given":"Susmit","family":"Sarkar","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"given":"Peter","family":"Sewell","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"given":"Francesco Zappa","family":"Nardelli","sequence":"additional","affiliation":[{"name":"INRIA, Rocquencourt, France"}]}],"member":"320","published-online":{"date-parts":[[2009,1,20]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_3_2_1_3_1","unstructured":"ARM. ARM Architecture Reference Manual (ARMv7-A and ARMv7-R edition). 2008. Available from ARM.  ARM. ARM Architecture Reference Manual (ARMv7-A and ARMv7-R edition). 2008. Available from ARM."},{"key":"e_1_3_2_1_4_1","unstructured":"ARM. ARM Barrier Litmus Tests and Cookbook February 2008.  ARM. ARM Barrier Litmus Tests and Cookbook February 2008."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792233.1792237"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375591"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353522.1353528"},{"key":"e_1_3_2_1_8_1","unstructured":"The Coq proof assistant. http:\/\/coq.inria.fr\/.  The Coq proof assistant. http:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_2"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11947950_7"},{"key":"e_1_3_2_1_12_1","unstructured":"The HOL 4 system. http:\/\/hol.sourceforge.net\/.  The HOL 4 system. http:\/\/hol.sourceforge.net\/."},{"key":"e_1_3_2_1_13_1","unstructured":"IBM. Book E -- Enhanced PowerPC Architecture. May 2002.  IBM. Book E -- Enhanced PowerPC Architecture. May 2002."},{"key":"e_1_3_2_1_14_1","unstructured":"A formal specification of Intel Itanium processor family memory ordering. http:\/\/developer.intel.com\/design\/itanium\/downloads\/251429.htm.  A formal specification of Intel Itanium processor family memory ordering. http:\/\/developer.intel.com\/design\/itanium\/downloads\/251429.htm."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_16_1","unstructured":"Michael Lyons Bill Hay and Brad Frey. PowerPC Storage Model and AIX Programming. November 2005.  Michael Lyons Bill Hay and Brad Frey. PowerPC Storage Model and AIX Programming. November 2005."},{"key":"e_1_3_2_1_17_1","volume-title":"PDCS","author":"Higham L.","year":"1997"},{"key":"e_1_3_2_1_18_1","volume-title":"MIT","author":"Luchangco V. M.","year":"2001"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517444"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/215399.215413"},{"key":"e_1_3_2_1_22_1","unstructured":"Power ISA Version 2.05. October 2007.  Power ISA Version 2.05. October 2007."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/40.372352"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1229428.1229469"},{"key":"e_1_3_2_1_25_1","unstructured":"The SPARC architecture manual v. 9. http:\/\/developers.sun.com\/solaris\/articles\/sparcv9.pdf.   The SPARC architecture manual v. 9. http:\/\/developers.sun.com\/solaris\/articles\/sparcv9.pdf."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_3_2_1_27_1","unstructured":"The semantics of multiprocessor machine code 2008. www.cl.cam.ac.uk\/users\/pes20\/weakmemory.  The semantics of multiprocessor machine code 2008. www.cl.cam.ac.uk\/users\/pes20\/weakmemory."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2004.1302944"}],"event":{"name":"POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Savannah GA USA","acronym":"POPL09","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 4th workshop on Declarative aspects of multicore programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481839.1481842","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1481839.1481842","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:10Z","timestamp":1750253410000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1481839.1481842"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,20]]},"references-count":27,"alternative-id":["10.1145\/1481839.1481842","10.1145\/1481839"],"URL":"https:\/\/doi.org\/10.1145\/1481839.1481842","relation":{},"subject":[],"published":{"date-parts":[[2009,1,20]]},"assertion":[{"value":"2009-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}