uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
Using refinement calculus techniques to prove linearizability
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
2012 (English)In: Formal Aspects of Computing, ISSN 0934-5043, E-ISSN 1433-299X, Vol. 24, no 4-6, 537-554 p.Article in journal (Refereed) Published
Abstract [en]

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's concurrent stack algorithm and Michael and Scott's concurrent queue algorithm.

Place, publisher, year, edition, pages
2012. Vol. 24, no 4-6, 537-554 p.
Keyword [en]
Refinement calculus, Multi-threading, Formal verification, Linearizability
National Category
Computer Science
URN: urn:nbn:se:uu:diva-178092DOI: 10.1007/s00165-012-0250-7ISI: 000305830700008OAI: oai:DiVA.org:uu-178092DiVA: diva2:542105
UPMARCAutomated verification of highly concurrent Algorithms
Available from: 2012-07-30 Created: 2012-07-27 Last updated: 2013-01-07Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Search in DiVA

By author/editor
Jonsson, Bengt
By organisation
Computer Systems
In the same journal
Formal Aspects of Computing
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

Total: 276 hits
ReferencesLink to record
Permanent link

Direct link