{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T08:48:12Z","timestamp":1672562892753},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"4-6","license":[{"start":{"date-parts":[[2012,7,1]],"date-time":"2012-07-01T00:00:00Z","timestamp":1341100800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2012,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Stepwise refinement is a method for systematically transforming a high-level program into an efficiently executable one. A sequence of successively refined programs can also serve as a correctness proof, which makes different mechanisms in the program explicit. We present rules for refinement of multi-threaded shared-variable concurrent programs. We apply our rules to the problem of verifying linearizability of concurrent objects, that are accessed by an unbounded number of concurrent threads. Linearizability is an established correctness criterion for concurrent objects, which states that the effect of each method execution can be considered to occur atomically at some point in time between its invocation and response. We show how linearizability can be expressed in terms of our refinement relation, and present rules for establishing this refinement relation between programs by a sequence of local transformations of method bodies. Contributions include strengthenings of previous techniques for atomicity refinement, as well as an absorption rule, which is particularly suitable for reasoning about concurrent algorithms that implement atomic operations. We illustrate the application of the refinement rules by proving linearizability of Treiber\u2019s concurrent stack algorithm and Michael and Scott\u2019s concurrent queue algorithm.<\/jats:p>","DOI":"10.1007\/s00165-012-0250-7","type":"journal-article","created":{"date-parts":[[2012,6,28]],"date-time":"2012-06-28T08:35:50Z","timestamp":1340872550000},"page":"537-554","source":"Crossref","is-referenced-by-count":6,"title":["Using refinement calculus techniques to prove linearizability"],"prefix":"10.1145","volume":"24","author":[{"given":"Bengt","family":"Jonsson","sequence":"first","affiliation":[{"name":"Department of IT, Uppsala University, Box 337, 751 05, Uppsala, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00291051"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Back RJR (1989) A method for refining atomicity in parallel algorithms. In:PARLE \u201989. Proceedings of parallel architectures and languages Europe. LNCS vol 366. Springer Berlin pp 199\u2013216","DOI":"10.1007\/3-540-51285-3_42"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bingham JD Rakamaric Z (2006) A logic and decision procedure for predicate abstraction of heap-manipulating programs. In: Proc VMCAI. LNCS vol 3855. Springer Berlin pp 207\u2013221","DOI":"10.1007\/11609773_14"},{"issue":"1","key":"e_1_2_1_2_4_2","first-page":"133","article-title":"Stepwise refinement of parallel algorithms","volume":"13","author":"Back RJR","year":"1989","journal-title":"Sci Comput Program"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Chandy KM Misra J (1988) Parallel program design: a foundation. Addison-Wesley","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Doherty S Detlefs D Groves L Flood CH Luchangco V Martin PA Moir M Shavit N Steele GL Jr (2004) DCAS is not a silver bullet for nonblocking algorithm design. In: SPAA 2004: Proceedings of 16th annual ACM symposium on parallel algorithms Barcelona Spain. ACM New York pp 216\u2013224","DOI":"10.1145\/1007912.1007945"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Elmas T Qadeer S Sezgin A Subasi O Tasiran S (2010) Simplifying linearizability proofs with reduction and abstraction. In: Esparza J Majumdar R (eds) Proceedings of TACAS \u201910 16th international conference on tools and algorithms for the construction and analysis of systems. LNCS vol 6015. Springer Berlin pp 296\u2013311","DOI":"10.1007\/978-3-642-12002-2_25"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2004.3.6.a4"},{"key":"e_1_2_1_2_9_2","unstructured":"Groves L (2008) Verifying Michael and Scott\u2019s lock-free queue algorithm using trace reduction. In: Harland J Manyem P (eds) Proceedings of CATS 2008: 14th computing: The Australasian theory symposium Wollongong NSW Australia. CRPIT vol 77. Australian Computer Society pp 133\u2013142"},{"issue":"1","key":"e_1_2_1_2_10_2","first-page":"72","article-title":"Reasoning about nonblocking concurrency","volume":"15","author":"Groves L","year":"2009","journal-title":"J UCS"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/174662.174665"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01786631"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Lynch NA Tuttle MR (1987) Hierarchical correctness proofs for distributed algorithms. In: Proceedings of 6th ACM symposium on principles of distributed computing Vancouver Canada. ACM New York pp 137\u2013151","DOI":"10.1145\/41840.41852"},{"key":"e_1_2_1_2_16_2","unstructured":"Morgan C (1990) Programming from specifications. Prentice-Hall"},{"key":"e_1_2_1_2_17_2","unstructured":"Michael MM Scott M (1995) Correction of a memory management method for lock-free data structures. Technical report TR599 University of Rochester Rochester NY USA"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Michael MM Scott M (1996) Simple fast and practical non-blocking and blocking concurrent queue algorithms. In: Proceedings of 15th ACM symposium on principles of distributed computing. ACM New York pp 267\u2013275","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_1_2_19_2","unstructured":"Treiber RK (1986) Systems programming: coping with parallelism. Technical report RJ5118 IBM Almaden Res. Ctr"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Wang L Stoller SD (2005) Static analysis of atomicity for programs with non-blocking synchronization. In: PPOPP Proceedings of ACM SIGPLAN symposium on principles and practice of parallel programming. ACM New York pp 61\u201371","DOI":"10.1145\/1065944.1065953"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0250-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0250-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0250-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:02:25Z","timestamp":1641484945000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0250-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":20,"journal-issue":{"issue":"4-6","published-print":{"date-parts":[[2012,7]]}},"alternative-id":["10.1007\/s00165-012-0250-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0250-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7]]}}}