{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T13:28:31Z","timestamp":1725888511023},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319602240"},{"type":"electronic","value":"9783319602257"}],"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-60225-7_4","type":"book-chapter","created":{"date-parts":[[2017,5,27]],"date-time":"2017-05-27T02:26:37Z","timestamp":1495851997000},"page":"50-66","source":"Crossref","is-referenced-by-count":8,"title":["Proving Opacity via Linearizability: A Sound and Complete Method"],"prefix":"10.1007","author":[{"given":"Alasdair","family":"Armstrong","sequence":"first","affiliation":[]},{"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[]},{"given":"Simon","family":"Doherty","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,5,28]]},"reference":[{"issue":"6","key":"4_CR1","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1109\/71.242161","volume":"4","author":"SV Adve","year":"1993","unstructured":"Adve, S.V., Aggarwal, J.K.: A unified formalization of four shared-memory models. IEEE Trans. Parallel Distrib. Syst. 4(6), 613\u2013624 (1993)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"4_CR2","unstructured":"Armstrong, A., Dongol, B., Doherty, S.: Reducing opacity to linearizability: a sound and complete method. arXiv e-prints (October 2016). https:\/\/arxiv.org\/abs\/1610.01004"},{"key":"4_CR3","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":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-662-47666-6_8","volume-title":"Automata, Languages, and Programming","author":"A Bouajjani","year":"2015","unstructured":"Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: On reducing linearizability to state reachability. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 95\u2013107. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-47666-6_8"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-642-14295-6_41","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2010","unstructured":"\u010cern\u00fd, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model Checking of linearizability of concurrent list implementations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 465\u2013479. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14295-6_41"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Chakraborty, S., Henzinger, T.A., Sezgin, A., Vafeiadis, V.: Aspect-oriented linearizability proofs. Logical Methods Comput. Sci. 11(1) (2015)","DOI":"10.2168\/LMCS-11(1:20)2015"},{"key":"4_CR7","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":"4_CR8","doi-asserted-by":"crossref","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)","DOI":"10.1145\/1693453.1693464"},{"key":"4_CR9","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":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30232-2_7","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"S Doherty","year":"2004","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a\u00a0practical lock-free queue algorithm. In: Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97\u2013114. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-30232-2_7"},{"issue":"5","key":"4_CR11","doi-asserted-by":"crossref","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. 25(5), 769\u2013799 (2013)","journal-title":"Formal Asp. Comput."},{"issue":"2","key":"4_CR12","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1145\/2796550","volume":"48","author":"B Dongol","year":"2015","unstructured":"Dongol, B., Derrick, J.: Verifying linearisability: a comparative survey. ACM Comput. Surv. 48(2), 19 (2015)","journal-title":"ACM Comput. Surv."},{"issue":"3","key":"4_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\u2013145 (2010)","journal-title":"Distrib. Comput."},{"key":"4_CR14","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":"4_CR15","series-title":"Synthesis Lectures on Distributed Computing Theory","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02002-5","volume-title":"Principles of Transactional Memory","author":"R Guerraoui","year":"2010","unstructured":"Guerraoui, R., Kapalka, M.: Principles of Transactional Memory. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2010)"},{"key":"4_CR16","series-title":"Synthesis Lectures on Computer Architecture","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-01728-5","volume-title":"Transactional Memory","author":"T Harris","year":"2010","unstructured":"Harris, T., Larus, J.R., Rajwar, R.: Transactional Memory. Synthesis Lectures on Computer Architecture, 2nd edn. Morgan & Claypool Publishers, San Rafael (2010)","edition":"2"},{"issue":"3","key":"4_CR17","doi-asserted-by":"crossref","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 12(3), 463\u2013492 (1990)","journal-title":"ACM TOPLAS"},{"issue":"8","key":"4_CR18","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Koskinen, E., Parkinson, M.: The push\/pull model of transactions. In: PLDI. PLDI 2015, vol. 50, pp. 186\u2013195. ACM, New York, NY, USA, June 2015","DOI":"10.1145\/2737924.2737995"},{"key":"4_CR20","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":"4_CR21","unstructured":"Lesani, M., Luchangco, V., Moir, M.: Putting opacity in its place. In: Workshop on the Theory of Transactional Memory (2012)"},{"key":"4_CR22","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"},{"issue":"7","key":"4_CR23","doi-asserted-by":"crossref","first-page":"1018","DOI":"10.1109\/TSE.2012.82","volume":"39","author":"Y Liu","year":"2013","unstructured":"Liu, Y., Chen, W., Liu, Y.A., Sun, J., Zhang, S.J., Dong, J.S.: Verifying linearizability via optimized refinement checking. IEEE Trans. Softw. Eng. 39(7), 1018\u20131039 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-14107-2_23","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"S Owens","year":"2010","unstructured":"Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 478\u2013503. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-14107-2_23"},{"issue":"4","key":"4_CR25","doi-asserted-by":"crossref","first-page":"31:1","DOI":"10.1145\/2629496","volume":"15","author":"G Schellhorn","year":"2014","unstructured":"Schellhorn, G., Derrick, J., Wehrheim, H.: A sound and complete proof technique for linearizability of concurrent data structures. ACM TOCL 15(4), 31:1\u201331:37 (2014)","journal-title":"ACM TOCL"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709\u2013714. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02658-4_59"},{"key":"4_CR27","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis. University of Cambridge (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-60225-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,28]],"date-time":"2022-07-28T22:26:41Z","timestamp":1659047201000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-60225-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319602240","9783319602257"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-60225-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}