{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:16:52Z","timestamp":1763468212616},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662451731"},{"type":"electronic","value":"9783662451748"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-45174-8_27","type":"book-chapter","created":{"date-parts":[[2014,9,29]],"date-time":"2014-09-29T15:28:20Z","timestamp":1412004500000},"page":"391-405","source":"Crossref","is-referenced-by-count":16,"title":["Decomposing Opacity"],"prefix":"10.1007","author":[{"given":"Mohsen","family":"Lesani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jens","family":"Palsberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Ananian, C.S., Asanovic, K., Kuszmaul, B.C., Leiserson, C.E., Lie, S.: Unbounded transactional memory. In: HPCA (2005)","DOI":"10.1109\/MM.2006.26"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Attiya, H., Hans, S., Kuznetsov, P., Ravi, S.: Safety of deferred update in transactional memory. In: ICDCS (2013)","DOI":"10.1109\/ICDCS.2013.57"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Attiya, H., Hillel, E., Milani, A.: Inherent limitations on disjoint-access parallel implementations of transactional memory. Theory of Computing Systems\u00a049(4) (2011)","DOI":"10.1007\/s00224-010-9304-5"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Baek, W., Bronson, N., Kozyrakis, C., Olukotun, K.: Implementing and evaluating a model checker for transactional memory systems. In: ICECCS (2010)","DOI":"10.1109\/ICECCS.2010.30"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Cohen, A., O\u2019Leary, J.W., Pnueli, A., Tuttle, M.R., Zuck, L.D.: Verifying correctness of transactional memories. In: FMCAD (2007)","DOI":"10.1109\/FMCAD.2007.4401980"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-70545-1_13","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2008","unstructured":"Cohen, A., Pnueli, A., Zuck, L.D.: Mechanical verification of transactional memories with non-transactional memory accesses. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 121\u2013134. Springer, Heidelberg (2008)"},{"key":"27_CR7","unstructured":"Intel Corporation. Intel architecture instruction set extensions programming reference, tsx. 319433-012 (2012)"},{"key":"27_CR8","doi-asserted-by":"crossref","unstructured":"Dalessandro, L., Carouge, F., White, S., Lev, Y., Moir, M., Scott, M.L., Spear, M.F.: Hybrid norec: A case study in the effectiveness of best effort hardware transactional memory. In: ASPLOS (2011)","DOI":"10.1145\/1950365.1950373"},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Dalessandro, L., Spear, M.F., Scott, M.L.: Norec: streamlining stm by abolishing ownership records. In: PPoPP (2010)","DOI":"10.1145\/1693453.1693464"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Damron, P., Fedorova, A., Lev, Y., Luchangco, V., Moir, M., Nussbaum, D.: Hybrid transactional memory. SIGPLAN Not.\u00a041(11) (2006)","DOI":"10.1145\/1168918.1168900"},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/11864219_14","volume-title":"Distributed Computing","author":"D. Dice","year":"2006","unstructured":"Dice, D., Shalev, O., Shavit, N.: Transactional locking II. In: Dolev, S. (ed.) DISC 2006. LNCS, vol.\u00a04167, pp. 194\u2013208. Springer, Heidelberg (2006)"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Dice, D., Shavit, N.: TLRW: Return of the read-write lock. In: SPAA (2010)","DOI":"10.1145\/1810479.1810531"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. Formal Aspects of Computing (2012)","DOI":"10.1007\/s00165-012-0225-8"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Emmi, M., Majumdar, R., Manevich, R.: Parameterized verification of transactional memories. In: PLDI (2010)","DOI":"10.1145\/1806596.1806613"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Felber, P., Fetzer, C., Riegel, T.: Dynamic performance tuning of word-based software transactional memory. In: PPoPP (2008)","DOI":"10.1145\/1345206.1345241"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Henzinger, T.A., Jobstmann, B., Singh, V.: Model checking transactional memories. In: PLDI (2008)","DOI":"10.1145\/1375581.1375626"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-02658-4_26","volume-title":"Computer Aided Verification","author":"R. Guerraoui","year":"2009","unstructured":"Guerraoui, R., Henzinger, T.A., Singh, V.: Software transactional memory on relaxed memory models. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 321\u2013336. Springer, Heidelberg (2009)"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Henzinger, T.A., Singh, V.: Model checking transactional memories. Distributed Computing (2010)","DOI":"10.1007\/s00446-009-0092-6"},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: On obstruction-free transactions. In: SPAA (2008)","DOI":"10.1145\/1378533.1378587"},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: PPOPP (2008)","DOI":"10.1145\/1345206.1345233"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: Principles of Transactional Memory. M&C (2010)","DOI":"10.2200\/S00253ED1V01Y201009DCT004"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"Hammond, L., Wong, V., Chen, M., Carlstrom, B.D., Davis, J.D., Hertzberg, B., Prabhu, M.K., Wijaya, H., Kozyrakis, C., Olukotun, K.: Transactional memory coherence and consistency. In: ISCA (2004)","DOI":"10.1145\/1028176.1006711"},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Luchangco, V., Moir, M., Scherer, I.W.N.: Software transactional memory for dynamic-sized data structures. In: PODC (2003)","DOI":"10.1145\/872035.872048"},{"key":"27_CR24","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Moss, J.E.B.: Transactional memory: Architectural support for lock-free data structures. In: ISCA (1993)","DOI":"10.1145\/165123.165164"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Imbs, D., de Mendivil, J.R., Raynal, M.: Brief announcement: virtual world consistency: A new condition for stm systems. In: PODC (2009)","DOI":"10.1145\/1582716.1582764"},{"key":"27_CR26","doi-asserted-by":"crossref","unstructured":"Kumar, S., Chu, M., Hughes, C.J., Kundu, P., Nguyen, A.: Hybrid transactional memory. In: PPoPP (2006)","DOI":"10.1145\/1122971.1123003"},{"key":"27_CR27","unstructured":"Lesani, M.: On the correctness of transactional memory algorithms. Phd Dissertation (2014), \n                    \n                      http:\/\/www.cs.ucla.edu\/~lesani\/companion\/dissertation"},{"key":"27_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/978-3-642-32940-1_36","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"M. Lesani","year":"2012","unstructured":"Lesani, M., Luchangco, V., Moir, M.: A framework for formally verifying software transactional memory algorithms. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 516\u2013530. Springer, Heidelberg (2012)"},{"key":"27_CR29","unstructured":"Lesani, M., Palsberg, J.: Decomposing opacity, the companion page, \n                    \n                      http:\/\/www.cs.ucla.edu\/~lesani\/companion\/disc14"},{"key":"27_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-642-41527-2_8","volume-title":"Distributed Computing","author":"M. Lesani","year":"2013","unstructured":"Lesani, M., Palsberg, J.: Proving non-opacity. In: Afek, Y. (ed.) DISC 2013. LNCS, vol.\u00a08205, pp. 106\u2013120. Springer, Heidelberg (2013)"},{"key":"27_CR31","doi-asserted-by":"crossref","unstructured":"Matveev, A., Shavit, N.: Reduced hardware transactions: A new approach to hybrid transactional memory. In: SPAA (2013)","DOI":"10.1145\/2486159.2486188"},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"Minh, C.C., Trautmann, M., Chung, J., McDonald, A., Bronson, N., Casper, J., Kozyrakis, C., Olukotun, K.: An effective hybrid transactional memory system with strong isolation guarantees. In: ISCA (2007)","DOI":"10.1145\/1250662.1250673"},{"key":"27_CR33","doi-asserted-by":"crossref","unstructured":"O\u2019Leary, J., Saha, B., Tuttle, M.R.: Model checking transactional memory with spin. In: ICDCS (2009)","DOI":"10.1109\/ICDCS.2009.72"},{"key":"27_CR34","doi-asserted-by":"crossref","unstructured":"Perelman, D., Fan, R., Keidar, I.: On maintaining multiple versions in stm. In: PODC (2010)","DOI":"10.1145\/1835698.1835704"},{"key":"27_CR35","doi-asserted-by":"crossref","unstructured":"Saha, B., Adl-Tabatabai, A.-R., Hudson, R.L., Minh, C.C., Hertzberg, B.: McRT-STM: A high performance software transactional memory system for a multi-core runtime. In: PPoPP (2006)","DOI":"10.1145\/1122971.1123001"},{"key":"27_CR36","doi-asserted-by":"crossref","unstructured":"Shavit, N., Touitou, D.: Software transactional memory. In: PODC (1995)","DOI":"10.1145\/224964.224987"},{"key":"27_CR37","doi-asserted-by":"crossref","unstructured":"Wang, A., Gaudet, M., Wu, P., Amaral, J.N., Ohmacht, M., Barton, C., Silvera, R., Michael, M.: Evaluation of blue gene\/q hardware support for transactional memories. In: PACT (2012)","DOI":"10.1145\/2370816.2370836"}],"container-title":["Lecture Notes in Computer Science","Distributed Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-45174-8_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T00:57:44Z","timestamp":1559005064000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-45174-8_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662451731","9783662451748"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-45174-8_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}