Aspect-oriented linearizability proofs Journal Article


Author(s): Chakraborty, Soham; Henzinger, Thomas A; Sezgin, Ali; Vafeiadis, Viktor
Article Title: Aspect-oriented linearizability proofs
Affiliation IST Austria
Abstract: Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of 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.
Keywords: verification; linearizability; Concurrency control; Herlihy-wing queue; Queue; Aspect-oriented; Concurrent data structures; Non-blocking; Queue algorithms; Linearization
Journal Title: Logical Methods in Computer Science
Volume: 11
Issue 1
ISSN: 1860-5974
Publisher: International Federation of Computational Logic  
Date Published: 2015-01-01
Start Page: Article number: 20
Copyright Statement: CC BY-ND 2.0
URL:
DOI: 10.2168/LMCS-11(1:20)2015
Notes: The research was supported by the EC FET FP7 project ADVENT, by the Austrian Science Fund NFN RISE (Rigorous Systems Engineering), by the ERC Advanced Grant QUAREM (Quantitative Reactive Modeling), and by the EPSRC Grants EP/H005633/1 and EP/K008528/1.
Open access: yes (OA journal)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
  2.  Ali Sezgin
    5 Sezgin
Related IST Austria Work