{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:36:48Z","timestamp":1791459408948,"version":"4.3.4"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"7","license":[{"start":{"date-parts":[[2010,7,1]],"date-time":"2010-07-01T00:00:00Z","timestamp":1277942400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/F036345EP\/H005633"],"award-info":[{"award-number":["EP\/F036345EP\/H005633"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-06-SETI-010-02"],"award-info":[{"award-number":["ANR-06-SETI-010-02"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2010,7]]},"abstract":"<jats:p>Exploiting the multiprocessors that have recently become ubiquitous requires high-performance and reliable concurrent systems code, for concurrent data structures, operating system kernels, synchronization libraries, compilers, and so on. However, concurrent programming, which is always challenging, is made much more so by two problems. First, real multiprocessors typically do not provide the sequentially consistent memory that is assumed by most work on semantics and verification. Instead, they have relaxed memory models, varying in subtle ways between processor families, in which different hardware threads may have only loosely consistent views of a shared memory. Second, the public vendor architectures, supposedly specifying what programmers can rely on, are often in ambiguous informal prose (a particularly poor medium for loose specifications), leading to widespread confusion.<\/jats:p>\n                  <jats:p>\n                    In this paper we focus on x86 processors. We review several recent Intel and AMD specifications, showing that all contain serious ambiguities, some are arguably too weak to program above, and some are simply unsound with respect to actual hardware. We present a new\n                    <jats:italic>x86-TSO<\/jats:italic>\n                    programmer's model that, to the best of our knowledge, suffers from none of these problems. It is mathematically precise (rigorously defined in HOL4) but can be presented as an intuitive abstract machine which should be widely accessible to working programmers. We illustrate how this can be used to reason about the correctness of a Linux spinlock implementation and describe a general theory of data-race freedom for x86-TSO. This should put x86 multiprocessor system building on a more solid foundation; it should also provide a basis for future work on verification of such systems.\n                  <\/jats:p>","DOI":"10.1145\/1785414.1785443","type":"journal-article","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T13:43:38Z","timestamp":1277473418000},"page":"89-97","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":376,"title":["x86-TSO"],"prefix":"10.1145","volume":"53","author":[{"given":"Peter","family":"Sewell","sequence":"first","affiliation":[{"name":"University of Cambridge"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Susmit","family":"Sarkar","sequence":"additional","affiliation":[{"name":"University of Cambridge"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Scott","family":"Owens","sequence":"additional","affiliation":[{"name":"University of Cambridge"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Francesco Zappa","family":"Nardelli","sequence":"additional","affiliation":[{"name":"INRIA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[{"name":"University of Cambridge"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,7]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Linux kernel mailing list thread \"spin_unlock optimization (i386)\" 119 messages Nov. 20--Dec. 7 1999 http:\/\/www.gossamer-threads.com\/lists\/engine?post=105365;list=linux. Accessed 2009\/11\/18.  Linux kernel mailing list thread \"spin_unlock optimization (i386)\" 119 messages Nov. 20--Dec. 7 1999 http:\/\/www.gossamer-threads.com\/lists\/engine?post=105365;list=linux. Accessed 2009\/11\/18."},{"key":"e_1_2_1_2_1","first-page":"I9308","author":"The SPARC","year":"1992","journal-title":"Inc."},{"key":"e_1_2_1_3_1","unstructured":"AMD64 Architecture Programmer's Manual (3 vols). Advanced Micro Devices Sept. 2007. rev. 3.14. AMD64 Architecture Programmer's Manual (3 vols ). Advanced Micro Devices Sept. 2007. rev. 3.14."},{"key":"e_1_2_1_4_1","unstructured":"Intel 64 architecture memory ordering white paper 2007. Intel Corporation. SKU 318147-001.  Intel 64 architecture memory ordering white paper 2007. Intel Corporation. SKU 318147-001."},{"key":"e_1_2_1_5_1","unstructured":"Intel 64 and IA-32 Architectures Software Developer's Manual (5 vols). Intel Corporation Mar. 2010. rev. 34. Intel 64 and IA-32 Architectures Software Developer's Manual (5 vols ). Intel Corporation Mar. 2010. rev. 34."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_2_1_7_1","unstructured":"Adve S.V. Boehm H.-J. Memory models: A case for rethinking parallel languages and hardware. C. ACM To appear.  Adve S.V. Boehm H.-J. Memory models: A case for rethinking parallel languages and hardware. C. ACM To appear."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.242161"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792233.1792237"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480930"},{"key":"e_1_2_1_14_1","unstructured":"Burckhardt S. Musuvathi M. Singh V. Verifying compiler transformations for concurrent programs Jan. 2009. Technical report MSR-TR-2008-171.  Burckhardt S. Musuvathi M. Singh V. Verifying compiler transformations for concurrent programs Jan. 2009. Technical report MSR-TR-2008-171."},{"key":"e_1_2_1_15_1","unstructured":"Dice D. Java memory model concerns on Intel and AMD systems. http:\/\/blogs.sun.com\/dave\/entry\/java_memory_model_concerns_on Jan. 2008.  Dice D. Java memory model concerns on Intel and AMD systems. http:\/\/blogs.sun.com\/dave\/entry\/java_memory_model_concerns_on Jan. 2008."},{"key":"e_1_2_1_16_1","volume-title":"Israel Institute of Technologic","author":"Friedman R.","year":"1994"},{"key":"e_1_2_1_17_1","first-page":"9","article-title":"Memory consistency models for shared-memory multiprocessors","volume":"95","author":"Gharachorloo K","year":"1995","journal-title":"WRL Res. Rep."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/998680.1006710"},{"key":"e_1_2_1_20_1","unstructured":"The HOL 4 system. http:\/\/hol.sourceforge.net\/.  The HOL 4 system. http:\/\/hol.sourceforge.net\/."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of AFM (Automated Formal Methods) (Aug. 2006). FLoC workshop. http:\/\/fm.csl.sri.com\/AFM06\/.","author":"Loewenstein P.N."},{"key":"e_1_2_1_23_1","volume-title":"MIT","author":"Luchango V.M.","year":"2001"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_2_1_25_1","volume-title":"Prentice Hall International","author":"Milner R.","year":"1989"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883978.1884011"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.752664"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_46"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1229428.1229469"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480929"},{"key":"e_1_2_1_32_1","first-page":"42","article-title":"Formal specification of memory models. In Scalable Shared Memory Multiprocessors","volume":"25","author":"Sindhu P.S.","year":"1991","journal-title":"Kluwer"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_3"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1785414.1785443","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1785414.1785443","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:39:48Z","timestamp":1750232388000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1785414.1785443"}},"subtitle":["a rigorous and usable programmer's model for x86 multiprocessors"],"short-title":[],"issued":{"date-parts":[[2010,7]]},"references-count":31,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2010,7]]}},"alternative-id":["10.1145\/1785414.1785443"],"URL":"https:\/\/doi.org\/10.1145\/1785414.1785443","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,7]]},"assertion":[{"value":"2010-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}