{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:13Z","timestamp":1750221313165,"version":"3.41.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2017,12,18]],"date-time":"2017-12-18T00:00:00Z","timestamp":1513555200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ADVENT","award":["308830"],"award-info":[{"award-number":["308830"]}]},{"name":"Broadcom Foundation and Tel Aviv University Authentication Initiative"},{"name":"EU FP7 projects TRANSFORM","award":["238639"],"award-info":[{"award-number":["238639"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2018,2,28]]},"abstract":"<jats:p>Transactional memory (TM) facilitates the development of concurrent applications by letting a programmer designate certain code blocks as atomic. The common approach to stating TM correctness is through a consistency condition that restricts the possible TM executions. Unfortunately, existing consistency conditions fall short of formalizing the intuitive semantics of atomic blocks through which programmers use a TM. To close this gap, we formalize programmer expectations as observational refinement between TM implementations. This states that properties of a program using a concrete TM implementation can be established by analyzing its behavior with an abstract TM, serving as a specification of the concrete one.<\/jats:p>\n          <jats:p>\n            We show that a variant of Transactional Memory Specification (TMS), a TM consistency condition, is equivalent to observational refinement for a programming language where local variables are rolled back upon a transaction abort. We thereby establish that TMS is the weakest acceptable condition for this case. We then propose a new consistency condition, called\n            <jats:italic>Strong Transactional Memory Specification (STMS)<\/jats:italic>\n            , and show that it is equivalent to observational refinement for a language where local variables are not rolled back upon aborts. Finally, we show that under certain natural assumptions on TM implementations, STMS is equivalent to a variant of a well-known condition of opacity.\n          <\/jats:p>\n          <jats:p>Our results suggest a new approach to evaluating TM consistency conditions and enable TM implementors and language designers to make better-informed decisions.<\/jats:p>","DOI":"10.1145\/3131360","type":"journal-article","created":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T14:54:00Z","timestamp":1513781640000},"page":"1-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Characterizing Transactional Memory Consistency Conditions Using Observational Refinement"],"prefix":"10.1145","volume":"65","author":[{"given":"Hagit","family":"Attiya","sequence":"first","affiliation":[{"name":"Technion\u2014Israel Institute of Technology, Haifa, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexey","family":"Gotsman","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sandeep","family":"Hans","sequence":"additional","affiliation":[{"name":"Technion\u2014Israel Institute of Technology"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,18]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328449"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2484239.2484267"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-45174-8_26"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2013.57"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987214"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1693453.1693464"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11864219_14"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0225-8"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_19"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2027223.2027269"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1345206.1345233"},{"volume-title":"Principles of Transactional Memory. Morgan 8 Claypool","author":"Guerraoui Rachid","key":"e_1_2_1_12_1","unstructured":"Rachid Guerraoui and Michal Kapalka . 2011. Principles of Transactional Memory. Morgan 8 Claypool , San Rafael, CA . Rachid Guerraoui and Michal Kapalka. 2011. Principles of Transactional Memory. Morgan 8 Claypool, San Rafael, CA."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"T. Harris J. Larus and R. Rajwar. 2010. Transactional Memory. Morgan 8 Claypool San Rafael CA.   T. Harris J. Larus and R. Rajwar. 2010. Transactional Memory. Morgan 8 Claypool San Rafael CA.","DOI":"10.1007\/978-3-031-01728-5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065944.1065952"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1133984"},{"volume-title":"Proceedings of ESOP. 187--196","author":"He J.","key":"e_1_2_1_16_1","unstructured":"J. He , C. Hoare , and J. Sanders . 1986. Data refinement refined . In Proceedings of ESOP. 187--196 . J. He, C. Hoare, and J. Sanders. 1986. Data refinement refined. In Proceedings of ESOP. 187--196."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(87)90224-9"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/872035.872048"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/173682.165164"},{"key":"e_1_2_1_20_1","unstructured":"Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann.   Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.04.037"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11561927_26"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328448"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.05.010"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1229428.1229442"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11864219_20"},{"key":"e_1_2_1_30_1","volume-title":"Retrieved","author":"Scala STM Expert Group","year":"2012","unstructured":"Scala STM Expert Group . 2012 . Scala STM Quick Start Guide . Retrieved October 29, 2017, from https:\/\/nbronson.github.io\/scala-stm\/quick_start.html. Scala STM Expert Group. 2012. Scala STM Quick Start Guide. Retrieved October 29, 2017, from https:\/\/nbronson.github.io\/scala-stm\/quick_start.html."},{"key":"e_1_2_1_31_1","volume-title":"Wojciechowski","author":"Siek Konrad","year":"2015","unstructured":"Konrad Siek and Pawel T . Wojciechowski . 2015 . Last-use opacity: A strong safety property for transactional memory with early release support. arXiv:1506.06275. http:\/\/arxiv.org\/abs\/1506.06275. Konrad Siek and Pawel T. Wojciechowski. 2015. Last-use opacity: A strong safety property for transactional memory with early release support. arXiv:1506.06275. http:\/\/arxiv.org\/abs\/1506.06275."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281161"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPP.2008.55"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1378533.1378584"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3131360","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3131360","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:40Z","timestamp":1750212820000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3131360"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,18]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,2,28]]}},"alternative-id":["10.1145\/3131360"],"URL":"https:\/\/doi.org\/10.1145\/3131360","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2017,12,18]]},"assertion":[{"value":"2016-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-12-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}