Aspect-oriented linearizability proofs Conference Paper

Author(s): Henzinger, Thomas A; Sezgin, Ali; Vafeiadis, Viktor
Title: Aspect-oriented linearizability proofs
Title Series: LNCS
Affiliation IST Austria
Abstract: Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on identifying the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof.
Conference Title: CONCUR: Concurrency Theory
Volume: 8052
Conference Dates: August 27-30, 2013
Conference Location: Buenos Aires, Argentina
ISBN: 978-3-95977-017-0
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik  
Date Published: 2013-08-01
Start Page: 242
End Page: 256
Sponsor: The research was supported by the EC FET FP7 project ADVENT, by the Austrian Science Fund NFN RISE (Rigorous Systems Engineering) and by the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling).
DOI: 10.1007/978-3-642-40184-8_18
Notes: We would like to thank the reviewers for their feedback.
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2.  Ali Sezgin
    5 Sezgin
Related IST Austria Work