Aspect-oriented linearizability proofs

T.A. Henzinger, A. Sezgin, V. Vafeiadis, 8052 (2013) 242–256.

Download
OA 337.06 KB

Conference Paper | Published | English
Department
Series Title
LNCS
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.
Publishing Year
Date Published
2013-08-01
Acknowledgement
The research was supported by the EC FET FP7 project ADVENT,
Volume
8052
Page
242 - 256
Conference
CONCUR: Concurrency Theory
Conference Location
Buenos Aires, Argentina
Conference Date
2013-08-27 – 2013-08-30
IST-REx-ID

Cite this

Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability proofs. 2013;8052:242-256. doi:10.1007/978-3-642-40184-8_18
Henzinger, T. A., Sezgin, A., & Vafeiadis, V. (2013). Aspect-oriented linearizability proofs. Presented at the CONCUR: Concurrency Theory, Buenos Aires, Argentina: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/978-3-642-40184-8_18
Henzinger, Thomas A, Ali Sezgin, and Viktor Vafeiadis. “Aspect-Oriented Linearizability Proofs.” Lecture Notes in Computer Science. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. https://doi.org/10.1007/978-3-642-40184-8_18.
T. A. Henzinger, A. Sezgin, and V. Vafeiadis, “Aspect-oriented linearizability proofs,” vol. 8052. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 242–256, 2013.
Henzinger TA, Sezgin A, Vafeiadis V. 2013. Aspect-oriented linearizability proofs. 8052, 242–256.
Henzinger, Thomas A., et al. Aspect-Oriented Linearizability Proofs. Vol. 8052, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 242–56, doi:10.1007/978-3-642-40184-8_18.
Main File(s)
Access Level
OA Open Access
Last Uploaded
2018-12-12T10:08:58Z


Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar