{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:34:10Z","timestamp":1761597250942,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011,1]]},"abstract":"<jats:p>Software Transactional Memory (STM) is an attractive basis for the development of language features for concurrent programming. However, the semantics of these features can be delicate and problematic. In this article we explore the trade-offs semantic simplicity, the viability of efficient implementation strategies, and the flexibility of language constructs. Specifically, we develop semantics and type systems for the constructs of the Automatic Mutual Exclusion (AME) programming model; our results apply also to other constructs, such as atomic blocks. With this semantics as a point of reference, we study several implementation strategies. We model STM systems that use in-place update, optimistic concurrency, lazy conflict detection, and rollback. These strategies are correct only under nontrivial assumptions that we identify and analyze. One important source of errors is that some efficient implementations create dangerous \u201czombie\u201d computations where a transaction keeps running after experiencing a conflict; the assumptions confine the effects of these computations.<\/jats:p>","DOI":"10.1145\/1889997.1889999","type":"journal-article","created":{"date-parts":[[2011,1,24]],"date-time":"2011-01-24T14:58:13Z","timestamp":1295881093000},"page":"1-50","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Semantics of transactional memory and automatic mutual exclusion"],"prefix":"10.1145","volume":"33","author":[{"given":"Mart\u00edn","family":"Abadi","sequence":"first","affiliation":[{"name":"Microsoft Research, Silicon Valley, University of California, Santa Cruz, and Coll\u00e8ge de France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Birrell","sequence":"additional","affiliation":[{"name":"Microsoft Research, Silicon Valley"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Harris","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Isard","sequence":"additional","affiliation":[{"name":"Microsoft Research, Silicon Valley"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2011,1,25]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1007\/978-3-540-68679-8_32"},{"unstructured":"Abadi M. Birrell A. Harris T. Hsieh J. and Isard M. 2008. Dynamic separation for transactional memory. Tech. rep. MSR-TR-2008-43 Microsoft Research.  Abadi M. Birrell A. Harris T. Hsieh J. and Isard M. 2008. Dynamic separation for transactional memory. Tech. rep. MSR-TR-2008-43 Microsoft Research.","key":"e_1_2_1_2_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1007\/978-3-642-00722-4_6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1145\/1119479.1119480"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1007\/978-3-540-85361-9_5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1145\/1133981.1133985"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1145\/325096.325100"},{"volume-title":"Proceedings of the USENIX Annual Technical Conference (USENIX'02)","author":"Adya A.","unstructured":"Adya , A. , Howell , J. , Theimer , M. , Bolosky , W. J. , and Douceur , J. R . 2002. Cooperative task management without manual stack management . In Proceedings of the USENIX Annual Technical Conference (USENIX'02) . 289--302. Adya, A., Howell, J., Theimer, M., Bolosky, W. J., and Douceur, J. R. 2002. Cooperative task management without manual stack management. In Proceedings of the USENIX Annual Technical Conference (USENIX'02). 289--302.","key":"e_1_2_1_8_1"},{"unstructured":"Allen E. Chase D. Hallett J. Luchangco V. Maessen J.-W. Ryu S. Steele  Jr. G. L. and Tobin-Hochstadt S. 2007. The Fortress language specification v1.0\u03b2. Tech. rep. Sun Microsystems.  Allen E. Chase D. Hallett J. Luchangco V. Maessen J.-W. Ryu S. Steele Jr. G. L. and Tobin-Hochstadt S. 2007. The Fortress language specification v1.0\u03b2. Tech. rep. Sun Microsystems.","key":"e_1_2_1_9_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1109\/L-CA.2006.18"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1145\/1480881.1480909"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1145\/1133981.1133983"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.5555\/1333874.1334162"},{"volume-title":"Proceedings of the 4th Workshop on Transactional Computing (TRANSACT'09)","author":"Dalessandro L.","unstructured":"Dalessandro , L. and Scott , M. L . 2009. Strong isolation is a weak idea . In Proceedings of the 4th Workshop on Transactional Computing (TRANSACT'09) . Dalessandro, L. and Scott, M. L. 2009. Strong isolation is a weak idea. In Proceedings of the 4th Workshop on Transactional Computing (TRANSACT'09).","key":"e_1_2_1_14_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1007\/11864219_14"},{"unstructured":"Dice D. and Shavit N. 2006. What really makes transactions faster&quest; In Proceedings of the ACM SIGPLAN Workshop on Languages Compilers and Hardware Support for Transactional Computing (TRANSACT'06). http:\/\/hdl.handle.net\/1802\/4051.  Dice D. and Shavit N. 2006. What really makes transactions faster&quest; In Proceedings of the ACM SIGPLAN Workshop on Languages Compilers and Hardware Support for Transactional Computing (TRANSACT'06). http:\/\/hdl.handle.net\/1802\/4051.","key":"e_1_2_1_16_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1145\/1178597.1178609"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1145\/1375581.1375626"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1007\/978-3-540-85361-9_6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1145\/949305.949340"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/1065944.1065952"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1145\/1133981.1133984"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1145\/503502.503505"},{"volume-title":"Proceedings of the 11th Workshop on Hot Topics in Operating Systems (HotOS'07)","author":"Isard M.","unstructured":"Isard , M. and Birrell , A . 2007. Automatic mutual exclusion . In Proceedings of the 11th Workshop on Hot Topics in Operating Systems (HotOS'07) . Isard, M. and Birrell, A. 2007. Automatic mutual exclusion. In Proceedings of the 11th Workshop on Hot Topics in Operating Systems (HotOS'07).","key":"e_1_2_1_24_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1016\/j.scico.2005.03.001"},{"unstructured":"Kuszmaul B. C. and Leiserson C. E. 2003. Transactions everywhere. Tech. rep. MIT. http:\/\/hdl.handle.net\/1721.1\/3692.  Kuszmaul B. C. and Leiserson C. E. 2003. Transactions everywhere. Tech. rep. MIT. http:\/\/hdl.handle.net\/1721.1\/3692.","key":"e_1_2_1_26_1"},{"unstructured":"Liblit B. 2006. An operational semantics for LogTM. Tech. rep. 1571 University of Wisconsin--Madison. Version 1.0.  Liblit B. 2006. An operational semantics for LogTM. Tech. rep. 1571 University of Wisconsin--Madison. Version 1.0.","key":"e_1_2_1_27_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1109\/RTSS.2005.34"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1145\/1040305.1040336"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.1145\/1378533.1378588"},{"volume-title":"Proceedings of the 12th International Symposium on High-Performance Computer Architecture (HPCA'06)","author":"Moore K. E.","unstructured":"Moore , K. E. , Bobba , J. , Moravan , M. J. , Hill , M. D. , and Wood , D. A . 2006. LogTM: Log-based transactional memory . In Proceedings of the 12th International Symposium on High-Performance Computer Architecture (HPCA'06) . 254--265. Moore, K. E., Bobba, J., Moravan, M. J., Hill, M. D., and Wood, D. A. 2006. LogTM: Log-based transactional memory. In Proceedings of the 12th International Symposium on High-Performance Computer Architecture (HPCA'06). 254--265.","key":"e_1_2_1_31_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_32_1","DOI":"10.1145\/1328438.1328448"},{"doi-asserted-by":"publisher","key":"e_1_2_1_33_1","DOI":"10.1145\/1133981.1134018"},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1145\/1122971.1123001"},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.1145\/1449764.1449779"},{"key":"e_1_2_1_36_1","volume-title":"Proceedings of the 1st ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT'06)","author":"Scott M. L.","year":"2006","unstructured":"Scott , M. L. 2006 . Sequential specification of transactional memory semantics . In Proceedings of the 1st ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT'06) . http:\/\/hdl.handle.net\/1802\/4050. Scott, M. L. 2006. Sequential specification of transactional memory semantics. In Proceedings of the 1st ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT'06). http:\/\/hdl.handle.net\/1802\/4050."},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1145\/224964.224987"},{"doi-asserted-by":"publisher","key":"e_1_2_1_38_1","DOI":"10.1145\/1250734.1250744"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.1007\/978-3-540-92221-6_19"},{"doi-asserted-by":"crossref","unstructured":"Spear M. F. Marathe V. J. Dalessandro L. and Scott M. L. 2007. Privatization techniques for software transactional memory. Tech. rep. 915 University of Rochester.  Spear M. F. Marathe V. J. Dalessandro L. and Scott M. L. 2007. Privatization techniques for software transactional memory. Tech. rep. 915 University of Rochester.","key":"e_1_2_1_40_1","DOI":"10.1145\/1281100.1281161"},{"key":"e_1_2_1_41_1","volume-title":"Proceedings of the USENIX Winter Technical Conference. 97--106","author":"Sterling N.","year":"1993","unstructured":"Sterling , N. 1993 . Warlock: A static data race analysis tool . In Proceedings of the USENIX Winter Technical Conference. 97--106 . Sterling, N. 1993. Warlock: A static data race analysis tool. In Proceedings of the USENIX Winter Technical Conference. 97--106."},{"unstructured":"Tasiran S. 2008. A compositional method for verifying software transactional memory implementations. Tech. rep. MSR-TR-2008-56 Microsoft Research.  Tasiran S. 2008. A compositional method for verifying software transactional memory implementations. Tech. rep. MSR-TR-2008-56 Microsoft Research.","key":"e_1_2_1_42_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_43_1","DOI":"10.1109\/CGO.2007.4"},{"doi-asserted-by":"publisher","key":"e_1_2_1_44_1","DOI":"10.1145\/1094811.1094845"},{"doi-asserted-by":"publisher","key":"e_1_2_1_45_1","DOI":"10.1006\/inco.1994.1093"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1889997.1889999","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1889997.1889999","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:52:18Z","timestamp":1750243938000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1889997.1889999"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["10.1145\/1889997.1889999"],"URL":"https:\/\/doi.org\/10.1145\/1889997.1889999","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2011,1]]},"assertion":[{"value":"2008-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}