{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T23:09:22Z","timestamp":1725750562434},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642415265"},{"type":"electronic","value":"9783642415272"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41527-2_8","type":"book-chapter","created":{"date-parts":[[2013,10,3]],"date-time":"2013-10-03T10:55:48Z","timestamp":1380797748000},"page":"106-120","source":"Crossref","is-referenced-by-count":6,"title":["Proving Non-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":"8_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Birrell, A., Harris, T., Isard, M.: Semantics of transactional memory and automatic mutual exclusion. In: POPL, pp. 63\u201374 (2008)","DOI":"10.1145\/1328897.1328449"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Scott Ananian, C., Asanovic, K., Kuszmaul, B.C., Leiserson, C.E., Lie, S.: Unbounded transactional memory. In: HPCA (2005)","DOI":"10.1109\/MM.2006.26"},{"issue":"2","key":"8_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/568271.223785","volume":"24","author":"H. Berenson","year":"1995","unstructured":"Berenson, H., Bernstein, P., Gray, J., Melton, J., O\u2019Neil, E., O\u2019Neil, P.: A critique of ANSI SQL isolation levels. SIGMOD Rec.\u00a024(2), 1\u201310 (1995)","journal-title":"SIGMOD Rec."},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Bushkov, V., Guerraoui, R., Kapalka, M.: On the liveness of transactional memory. In: PODC, pp. 9\u201318 (2012)","DOI":"10.1145\/2332432.2332435"},{"key":"8_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":"8_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":"8_CR7","unstructured":"Intel Corporation. Intel architecture instruction set extensions programming reference. 319433-012 (2012)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"8_CR9","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.N.: Transactional locking II. In: Dolev, S. (ed.) DISC 2006. LNCS, vol.\u00a04167, pp. 194\u2013208. Springer, Heidelberg (2006)"},{"key":"8_CR10","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":"8_CR11","doi-asserted-by":"crossref","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. In: Formal Aspects of Computing (2012)","DOI":"10.1007\/s00165-012-0225-8"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Emmi, M., Majumdar, R., Manevich, R.: Parameterized verification of transactional memories. In: PLDI, pp. 134\u2013145 (2010)","DOI":"10.1145\/1809028.1806613"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: PPOPP, pp. 175\u2013184 (2008)","DOI":"10.1145\/1345206.1345233"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Henzinger, T.A., Jobstmann, B., Singh, V.: Model checking transactional memories. In: PLDI, pp. 372\u2013382 (2008)","DOI":"10.1145\/1379022.1375626"},{"key":"8_CR15","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":"8_CR16","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":"8_CR17","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: Principles of Transactional Memory. Morgan and Claypool Publishers (2010)","DOI":"10.2200\/S00253ED1V01Y201009DCT004"},{"key":"8_CR18","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":"8_CR19","doi-asserted-by":"crossref","unstructured":"Haring, R., Ohnmacht, M., Fox, T., Gschwind, M., Sattereld, D., Sugavanam, K., Coteus, P., Heidelberger, P., Blumrich, M., Wisniewski, R., Gara, A., Chiu, G.-T., Boyle, P., Chist, N., Kim, C.: The IBM Blue Gene\/Q compute chip (2012)","DOI":"10.1109\/MM.2011.108"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Harris, T., Larus, J., Rajwar, R.: Transactional Memory, 2nd edn. Morgan and Claypool Publishers (2010)","DOI":"10.2200\/S00272ED1V01Y201006CAC011"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Harris, T., Marlow, S., Jones, S.P., Herlihy, M.: Composable memory transactions. In: PPOPP, pp. 48\u201360. ACM Press (2005)","DOI":"10.1145\/1065944.1065952"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Luchangco, V., Moir, M.: A flexible framework for implementing software transactional memory. In: OOPSLA, pp. 253\u2013262 (2006)","DOI":"10.1145\/1167515.1167495"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Luchangco, V., Moir, M., Scherer III, W.N.: Software transactional memory for dynamic-sized data structures. In: PODC (2003)","DOI":"10.1145\/872035.872048"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Moss, J.E.B.: Transactional memory: Architectural support for lock-free data structures. In: ISCA, pp. 289\u2013300 (1993)","DOI":"10.1145\/173682.165164"},{"key":"8_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, pp. 280\u2013281 (2009)","DOI":"10.1145\/1582716.1582764"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Koskinen, E., Parkinson, M., Herlihy, M.: Coarse-grained transactions. In: POPL, pp. 19\u201330 (2010)","DOI":"10.1145\/1707801.1706304"},{"key":"8_CR27","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":"8_CR28","unstructured":"Lesani, M., Palsberg, J.: Proving non-opacity, \n                    \n                      http:\/\/www.cs.ucla.edu\/~lesani\/companion\/disc13"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Moore, K.F., Grossman, D.: High-level small-step operational semantics for transactions. In: POPL, pp. 51\u201362 (2008)","DOI":"10.1145\/1328897.1328448"},{"key":"8_CR30","unstructured":"Pankratius, V., Adl-Tabatabai, A.-R., Otto, F.: Does transactional memory keep its promises? results from an empirical study. Technical Report 2009\u201312, Institute for Program Structures and Data Organization (IPD), University of Karlsruhe (September 2009)"},{"issue":"4","key":"8_CR31","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"C.H. Papadimitriou","year":"1979","unstructured":"Papadimitriou, C.H.: The serializability of concurrent database updates. Journal of the ACM\u00a026(4), 631\u2013653 (1979)","journal-title":"Journal of the ACM"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Rossbach, C.J., Hofmann, O.S., Witchel, E.: Is transactional programming actually easier? SIGPLAN Notices\u00a045(5) (January 2010)","DOI":"10.1145\/1837853.1693462"},{"key":"8_CR33","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":"8_CR34","unstructured":"Scott, M.L.: Sequential specification of transactional memory semantics. In: TRANSACT (2006)"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Shavit, N., Touitou, D.: Software transactional memory. In: PODC (1995)","DOI":"10.1145\/224964.224987"},{"key":"8_CR36","unstructured":"Tasiran, S.: A compositional method for verifying software transactional memory implementations. Technical Report MSR-TR-2008-56, Microsoft Research (2008)"}],"container-title":["Lecture Notes in Computer Science","Distributed Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41527-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T14:36:10Z","timestamp":1558103770000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41527-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642415265","9783642415272"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41527-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}