{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:49:07Z","timestamp":1740098947872,"version":"3.37.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319677286"},{"type":"electronic","value":"9783319677293"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-67729-3_8","type":"book-chapter","created":{"date-parts":[[2017,9,16]],"date-time":"2017-09-16T01:04:04Z","timestamp":1505523844000},"page":"118-135","source":"Crossref","is-referenced-by-count":1,"title":["Value-Based or Conflict-Based? Opacity Definitions for STMs"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"K\u00f6nig","sequence":"first","affiliation":[]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,17]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Armstrong, A., Dongol, B., Doherty, S.: Reducing opacity to linearizability: a sound and complete method. arXiv preprint arXiv:1610.01004 (2016)","DOI":"10.1007\/978-3-319-60225-7_4"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Attiya, H., Hans, S., Kuznetsov, P., Ravi, S.: Safety of deferred update in transactional memory. In: 2013 IEEE 33rd International Conference on Distributed Computing Systems (ICDCS), pp. 601\u2013610. IEEE (2013)","DOI":"10.1109\/ICDCS.2013.57"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: ACM SIGPLAN Notices, vol. 45, pp. 330\u2013340. ACM (2010)","DOI":"10.1145\/1806596.1806634"},{"key":"8_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., Shavit, N., Spear, M.: Transactional mutex locks. In: D\u2019Ambra, P., Guarracino, M., Talia, D. (eds.) Euro-Par 2010. LNCS, vol. 6272, pp. 2\u201313. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15291-7_2"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Dalessandro, L., Spear, M.F., Scott, M.L.: NOrec: streamlining STM by abolishing ownership records. In: ACM Sigplan Notices, vol. 45, pp. 67\u201378. ACM (2010)","DOI":"10.1145\/1693453.1693464"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-319-19249-9_11","volume-title":"FM 2015: Formal Methods","author":"J Derrick","year":"2015","unstructured":"Derrick, J., Dongol, B., Schellhorn, G., Travkin, O., Wehrheim, H.: Verifying opacity of a transactional mutex lock. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 161\u2013177. Springer, Cham (2015). doi: 10.1007\/978-3-319-19249-9_11"},{"key":"8_CR7","unstructured":"Doherty, S., Dongol, B., Derrick, J., Schellhorn, G., Wehrheim, H.: Proving opacity of a pessimistic STM. In: Fatourou, P., Jim\u00e9nez, E., Pedone, F. (eds.) 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol. 70, pp. 35:1\u201335:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl (2017). http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2017\/7104"},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. Formal Aspects Comput. 25(5), 769\u2013799 (2013). http:\/\/dx.doi.org\/10.1007\/s00165-012-0225-8","DOI":"10.1007\/s00165-012-0225-8"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-14720-8_1","volume-title":"Transactional Memory. Foundations, Algorithms, Tools, and Applications","author":"D Dziuma","year":"2015","unstructured":"Dziuma, D., Fatourou, P., Kanellou, E.: Consistency for transactional memory computing. In: Guerraoui, R., Romano, P. (eds.) Transactional Memory. Foundations, Algorithms, Tools, and Applications. LNCS, vol. 8913, pp. 3\u201331. Springer, Cham (2015). doi: 10.1007\/978-3-319-14720-8_1"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-04355-0_12","volume-title":"Distributed Computing","author":"P Felber","year":"2009","unstructured":"Felber, P., Gramoli, V., Guerraoui, R.: Elastic transactions. In: Keidar, I. (ed.) DISC 2009. LNCS, vol. 5805, pp. 93\u2013107. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04355-0_12"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-85361-9_6","volume-title":"CONCUR 2008 - Concurrency Theory","author":"R Guerraoui","year":"2008","unstructured":"Guerraoui, R., Henzinger, T.A., Singh, V.: Completeness and nondeterminism in model checking transactional memories. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 21\u201335. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-85361-9_6"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Henzinger, T.A., Singh, V.: Model checking transactional memories. Distrib. Comput. 22(3), 129\u2013145 (2010). http:\/\/dx.doi.org\/10.1007\/s00446-009-0092-6","DOI":"10.1007\/s00446-009-0092-6"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP 2008), pp. 175\u2013184. ACM, New York (2008). http:\/\/doi.acm.org\/10.1145\/1345206.1345233","DOI":"10.1145\/1345206.1345233"},{"key":"8_CR14","unstructured":"Herlihy, M., Moss, J.E.B.: Transactional memory: architectural support for lock-free data structures. In: Proceedings of the 20th Annual International Symposium on Computer Architecture, San Diego, CA, May 1993, pp. 289\u2013300 (1993). http:\/\/doi.acm.org\/10.1145\/165123.165164"},{"issue":"3","key":"8_CR15","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"MP Herlihy","year":"1990","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. (TOPLAS) 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"8_CR16","doi-asserted-by":"crossref","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). Theoret. Comput. Sci. 444, 113\u2013127 (2012)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR17","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. 7454, pp. 516\u2013530. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32940-1_36"},{"key":"8_CR18","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. 8205, pp. 106\u2013120. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-41527-2_8"},{"key":"8_CR19","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. 8784, pp. 391\u2013405. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-45174-8_27"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Manovit, C., Hangal, S., Chafi, H., McDonald, A., Kozyrakis, C., Olukotun, K.: Testing implementations of transactional memory. In: Proceedings of the 15th International Conference on Parallel Architectures and Compilation Techniques, pp. 134\u2013143. ACM (2006)","DOI":"10.1145\/1152154.1152177"},{"key":"8_CR21","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":"LM Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-78800-3_24"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"O\u2019Leary, J., Saha, B., Tuttle, M.R.: Model checking transactional memory with spin. In: 2009 29th IEEE International Conference on Distributed Computing Systems (ICDCS 2009), pp. 335\u2013342. IEEE (2009)","DOI":"10.1109\/ICDCS.2009.72"},{"issue":"4","key":"8_CR23","doi-asserted-by":"crossref","first-page":"631","DOI":"10.1145\/322154.322158","volume":"26","author":"CH Papadimitriou","year":"1979","unstructured":"Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM (JACM) 26(4), 631\u2013653 (1979)","journal-title":"J. ACM (JACM)"},{"key":"8_CR24","unstructured":"Riegel, T., Fetzer, C., Felber, P.: Snapshot isolation for software transactional memory. In: First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT 2006), pp. 1\u201310. Association for Computing Machinery (ACM) (2006)"},{"issue":"2","key":"8_CR25","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/s004460050028","volume":"10","author":"N Shavit","year":"1997","unstructured":"Shavit, N., Touitou, D.: Software transactional memory. Distrib. Comput. 10(2), 99\u2013116 (1997)","journal-title":"Distrib. Comput."},{"key":"8_CR26","unstructured":"Siek, K., Wojciechowski, P.T.: Last-use opacity: a strong safety property for transactional memory with early release support. CoRR abs\/1506.06275 (2015). http:\/\/arxiv.org\/abs\/1506.06275"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Sinha, A., Malik, S.: Runtime checking of serializability in software transactional memory. In: 2010 IEEE International Symposium on Parallel and Distributed Processing (IPDPS), pp. 1\u201312. IEEE (2010)","DOI":"10.1109\/IPDPS.2010.5470389"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Spear, M.F., Michael, M.M., von Praun, C.: RingSTM: Scalable transactions with a single atomic instruction. In: Proceedings of the Twentieth Annual Symposium on Parallelism in Algorithms and Architectures, pp. 275\u2013284. ACM (2008)","DOI":"10.1145\/1378533.1378583"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2017"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67729-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,3]],"date-time":"2019-10-03T11:18:24Z","timestamp":1570101504000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67729-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319677286","9783319677293"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67729-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}