{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T01:06:30Z","timestamp":1743123990181,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319192482"},{"type":"electronic","value":"9783319192499"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19249-9_11","type":"book-chapter","created":{"date-parts":[[2015,5,23]],"date-time":"2015-05-23T07:55:31Z","timestamp":1432367731000},"page":"161-177","source":"Crossref","is-referenced-by-count":10,"title":["Verifying Opacity of a Transactional Mutex Lock"],"prefix":"10.1007","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oleg","family":"Travkin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-662-45174-8_26","volume-title":"Distributed Computing","author":"H. Attiya","year":"2014","unstructured":"Attiya, H., Gotsman, A., Hans, S., Rinetzky, N.: Safety of live transactions in transactional memory: TMS is necessary and sufficient. In: Kuhn, F. (ed.) DISC 2014. LNCS, vol.\u00a08784, pp. 376\u2013390. Springer, Heidelberg (2014)"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Attiya, H., Gotsman, A., Hans, S., Rinetzky, N.: A programming language perspective on transactional memory consistency. In: Fatourou, P., Taubenfeld, G. (eds.) PODC 2013, pp. 309\u2013318. ACM (2013)","DOI":"10.1145\/2484239.2484267"},{"key":"11_CR3","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":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-15291-7_2","volume-title":"Euro-Par 2010 - Parallel Processing","author":"L. Dalessandro","year":"2010","unstructured":"Dalessandro, L., Dice, D., Scott, M.L., Shavit, N., Spear, M.F.: Transactional mutex locks. In: D\u2019Ambra, P., Guarracino, M., Talia, D. (eds.) Euro-Par 2010, Part II. LNCS, vol.\u00a06272, pp. 2\u201313. Springer, Heidelberg (2010)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-642-21437-0_25","volume-title":"FM 2011: Formal Methods","author":"J. Derrick","year":"2011","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Verifying linearisability with potential linearisation points. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 323\u2013337. Springer, Heidelberg (2011)"},{"issue":"5","key":"11_CR6","doi-asserted-by":"publisher","first-page":"769","DOI":"10.1007\/s00165-012-0225-8","volume":"25","author":"S. Doherty","year":"2013","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. Formal Asp. Comput.\u00a025(5), 769\u2013799 (2013)","journal-title":"Formal Asp. Comput."},{"issue":"3","key":"11_CR7","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s00446-009-0092-6","volume":"22","author":"R. Guerraoui","year":"2010","unstructured":"Guerraoui, R., Henzinger, T.A., Singh, V.: Model checking transactional memories. Distributed Computing\u00a022(3), 129\u2013145 (2010)","journal-title":"Distributed Computing"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: Chatterjee, S., Scott, M.L. (eds.) PPOPP, pp. 175\u2013184. ACM (2008)","DOI":"10.1145\/1345206.1345233"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: Principles of Transactional Memory. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2010)","DOI":"10.1007\/978-3-031-02002-5"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Harris, T., Larus, J.R., Rajwar, R.: Transactional Memory, 2nd edition. Synthesis Lectures on Computer Architecture. Morgan & Claypool Publishers (2010)","DOI":"10.1007\/978-3-031-01728-5"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Harris, T.L., Fraser, K.: Language support for lightweight transactions. In: Crocker, R., Steele Jr., G.L. (eds.) OOPSLA, pp. 388\u2013402. ACM (2003)","DOI":"10.1145\/949343.949340"},{"issue":"3","key":"11_CR12","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M. Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM TOPLAS\u00a012(3), 463\u2013492 (1990)","journal-title":"ACM TOPLAS"},{"key":"11_CR13","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.tcs.2012.04.037","volume":"444","author":"D. Imbs","year":"2012","unstructured":"Imbs, D., Raynal, M.: Virtual world consistency: A condition for STM systems (with a versatile protocol with invisible read operations). Theor. Comput. Sci.\u00a0444, 113\u2013127 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR14","unstructured":"Lesani, M.: On the Correctness of Transactional Memory Algorithms. PhD thesis, UCLA (2014)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-662-45174-8_27","volume-title":"Distributed Computing","author":"M. Lesani","year":"2014","unstructured":"Lesani, M., Palsberg, J.: Decomposing opacity. In: Kuhn, F. (ed.) DISC 2014. LNCS, vol.\u00a08784, pp. 391\u2013405. Springer, Heidelberg (2014)"},{"key":"11_CR16","unstructured":"Luchangco, V., Lesani, M., Moir, M.: Putting opacity in its place. In: Workshop on the Theory of Transactional Memory (2012)"},{"issue":"4","key":"11_CR17","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. J. ACM\u00a026(4), 631\u2013653 (1979)","journal-title":"J. ACM"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Automated Deduction\u2014A Basis for Applications. Interactive Theorem Proving, vol.\u00a0II, ch.1, pp. 13\u201339. Kluwer (1998)","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Derrick., J., Wehrheim, H.: A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. ACM Trans. Comput. Logic, 15 (2014)","DOI":"10.1145\/2629496"},{"issue":"2","key":"11_CR20","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s004460050028","volume":"10","author":"N. Shavit","year":"1997","unstructured":"Shavit, N., Touitou, D.: Software transactional memory. Distributed Computing\u00a010(2), 99\u2013116 (1997)","journal-title":"Distributed Computing"},{"key":"11_CR21","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall (1992)"},{"key":"11_CR22","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. PhD thesis, University of Cambridge (2007)"}],"container-title":["Lecture Notes in Computer Science","FM 2015: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19249-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T12:23:32Z","timestamp":1675859012000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19249-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319192482","9783319192499"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19249-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}