{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T02:12:28Z","timestamp":1712369548477},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"1","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2011,1]]},"abstract":"\n Concurrent objects are inherently complex to verify. In the late 80s and early 90s, Herlihy and Wing proposed\n linearizability<\/jats:italic>\n as a correctness condition for concurrent objects, which, once proven, allows us to reason about concurrent objects using pre- and postconditions only. 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 \n In this article we define simulation-based proof conditions for linearizability and apply them to two concurrent implementations, a lock-free stack and a set with lock-coupling. Similar to other approaches, we employ a theorem prover (here, KIV) to mechanize our proofs. Contrary to other approaches, we also use the prover to mechanically check that our proof obligations actually guarantee linearizability. This check employs the original ideas of Herlihy and Wing of verifying linearizability via\n possibilities<\/jats:italic>\n .\n <\/jats:p>","DOI":"10.1145\/1889997.1890001","type":"journal-article","created":{"date-parts":[[2011,1,24]],"date-time":"2011-01-24T14:58:13Z","timestamp":1295881093000},"page":"1-43","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":41,"title":["Mechanically verified proof obligations for linearizability"],"prefix":"10.1145","volume":"33","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[{"name":"University of Sheffield, Sheffield, UK"}]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[{"name":"Institute for Software and Systems Engineering, Augsburg, Germany"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[{"name":"Institut f\u00fcr Informatik, Paderborn, Germany"}]}],"member":"320","published-online":{"date-parts":[[2011,1,25]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"744","article-title":"Formal construction of a non-blocking concurrent queue algorithm (a case study in atomicity)","volume":"11","author":"Abrial I.-R.","year":"2005","unstructured":"Abrial , I.-R. and Cansell , D. 2005 . Formal construction of a non-blocking concurrent queue algorithm (a case study in atomicity) . J. Univ. Comput. Sci. 11 , 5, 744 -- 770 . Abrial, I.-R. and Cansell, D. 2005. Formal construction of a non-blocking concurrent queue algorithm (a case study in atomicity). J. Univ. Comput. Sci. 11, 5, 744--770.","journal-title":"J. Univ. Comput. Sci."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the International Conference on Computer Aided Verification. W. Damm and H. Hermanns, Eds. Lecture Notes in Computer Science","volume":"4590","author":"Amit D.","unstructured":"Amit , D. , Rinetzky , N. , Reps , T. W. , Sagiv , M. , and Yahav , E . 2007. Comparison under abstraction for verifying linearizability . In Proceedings of the International Conference on Computer Aided Verification. W. Damm and H. Hermanns, Eds. Lecture Notes in Computer Science , vol. 4590 , Springer, 477--490. Amit, D., Rinetzky, N., Reps, T. W., Sagiv, M., and Yahav, E. 2007. Comparison under abstraction for verifying linearizability. In Proceedings of the International Conference on Computer Aided Verification. W. Damm and H. Hermanns, Eds. Lecture Notes in Computer Science, vol. 4590, Springer, 477--490."},{"key":"e_1_2_1_3_1","unstructured":"Barden R. Stepney S. and Cooper D. 1994. Z in Practice. BCS Practitioner Series. Prentice-Hall. Barden R. Stepney S. and Cooper D. 1994. Z in Practice. BCS Practitioner Series. Prentice-Hall."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_2_1_5_1","unstructured":"B\u00e4umler S. Schellhorn G. Tofan B. and Reif W. 2009. Proving linearizability with temporal logic. Form. Asp. Comput. B\u00e4umler S. Schellhorn G. Tofan B. and Reif W. 2009. Proving linearizability with temporal logic. Form. Asp. Comput."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00263762"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391451.2391468"},{"key":"e_1_2_1_8_1","series-title":"Lecture Notes in Computer Science","volume-title":"CASL Reference Manual","author":"Co FI.","unstructured":"Co FI. 2004. CASL Reference Manual . Lecture Notes in Computer Science , vol. 2960 , (IFIP Series). Springer . CoFI. 2004. CASL Reference Manual. Lecture Notes in Computer Science, vol. 2960, (IFIP Series). Springer."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 9th International Conference on Concurrency Theory (CONCUR'98)","author":"Cohen E.","unstructured":"Cohen , E. and Lamport , L . 1998. Reduction in TLA . In Proceedings of the 9th International Conference on Concurrency Theory (CONCUR'98) . Springer-Verlag, 317--331. Cohen, E. and Lamport, L. 1998. Reduction in TLA. In Proceedings of the 9th International Conference on Concurrency Theory (CONCUR'98). Springer-Verlag, 317--331."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.026"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663079"},{"key":"e_1_2_1_12_1","doi-asserted-by":"crossref","unstructured":"Derrick J. and Boiten E. 2001. Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer. Derrick J. and Boiten E. 2001. Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer.","DOI":"10.1007\/978-1-4471-0257-1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Derrick J. Schellhorn G. and \n Wehrheim H\n . \n 2007\n . Proving linearizability via non-atomic refinement. In Proceedings of the 6th International Conference on Integrated Formal Methods. J. Davies and J. Gibbons Eds. Lecture Notes in Computer Science vol. \n 4591 Springer 195--214. Derrick J. Schellhorn G. and Wehrheim H. 2007. Proving linearizability via non-atomic refinement. In Proceedings of the 6th International Conference on Integrated Formal Methods. J. Davies and J. Gibbons Eds. Lecture Notes in Computer Science vol. 4591 Springer 195--214.","DOI":"10.1007\/978-3-540-73210-5_11"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68863-1_6"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1761968.1761978"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11415787_3"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/647963.743803"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 16th European Symposium on Programming. Springer, 173--188","author":"Feng X.","unstructured":"Feng , X. , Ferheira , R. , and Shao , Z . 2007. On the relationship between concurrent separation logic and assume-guarantee reasoning . In Proceedings of the 16th European Symposium on Programming. Springer, 173--188 . Feng, X., Ferheira, R., and Shao, Z. 2007. On the relationship between concurrent separation logic and assume-guarantee reasoning. In Proceedings of the 16th European Symposium on Programming. Springer, 173--188."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1767111.1767125"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.10.003"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.08.044"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007944"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41627"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.06.001"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042044"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-006-0020-1"},{"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.1007\/11901433_23"},{"key":"e_1_2_1_32_1","unstructured":"Jones C. B. 1983. Specification and design of (parallel) programs. InProceedings of the International Federation for Information Processing (IFIP'83). North-Holland 321--332. Jones C. B. 1983. Specification and design of (parallel) programs. InProceedings of the International Federation for Information Processing (IFIP'83). North-Holland 321--332."},{"key":"e_1_2_1_33_1","unstructured":"KIV. 2009. Web presentation of the linearization case study in KIV. http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/linearizability2.html. KIV. 2009. Web presentation of the linearization case study in KIV. http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/linearizability2.html."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_35_1","unstructured":"Lamport L. and Schneider F. B. 1989. Pretending atomicity. Tech. rep. TR89-1005 SRC Digital. Lamport L. and Schneider F. B. 1989. Pretending atomicity. Tech. rep. TR89-1005 SRC Digital."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_21"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1998.1446"},{"key":"e_1_2_1_39_1","volume-title":"A reduction theorem for concurrent object-oriented programs","author":"Misra J.","unstructured":"Misra , J. 2003. A reduction theorem for concurrent object-oriented programs . In Programming Methodology. A. McIver and C. Morgan Eds., Springer-Verlag , 69--92. Misra, J. 2003. A reduction theorem for concurrent object-oriented programs. In Programming Methodology. A. McIver and C. Morgan Eds., Springer-Verlag, 69--92."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190261"},{"key":"e_1_2_1_42_1","volume-title":"Systems and Implementation Techniques","author":"Reif W.","year":"1998","unstructured":"Reif , W. , Schellhorn , G. , Stenzel , K. , and Balser , M . 1998 . Structured specifications and interactive proofs with KIV. In Automated Deduction\u2014A Basis for Applications , Vol. II : Systems and Implementation Techniques , W. Bibel and P. Schmitt Eds., Kluwer Academic Publishers , Dordrecht, Chapter 1, 13--39. Reif, W., Schellhorn, G., Stenzel, K., and Balser, M. 1998. Structured specifications and interactive proofs with KIV. In Automated Deduction\u2014A Basis for Applications, Vol. II: Systems and Implementation Techniques, W. Bibel and P. Schmitt Eds., Kluwer Academic Publishers, Dordrecht, Chapter 1, 13--39."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_44_1","volume-title":"The Z Notation: A Reference Manual","author":"Spivey J.","unstructured":"Spivey , J. 1992. The Z Notation: A Reference Manual . Prentice Hall . Spivey, J. 1992. The Z Notation: A Reference Manual. Prentice Hall."},{"key":"e_1_2_1_45_1","volume-title":"Computer Laboratory","author":"Vafeiadis V.","unstructured":"Vafeiadis , V. 2008. Modular fine-grained concurrency verification. Tech. rep. UCAM-CL-TR726 , Computer Laboratory , University of Cambridge . Vafeiadis, V. 2008. Modular fine-grained concurrency verification. Tech. rep. UCAM-CL-TR726, Computer Laboratory, University of Cambridge."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1122992"},{"key":"e_1_2_1_47_1","unstructured":"Vafeiadis V.\n and \n Parkinson M. J\n . \n 2007\n . A marriage of rely\/guarantee and separation logic. In Proceedings of the 18th International Conference on Concurrency Theory (CONCUR'07). L. Caires and V. T. Vasconcelos Eds. Lecture Notes in Computer Science vol. \n 4703 Springer 256--27l. Vafeiadis V. and Parkinson M. J. 2007. A marriage of rely\/guarantee and separation logic. In Proceedings of the 18th International Conference on Concurrency Theory (CONCUR'07). L. Caires and V. T. Vasconcelos Eds. Lecture Notes in Computer Science vol. 4703 Springer 256--27l."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375598"},{"key":"e_1_2_1_49_1","unstructured":"Wang L. and Stoller S. D. 2004. Automated verification of programs with non-blocking synchronization. Tech. rep. DAR-04-17 Computer Science Department SUNY at Stony BroDk. http:\/\/www.cs.sunysb.edu\/~liqiang\/lockfree.html. Wang L. and Stoller S. D. 2004. Automated verification of programs with non-blocking synchronization. Tech. rep. DAR-04-17 Computer Science Department SUNY at Stony BroDk. http:\/\/www.cs.sunysb.edu\/~liqiang\/lockfree.html."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065944.1065953"},{"key":"e_1_2_1_51_1","unstructured":"Woodcock J. C. P. and Davies J. 1996. Using Z: Specification Refinement and Proof. Prentice Hall. Woodcock J. C. P. and Davies J. 1996. Using Z: Specification Refinement and Proof. Prentice Hall."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1889997.1890001","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T18:32:58Z","timestamp":1672338778000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1889997.1890001"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["10.1145\/1889997.1890001"],"URL":"http:\/\/dx.doi.org\/10.1145\/1889997.1890001","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1]]},"assertion":[{"value":"2009-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-01-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}
