{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:11Z","timestamp":1740109091762,"version":"3.37.3"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2018,9,1]],"date-time":"2018-09-01T00:00:00Z","timestamp":1535760000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/N016661\/1"],"award-info":[{"award-number":["EP\/N016661\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/M017044\/1"],"award-info":[{"award-number":["EP\/M017044\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Software transactional memory (STM) provides programmers with a high-level programming abstraction for synchronization of parallel processes, allowing blocks of codes that execute in an interleaved manner to be treated as atomic blocks. This atomicity property is captured by a correctness criterion called\n            <jats:italic>opacity<\/jats:italic>\n            , which relates the behaviour of an STM implementation to those of a sequential atomic specification. In this paper, we prove opacity of a recently proposed STM implementation: the Transactional Mutex Lock (TML) by Dalessandro et\u00a0al. For this, we employ two different methods: the first method directly shows all histories of TML to be opaque (proof by induction), using a linearizability proof of TML as an assistance; the second method shows TML to be a refinement of an existing intermediate specification called TMS2 which is known to be opaque (proof by simulation). Both proofs are carried out within interactive provers, the first with KIV and the second with both Isabelle and KIV. This allows to compare not only the proof techniques in principle, but also their complexity in mechanization. It turns out that the second method, already leveraging an existing proof of opacity of TMS2, allows the proof to be decomposed into two independent proofs in the way that the linearizability proof does not.\n          <\/jats:p>","DOI":"10.1007\/s00165-017-0433-3","type":"journal-article","created":{"date-parts":[[2017,8,21]],"date-time":"2017-08-21T07:34:56Z","timestamp":1503300896000},"page":"597-625","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Mechanized proofs of opacity: a comparison of two techniques"],"prefix":"10.1145","volume":"30","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[{"name":"Department of Computing, University of Sheffield, Sheffield, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Doherty","sequence":"additional","affiliation":[{"name":"Department of Computing, University of Sheffield, Sheffield, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Brunel University, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Universit\u00e4t Augsburg, 86135, Augsburg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oleg","family":"Travkin","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Universit\u00e4t Paderborn, 33098, Paderborn, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Universit\u00e4t Paderborn, 33098, Paderborn, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Attiya H Gotsman A Hans S Rinetzky N (2013) A programming language perspective on transactional memory consistency. In: Fatourou P Taubenfeld G (eds) PODC\u201913. ACM pp 309\u2013318","DOI":"10.1145\/2484239.2484267"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Attiya H Gotsman A Hans S Rinetzky N (2014) Safety of live transactions in transactional memory: TMS is necessary and sufficient. In: Kuhn F (ed) DISC volume 8784 of LNCS. Springer pp 376\u2013390","DOI":"10.1007\/978-3-662-45174-8_26"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Anand AS Shyamasundar RK Peri S (2016) Opacity proof for CaPR+ algorithm. In: Proceedings of the 17th international conference on distributed computing and networking ICDCN \u201916 New York NY USA. ACM pp 16:1\u201316:4","DOI":"10.1145\/2833312.2833445"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Cristal A Kulahcioglu Ozkan B Cohen E Kestor G Kuru I Unsal OS Tasiran S Mutluergil SO Elmas T (2015) Verification tools for transactional programs. In: Guerraoui R Romano P (eds) Transactional memory. Foundations algorithms tools and applications\u2014COST Action Euro-TM IC1001 volume 8913 of lecture notes in computer science. Springer pp 283\u2013306","DOI":"10.1007\/978-3-319-14720-8_14"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Cohen A O\u2019Leary JW Pnueli A Tuttle MR Zuck LD (2007) Verifying correctness of transactional memories. In: FMCAD Washington DC USA. IEEE Computer Society pp 37\u201344","DOI":"10.1109\/FAMCAD.2007.40"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/2796550"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Dalessandro L Dice D Scott ML Shavit N Spear MF (2010) Transactional mutex locks. In: D\u2019Ambra P Guarracino MR Talia D (eds) Euro-Par (2) volume 6272 of LNCS. Springer pp 2\u201313","DOI":"10.1007\/978-3-642-15291-7_2"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Derrick J Dongol B Schellhorn G Travkin O Wehrheim H (2015) Verifying opacity of a transactional mutex lock. In: FM volume 9109 of LNCS. Springer pp 161\u2013177","DOI":"10.1007\/978-3-319-19249-9_11"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Doherty S Groves L Luchangco V Moir M (2004) Formal verification of a practical lock-free queue algorithm. In: FORTE volume 3235 of LNCS. Springer pp 97\u2013114","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0225-8"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Dice D Shalev O Shavit N (2006) Transactional locking II. In: Dolev S (ed) DISC volume 4167 of LNCS. Springer pp 194\u2013208","DOI":"10.1007\/11864219_14"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Dalessandro L Spear MF Scott ML (2010) Norec: streamlining STM by abolishing ownership records. In: Govindarajan R Padua DA Hall MW (eds) PPoPP. ACM pp 67\u201378","DOI":"10.1145\/1837853.1693464"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Derrick J Schellhorn G Wehrheim H (2011) Verifying linearisabilty with potential linearisation points. In: Proceedings formal methods (FM) LNCS 6664. Springer pp 323\u2013337","DOI":"10.1007\/978-3-642-21437-0_25"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/1809028.1806613"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Ernst G Pf\u00e4hler J Schellhorn G Haneberg D Reif W (2015) KIV: overview and VerifyThis competition. Int J Softw Tools Technol Transfer 17(6):677\u2013694. doi:10.1007\/s10009-014-0308-3","DOI":"10.1007\/s10009-014-0308-3"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Guerraoui R Henzinger TA Singh V (2008) Completeness and nondeterminism in model checking transactional memories. In: van Breugel F Chechik M (eds) CONCUR. Springer pp 21\u201335","DOI":"10.1007\/978-3-540-85361-9_6"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00446-009-0092-6"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Guerraoui R Kapalka M (2008) On the correctness of transactional memory. In: Chatterjee S Scott ML (eds) PPOPP. ACM pp 175\u2013184","DOI":"10.1145\/1345206.1345233"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Guerraoui R Kapalka M (2010) Principles of transactional memory. Synthesis lectures on distributed computing theory. Morgan & Claypool Publishers San Rafael","DOI":"10.2200\/S00253ED1V01Y201009DCT004"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Herlihy M Luchangco V Moir M Scherer III WN (2003) Software transactional memory for dynamic-sized data structures. In: PODC. ACM pp 92\u2013101","DOI":"10.1145\/872035.872048"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Harris T Larus JR Rajwar R (2010) Transactional memory. In: Synthesis lectures on computer architecture 2nd edn. Morgan & Claypool Publishers San Rafael","DOI":"10.2200\/S00272ED1V01Y201006CAC011"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.04.037"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_2_25_2","unstructured":"Lesani M (2014) On the correctness of transactional memory algorithms. Ph.D. thesis UCLA"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Lesani M Luchangco V Moir M (2012) A framework for formally verifying software transactional memory algorithms. In: Koutny M Ulidowski I (eds) CONCUR 2012. Springer Berlin pp 516\u2013530","DOI":"10.1007\/978-3-642-32940-1_36"},{"key":"e_1_2_1_2_27_2","unstructured":"Lesani M Luchangco V Moir M (2012) Putting opacity in its place. In: Workshop on the theory of transactional memory"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Lesani M Palsberg J (2013) Proving non-opacity. In: Afek Y (ed) DISC volume 8205 of LNCS. Springer pp 106\u2013120","DOI":"10.1007\/978-3-642-41527-2_8"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Lesani M Palsberg J (2014) Decomposing opacity. In: Kuhn F (ed) DISC volume 8784 of LNCS. Springer pp 391\u2013405","DOI":"10.1007\/978-3-662-45174-8_27"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Lynch NA Tuttle MR (1987) Hierarchical correctness proofs for distributed algorithms. In: PODC New York NY USA. ACM pp 137\u2013151","DOI":"10.1145\/41840.41852"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-010-9369-2"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"M\u00fcller O (1998) I\/O Automata and beyond: temporal logic and abstraction in Isabelle. In: Grundy J Newey M (eds) TPHOLs. Springer Berlin pp 331\u2013348","DOI":"10.1007\/BFb0055145"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Nipkow T Paulson LC Wenzel M (2002) Isabelle\/HOL\u2014 a proof assistant for higher-order logic volume 2283 of LNCS. Springer","DOI":"10.1007\/3-540-45949-9"},{"key":"#cr-split#-e_1_2_1_2_35_2.1","doi-asserted-by":"crossref","unstructured":"Owre S Rushby JM Shankar N (1992) PVS: A prototype verification system. In: Kapur D","DOI":"10.1007\/3-540-55602-8_217"},{"key":"#cr-split#-e_1_2_1_2_35_2.2","unstructured":"(ed) Automated deduction-CADE-11 11th international conference on automated deduction Saratoga Springs NY USA June 15-18 1992 proceedings volume 607 of LNCS. Springer pp 748-752"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/322154.322158"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Schellhorn G Derrick J Wehrheim H (2014) A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans Comput Log 15(4):31:1\u201331:37","DOI":"10.1145\/2629496"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Spear MF Michael MM von Praun C (2008) RingSTM: scalable transactions with a single atomic instruction. In: Proceedings of the twentieth annual symposium on parallelism in algorithms and architectures. ACM pp 275\u2013284","DOI":"10.1145\/1378533.1378583"},{"key":"e_1_2_1_2_39_2","unstructured":"Verification of opacity of a Transactional Mutex Lock with KIV and Isabelle 2016. http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/Opacity-TML.html"},{"key":"e_1_2_1_2_40_2","unstructured":"Vafeiadis V (2007) Modular fine-grained concurrency verification. Ph.D. thesis University of Cambridge"},{"key":"e_1_2_1_2_41_2","unstructured":"Wenzel M (2002) Isabelle\/Isar-a versatile environment for human-readable formal proof documents. Ph.D. thesis Institut f\u00fcr Informatik Technische Universit\u00e4t M\u00fcnchen"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0433-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0433-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0433-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0433-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:19:48Z","timestamp":1641485988000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0433-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9]]},"references-count":42,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,9]]}},"alternative-id":["10.1007\/s00165-017-0433-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0433-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2018,9]]}}}