Aspect-Oriented Linearizability Proofs

Henzinger, Thomas A and Sezgin, Ali and Viktor, Vafeiadis (2013) Aspect-Oriented Linearizability Proofs. In: CONCUR: Concurrency Theor, August 27-30, 2013 , Buenos Aires, Argentina .

[img] Text
main-queue-verification.pdf - Accepted Version
Available under License All rights reserved.
[IST-2014-197-v1+1]
Download (329Kb)
Official URL: http://link.springer.com/chapter/10.1007/978-3-642...

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.

Item Type: Conference or Workshop Item (Paper)
DOI: 10.1007/978-3-642-40184-8_18
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems
000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems > 004 Data processing & computer science
Research Group: Henzinger Group
Depositing User: Cezara Dragoi
Date Deposited: 28 Apr 2014 09:10
Last Modified: 07 Mar 2017 14:02
URI: https://repository.ist.ac.at/id/eprint/197

Actions (login required)

View Item View Item