{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T18:05:45Z","timestamp":1742925945371,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319929699"},{"type":"electronic","value":"9783319929705"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-92970-5_7","type":"book-chapter","created":{"date-parts":[[2018,5,29]],"date-time":"2018-05-29T08:54:12Z","timestamp":1527584052000},"page":"105-120","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["FastLane Is Opaque \u2013 a Case Study in Mechanized Proofs of Opacity"],"prefix":"10.1007","author":[{"given":"Gerhard","family":"Schellhorn","sequence":"first","affiliation":[]},{"given":"Monika","family":"Wedel","sequence":"additional","affiliation":[]},{"given":"Oleg","family":"Travkin","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"K\u00f6nig","sequence":"additional","affiliation":[]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,5,30]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","unstructured":"Armstrong, A., Dongol, B.: Modularising opacity verification for hybrid transactional memory. In: Bouajjani and Silva [3], pp. 33\u201349. https:\/\/doi.org\/10.1007\/978-3-319-60225-7_3","DOI":"10.1007\/978-3-319-60225-7_3"},{"key":"7_CR2","doi-asserted-by":"publisher","unstructured":"Armstrong, A., Dongol, B., Doherty, S.: Proving opacity via linearizability: a sound and complete method. In: Bouajjani and Silva [3], pp. 50\u201366. https:\/\/doi.org\/10.1007\/978-3-319-60225-7_4","DOI":"10.1007\/978-3-319-60225-7_4"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-60225-7","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","year":"2017","unstructured":"Bouajjani, A., Silva, A. (eds.): FORTE 2017. LNCS, vol. 10321. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-60225-7"},{"key":"7_CR4","unstructured":"Cohen, A., O\u2019Leary, J.W., Pnueli, A., Tuttle, M.R., Zuck, L.D.: Verifying correctness of transactional memories. In: Formal Methods in Computer Aided Design, 2007, FMCAD 2007, pp. 37\u201344. IEEE (2007)"},{"key":"7_CR5","unstructured":"Dalessandro, L., Spear, M.F., Scott, M.L.: NOrec: streamlining STM by abolishing ownership records. In: Govindarajan, R., Padua, D.A., Hall, M.W. (eds.) PPoPP, pp. 67\u201378. ACM (2010). http:\/\/doi.acm.org\/10.1145\/1693453.1693464"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Derrick, J., Doherty, S., Dongol, B., Schellhorn, G., Travkin, O., Wehrheim, H.: Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects Comput. (2017). https:\/\/doi.org\/10.1007\/s00165-017-0433-3","DOI":"10.1007\/s00165-017-0433-3"},{"key":"7_CR7","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. 4167, pp. 194\u2013208. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11864219_14"},{"key":"7_CR8","doi-asserted-by":"publisher","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.) OPODIS. LIPIcs, vol. 70, pp. 35:1\u201335:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.OPODIS.2016.35","DOI":"10.4230\/LIPIcs.OPODIS.2016.35"},{"issue":"5","key":"7_CR9","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 Aspects Comput. 25(5), 769\u2013799 (2013). https:\/\/doi.org\/10.1007\/s00165-012-0225-8","journal-title":"Formal Aspects Comput."},{"key":"7_CR10","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2014","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV - overview and verify this competition. Softw. Tools Technol. Transf. 17, 677\u2013694 (2014)","journal-title":"Softw. Tools Technol. Transf."},{"key":"7_CR11","unstructured":"KIV proofs for FastLane (2018). http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/FastLane.html"},{"key":"7_CR12","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). https:\/\/doi.org\/10.1007\/978-3-540-85361-9_6"},{"issue":"3","key":"7_CR13","doi-asserted-by":"crossref","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. Distrib. Comput. 22(3), 129 (2010)","journal-title":"Distrib. Comput."},{"key":"7_CR14","unstructured":"Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: Chatterjee, S., Scott, M.L. (eds.) PPOPP, pp. 175\u2013184. ACM (2008). http:\/\/doi.acm.org\/10.1145\/1345206.1345233"},{"key":"7_CR15","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, pp. 92\u2013101. ACM (2003)","DOI":"10.1145\/872035.872048"},{"issue":"3","key":"7_CR16","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 Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990). https:\/\/doi.org\/10.1145\/78969.78972","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_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). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_36"},{"key":"7_CR18","unstructured":"Lesani, M., Luchangco, V., Moir, M.: Putting opacity in its place. In: Workshop on the Theory of Transactional Memory (2012)"},{"key":"7_CR19","unstructured":"Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: Schneider, F.B. (ed.) PODC, pp. 137\u2013151. ACM (1987). http:\/\/doi.acm.org\/10.1145\/41840.41852"},{"issue":"2","key":"7_CR20","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"NA Lynch","year":"1995","unstructured":"Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: I Untimed Systems. Inf. Comput. 121(2), 214\u2013233 (1995). https:\/\/doi.org\/10.1006\/inco.1995.1134","journal-title":"Inf. Comput."},{"key":"7_CR21","unstructured":"O\u2019Leary, J., Saha, B., Tuttle, M.R.: Model checking transactional memory with Spin. In: 29th IEEE International Conference on Distributed Computing Systems, 2009, ICDCS 2009, pp. 335\u2013342. IEEE (2009)"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Papadimitriou, C.H.: The serializability of concurrent database updates. J. ACM 26(4), 631\u2013653 (1979). http:\/\/doi.acm.org\/10.1145\/322154.322158","DOI":"10.1145\/322154.322158"},{"issue":"2","key":"7_CR23","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. Distrib. Comput. 10(2), 99\u2013116 (1997). https:\/\/doi.org\/10.1007\/s004460050028","journal-title":"Distrib. Comput."},{"key":"7_CR24","unstructured":"Wamhoff, J., Fetzer, C., Felber, P., Rivi\u00e8re, E., Muller, G.: FastLane: improving performance of software transactional memory for low thread counts. In: Nicolau, A., Shen, X., Amarasinghe, S.P., Vuduc, R.W. (eds.) PPoPP, pp. 113\u2013122. ACM (2013). http:\/\/doi.acm.org\/10.1145\/2442516.2442528"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-92970-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T15:23:28Z","timestamp":1571412208000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-92970-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319929699","9783319929705"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-92970-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}