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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
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
Identifiers
URN: urn:nbn:se:uu:diva-178092DOI: 10.1007/s00165-012-0250-7ISI: 000305830700008OAI: oai:DiVA.org:uu-178092DiVA: diva2:542105
Projects
UPMARCAutomated verification of highly concurrent Algorithms
Available from: 2012-07-30 Created: 2012-07-27 Last updated: 2017-12-07Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Jonsson, Bengt

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

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 607 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf