{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:56:24Z","timestamp":1774025784987,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,1,21]],"date-time":"2009-01-21T00:00:00Z","timestamp":1232496000000},"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,21]]},"DOI":"10.1145\/1480881.1480929","type":"proceedings-article","created":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T09:41:38Z","timestamp":1232444498000},"page":"379-391","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":74,"title":["The semantics of x86-CC multiprocessor machine code"],"prefix":"10.1145","author":[{"given":"Susmit","family":"Sarkar","sequence":"first","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"}]},{"given":"Scott","family":"Owens","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"given":"Tom","family":"Ridge","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]},{"given":"Thomas","family":"Braibant","sequence":"additional","affiliation":[{"name":"INRIA, Rocquencourt, France"}]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[{"name":"Unviersity of Cambridge, Cambridge, United Kingdom"}]},{"given":"Jade","family":"Alglave","sequence":"additional","affiliation":[{"name":"INRIA, Rocquencourt, France"}]}],"member":"320","published-online":{"date-parts":[[2009,1,21]]},"reference":[{"key":"e_1_3_2_1_1_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_2_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_3_1","unstructured":"Linux kernel traffic 1999. http:\/\/www.kernel-traffic.org\/kernel-traffic\/kt19991220_47.txt.  Linux kernel traffic 1999. http:\/\/www.kernel-traffic.org\/kernel-traffic\/kt19991220_47.txt."},{"key":"e_1_3_2_1_4_1","volume-title":"Sept.","author":"Manual Architecture Programmer's","year":"2007","unstructured":"AMD64 Architecture Programmer's Manual . Advanced Micro Devices , Sept. 2007 . (3 vols). AMD64 Architecture Programmer's Manual. Advanced Micro Devices, Sept. 2007. (3 vols)."},{"key":"e_1_3_2_1_5_1","unstructured":"Intel 64 and IA-32 Architectures Software Developer's Manual. Intel Corporation April (vol 1 2A 2B; rev.27) Feb. (vol.3A 3B; rev.26) 2008.  Intel 64 and IA-32 Architectures Software Developer's Manual. Intel Corporation April (vol 1 2A 2B; rev.27) Feb. (vol.3A 3B; rev.26) 2008."},{"key":"e_1_3_2_1_6_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_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/165231.165264"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_3_2_1_11_1","volume-title":"ARM Architecture Reference Manual (ARMv7-A and ARMv7-R edition)","author":"ARM.","year":"2008","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_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792233.1792237"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375591"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_12"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1353522.1353528"},{"key":"e_1_3_2_1_17_1","volume-title":"Reasoning about parallel architectures","author":"Collier W.","year":"1992","unstructured":"W. Collier . Reasoning about parallel architectures . Prentice-Hall, Inc. , 1992 . W. Collier. Reasoning about parallel architectures. Prentice-Hall, Inc., 1992."},{"key":"e_1_3_2_1_18_1","volume-title":"ISCA","author":"Dubois M.","year":"1986","unstructured":"M. Dubois , C. Scheurich , and F. Briggs . Memory access buffering in multiprocessors . In ISCA , 1986 . M. Dubois, C. Scheurich, and F. Briggs. Memory access buffering in multiprocessors. In ISCA, 1986."},{"key":"e_1_3_2_1_19_1","volume-title":"ISCA","author":"Gordon M.","year":"1986","unstructured":"M. Gordon . Memory access semantics for a multiprocessor instruction set. Unpublished note (c.1993) www.cl.cam.ac.buffering in multiprocessors . In ISCA , 1986 . M. Gordon. Memory access semantics for a multiprocessor instruction set. Unpublished note (c.1993) www.cl.cam.ac.buffering in multiprocessors. In ISCA, 1986."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11947950_7"},{"key":"e_1_3_2_1_21_1","unstructured":"The HOL 4 system. http:\/\/hol.sourceforge.net\/.  The HOL 4 system. http:\/\/hol.sourceforge.net\/."},{"key":"e_1_3_2_1_22_1","volume-title":"Intel 64 architecture memory ordering white paper","year":"2007","unstructured":"Intel. Intel 64 architecture memory ordering white paper , 2007 . SKU 318147-001. Intel. Intel 64 architecture memory ordering white paper, 2007. SKU 318147-001."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_24_1","unstructured":"D. Lea. The JSR-133 cookbook for compiler writers. gee.cs.oswego.edu\/dl\/jmm\/cookbook.html.  D. Lea. The JSR-133 cookbook for compiler writers. gee.cs.oswego.edu\/dl\/jmm\/cookbook.html."},{"key":"e_1_3_2_1_25_1","volume-title":"PDCS","author":"Higham L.","year":"1997","unstructured":"L. Higham , J. Kawash , and N. Verwaal . Defining and comparing memory consistency models . In PDCS , 1997 . L.Higham, J.Kawash, and N. Verwaal. Defining and comparing memory consistency models. In PDCS, 1997."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/215399.215413"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1229428.1229469"},{"key":"e_1_3_2_1_30_1","first-page":"255","article-title":"Event structures. In Advances in Petri Nets","author":"Winskel G.","year":"1986","unstructured":"G. Winskel . Event structures. In Advances in Petri Nets , LNCS 255 , 1986 . G. Winskel. Event structures. In Advances in Petri Nets, LNCS 255, 1986.","journal-title":"LNCS"},{"key":"e_1_3_2_1_31_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","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1480881.1480929","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1480881.1480929","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:30:00Z","timestamp":1750239000000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1480881.1480929"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,21]]},"references-count":30,"alternative-id":["10.1145\/1480881.1480929","10.1145\/1480881"],"URL":"https:\/\/doi.org\/10.1145\/1480881.1480929","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1594834.1480929","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2009,1,21]]},"assertion":[{"value":"2009-01-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}