{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T03:40:59Z","timestamp":1752982859088,"version":"3.41.0"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,8,1]],"date-time":"2014-08-01T00:00:00Z","timestamp":1406851200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2014,8]]},"abstract":"<jats:p>\n            Efficient implementations of data structures such as queues, stacks or hash-tables allow for concurrent access by many processes at the same time. To increase concurrency, these algorithms often completely dispose with locking, or only lock small parts of the structure.\n            <jats:italic>Linearizability<\/jats:italic>\n            is the standard correctness criterion for such a scenario\u2014where a concurrent object is linearizable if all of its operations appear to take effect instantaneously some time between their invocation and return.\n          <\/jats:p>\n          <jats:p>\n            The potential concurrent access to the shared data structure tremendously increases the complexity of the verification problem, and thus current proof techniques for showing linearizability are all tailored to specific types of data structures. In previous work, we have shown how simulation-based proof conditions for linearizability can be used to verify a number of subtle concurrent algorithms. In this article, we now show that conditions based on\n            <jats:italic>backward<\/jats:italic>\n            simulation can be used to show linearizability of\n            <jats:italic>every<\/jats:italic>\n            linearizable algorithm, that is, we show that our proof technique is both sound\n            <jats:italic>and<\/jats:italic>\n            complete. We exemplify our approach by a linearizability proof of a concurrent queue, introduced in Herlihy and Wing's landmark paper on linearizability. Except for their manual proof, none of the numerous other approaches have successfully treated this queue.\n          <\/jats:p>\n          <jats:p>Our approach is supported by a full mechanisation: both the linearizability proofs for case studies like the queue, and the proofs of soundness and completeness have been carried out with an interactive prover, which is KIV.<\/jats:p>","DOI":"10.1145\/2629496","type":"journal-article","created":{"date-parts":[[2014,9,17]],"date-time":"2014-09-17T14:22:25Z","timestamp":1410963745000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures"],"prefix":"10.1145","volume":"15","author":[{"given":"Gerhard","family":"Schellhorn","sequence":"first","affiliation":[{"name":"University of Augsburg, Germany"}]},{"given":"John","family":"Derrick","sequence":"additional","affiliation":[{"name":"University of Sheffield, UK"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[{"name":"University of Paderborn, Germany"}]}],"member":"320","published-online":{"date-parts":[[2014,9,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_1","first-page":"744","article-title":"Formal construction of a non-blocking concurrent queue algorithm (a case study in atomicity)","volume":"11","author":"Abrial J.-R.","year":"2005","unstructured":"J.-R. Abrial and D. Cansell . 2005 . Formal construction of a non-blocking concurrent queue algorithm (a case study in atomicity) . Journal of Universal Computer Science 11 , 5, 744 -- 770 . J.-R. Abrial and D. Cansell. 2005. Formal construction of a non-blocking concurrent queue algorithm (a case study in atomicity). Journal of Universal Computer Science 11, 5, 744--770.","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/153724.153741"},{"volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07)","author":"Amit D.","key":"e_1_2_1_4_1","unstructured":"D. Amit , N. Rinetzky , T. W. Reps , M. Sagiv , and E. Yahav . 2007. Comparison under abstraction for verifying linearizability . In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07) . 477--490. D. Amit, N. Rinetzky, T. W. Reps, M. Sagiv, and E. Yahav. 2007. Comparison under abstraction for verifying linearizability. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07). 477--490."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0103-1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806634"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 14th International Static Analysis Symposium (SAS'07)","volume":"4634","author":"Calcagno C.","unstructured":"C. Calcagno , M. Parkinson , and V. Vafeiadis . 2007. Modular safety checking for fine-grained concurrency . In Proceedings of the 14th International Static Analysis Symposium (SAS'07) . Lecture Notes in Computer Science , Vol. 4634 . Springer, 233--238. C. Calcagno, M. Parkinson, and V. Vafeiadis. 2007. Modular safety checking for fine-grained concurrency. In Proceedings of the 14th International Static Analysis Symposium (SAS'07). Lecture Notes in Computer Science, Vol. 4634. Springer, 233--238."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_41"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.026"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2005.49"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_44"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663079"},{"key":"e_1_2_1_13_1","unstructured":"J. Derrick and E. Boiten. 2001. Refinement in Z and object-Z: Foundations and advanced applications. In Formal Approaches to Computing and Information Technology. Springer. Available at http:\/\/www.cs.kent.ac.uk\/pubs\/2001\/1200.   J. Derrick and E. Boiten. 2001. Refinement in Z and object-Z: Foundations and advanced applications. In Formal Approaches to Computing and Information Technology. Springer. Available at http:\/\/www.cs.kent.ac.uk\/pubs\/2001\/1200."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 10th International Conference of Z Users. Lecture Notes in Computer Science","volume":"1212","author":"Derrick J.","unstructured":"J. Derrick , E. A. Boiten , H. Bowman , and M. Steen . 1997. Weak refinement in Z . In Proceedings of the 10th International Conference of Z Users. Lecture Notes in Computer Science , Vol. 1212 . Springer, 369--388. J. Derrick, E. A. Boiten, H. Bowman, and M. Steen. 1997. Weak refinement in Z. In Proceedings of the 10th International Conference of Z Users. Lecture Notes in Computer Science, Vol. 1212. Springer, 369--388."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68863-1_6"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890001"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 17th International Conference on Formal Methods (FM'11)","volume":"6664","author":"Derrick J.","unstructured":"J. Derrick , G. Schellhorn , and H. Wehrheim . 2011b. Verifying linearisability with potential linearisation points . In Proceedings of the 17th International Conference on Formal Methods (FM'11) . Lecture Notes in Computer Science , Vol. 6664 . Springer, 323--337. J. Derrick, G. Schellhorn, and H. Wehrheim. 2011b. Verifying linearisability with potential linearisation points. In Proceedings of the 17th International Conference on Formal Methods (FM'11). Lecture Notes in Computer Science, Vol. 6664. Springer, 323--337."},{"key":"e_1_2_1_18_1","volume-title":"Lecture Notes in Computer Science","volume":"3235","author":"Doherty S.","unstructured":"S. Doherty , L. Groves , V. Luchangco , and M. Moir . 2004. Formal verification of a practical lock-free queue algorithm. In Formal Techniques for Networked and Distributed Systems (FORTE 2004) . Lecture Notes in Computer Science , Vol. 3235 . Springer, 97--114. S. Doherty, L. Groves, V. Luchangco, and M. Moir. 2004. Formal verification of a practical lock-free queue algorithm. In Formal Techniques for Networked and Distributed Systems (FORTE 2004). Lecture Notes in Computer Science, Vol. 3235. Springer, 97--114."},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the 23rd International Conference on Distributed Computed. Lecture Notes in Computer Science","volume":"5805","author":"Doherty S.","unstructured":"S. Doherty and M. Moir . 2009. Nonblocking algorithms and backward simulation . In Proceedings of the 23rd International Conference on Distributed Computed. Lecture Notes in Computer Science , Vol. 5805 . Springer, 274--288. S. Doherty and M. Moir. 2009. Nonblocking algorithms and backward simulation. In Proceedings of the 23rd International Conference on Distributed Computed. Lecture Notes in Computer Science, Vol. 5805. Springer, 274--288."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_25"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the 21st International Conference on Concurrency Theory. Lecture Notes in Computer Science","volume":"6269","author":"Fu M.","unstructured":"M. Fu , Yong Y. Li , X. Feng , Z. Shao , and Y. Zhang . 2010. Reasoning about optimistic concurrency using a program logic for history . In Proceedings of the 21st International Conference on Concurrency Theory. Lecture Notes in Computer Science , Vol. 6269 . Springer, 388--402. M. Fu, Yong Y. Li, X. Feng, Z. Shao, and Y. Zhang. 2010. Reasoning about optimistic concurrency using a program logic for history. In Proceedings of the 21st International Conference on Concurrency Theory. Lecture Notes in Computer Science, Vol. 6269. Springer, 388--402."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.02.016"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.08.044"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0092-5"},{"volume-title":"Proceedings of the European Symposium on Programming (ESOP'86)","author":"He J.","key":"e_1_2_1_26_1","unstructured":"J. He , C. A. R. Hoare , and J. W. Sanders . 1986. Data refinement refined . In Proceedings of the European Symposium on Programming (ESOP'86) . Springer, 187--196. J. He, C. A. R. Hoare, and J. W. Sanders. 1986. Data refinement refined. In Proceedings of the European Symposium on Programming (ESOP'86). Springer, 187--196."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11795490_3"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_18"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-007-0044-1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.10.003"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the IFIP 9th World Computer Congress (IFIP'83)","author":"Jones C. B.","year":"1983","unstructured":"C. B. Jones . 1983 . Specification and design of (parallel) programs . In Proceedings of the IFIP 9th World Computer Congress (IFIP'83) . 321--332. C. B. Jones. 1983. Specification and design of (parallel) programs. In Proceedings of the IFIP 9th World Computer Congress (IFIP'83). 321--332."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0250-7"},{"key":"e_1_2_1_34_1","volume-title":"Local Proof Obligations and Their Application to the Lazy Set Algorithm. Retrieved","author":"KIV.","year":"2014","unstructured":"KIV. 2010. Verification of Linearizability as Refinement Using Possibilities , Local Proof Obligations and Their Application to the Lazy Set Algorithm. Retrieved July 6, 2014 , from http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/possibilities.html. KIV. 2010. Verification of Linearizability as Refinement Using Possibilities, Local Proof Obligations and Their Application to the Lazy Set Algorithm. Retrieved July 6, 2014, from http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/possibilities.html."},{"key":"e_1_2_1_35_1","volume-title":"Verification of Herlihy & Wing's Queue as an Instance of the Complete Refinement Theory of Linearizability. Retrieved","author":"KIV.","year":"2014","unstructured":"KIV. 2011. Verification of Herlihy & Wing's Queue as an Instance of the Complete Refinement Theory of Linearizability. Retrieved July 6, 2014 , from http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/Herlihy-Wing-queue.html. KIV. 2011. Verification of Herlihy & Wing's Queue as an Instance of the Complete Refinement Theory of Linearizability. Retrieved July 6, 2014, from http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/Herlihy-Wing-queue.html."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_1_37_1","unstructured":"N. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann.   N. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1073970.1074013"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835722"},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"W. Reif G. Schellhorn K. Stenzel and M. Balser. 1998. Structured specifications and interactive proofs with KIV. In Automated Deduction\u2014A Basis for Applications Vol. II. Kluwer 13--39.  W. Reif G. Schellhorn K. Stenzel and M. Balser. 1998. Structured specifications and interactive proofs with KIV. In Automated Deduction\u2014A Basis for Applications Vol. II. Kluwer 13--39.","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.003"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2009.10.004"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-013-9389-z"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_21"},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the 10th International Conference on Mathematics of Program Construction (MPC'10)","volume":"6120","author":"Tofan B.","unstructured":"B. Tofan , S. B\u00e4umler , G. Schellhorn , and W. Reif . 2010. Temporal logic verification of lock-freedom . In Proceedings of the 10th International Conference on Mathematics of Program Construction (MPC'10) . Lecture Notes in Computer Science , Vol. 6120 . Springer, 377--396. B. Tofan, S. B\u00e4umler, G. Schellhorn, and W. Reif. 2010. Temporal logic verification of lock-freedom. In Proceedings of the 10th International Conference on Mathematics of Program Construction (MPC'10). Lecture Notes in Computer Science, Vol. 6120. Springer, 377--396."},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of the 8th International Conference on Theoretical Aspects of Computing (ICTAC'11)","volume":"6916","author":"Tofan B.","unstructured":"B. Tofan , G. Schellhorn , and W. Reif . 2011. Formal verification of a lock-free stack with hazard pointers . In Proceedings of the 8th International Conference on Theoretical Aspects of Computing (ICTAC'11) . Lecture Notes in Computer Science , Vol. 6916 . Springer, 239--255. B. Tofan, G. Schellhorn, and W. Reif. 2011. Formal verification of a lock-free stack with hazard pointers. In Proceedings of the 8th International Conference on Theoretical Aspects of Computing (ICTAC'11). Lecture Notes in Computer Science, Vol. 6916. Springer, 239--255."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.04.001"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the 12th International Workshop on Automated Verification of Critical Systems (AVoCS'12)","volume":"53","author":"Travkin O.","unstructured":"O. Travkin , H. Wehrheim , and G. Schellhorn . 2012. Proving linearizability of multiset with local proof obligations . In Proceedings of the 12th International Workshop on Automated Verification of Critical Systems (AVoCS'12) . Automated Verification of Critical Systems , Vol. 53 , ECEASST, 1--15. O. Travkin, H. Wehrheim, and G. Schellhorn. 2012. Proving linearizability of multiset with local proof obligations. In Proceedings of the 12th International Workshop on Automated Verification of Critical Systems (AVoCS'12). Automated Verification of Critical Systems, Vol. 53, ECEASST, 1--15."},{"key":"e_1_2_1_51_1","volume-title":"System Programming: Coping with Parallelism. Technical Report RJ 5118","author":"Treiber R. K.","year":"1986","unstructured":"R. K. Treiber . 1986 . System Programming: Coping with Parallelism. Technical Report RJ 5118 . IBM Almaden Research Center . R. K. Treiber. 1986. System Programming: Coping with Parallelism. Technical Report RJ 5118. IBM Almaden Research Center."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926415"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1122992"},{"key":"e_1_2_1_56_1","unstructured":"J. C. P. Woodcock and J. Davies. 1996. Using Z: Specification Refinement and Proof. Prentice Hall.   J. C. P. Woodcock and J. Davies. 1996. Using Z: Specification Refinement and Proof. Prentice Hall."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629496","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2629496","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:01:17Z","timestamp":1750230077000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629496"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,8]]},"references-count":55,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["10.1145\/2629496"],"URL":"https:\/\/doi.org\/10.1145\/2629496","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2014,8]]},"assertion":[{"value":"2013-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-09-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}