Aspect-oriented linearizability proofs

S. Chakraborty, T.A. Henzinger, A. Sezgin, V. Vafeiadis, Logical Methods in Computer Science 11 (2015) 20.

Download
OA 380.20 KB

Journal Article | Published | English
Author
; ; ;
Department
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.
Publishing Year
Date Published
2015-04-01
Journal Title
Logical Methods in Computer Science
Acknowledgement
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.
Volume
11
Issue
1
Article Number
20
IST-REx-ID

Cite this

Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability proofs. Logical Methods in Computer Science. 2015;11(1):20. doi:10.2168/LMCS-11(1:20)2015
Chakraborty, S., Henzinger, T. A., Sezgin, A., & Vafeiadis, V. (2015). Aspect-oriented linearizability proofs. Logical Methods in Computer Science, 11(1), 20. https://doi.org/10.2168/LMCS-11(1:20)2015
Chakraborty, Soham, Thomas A Henzinger, Ali Sezgin, and Viktor Vafeiadis. “Aspect-Oriented Linearizability Proofs.” Logical Methods in Computer Science 11, no. 1 (2015): 20. https://doi.org/10.2168/LMCS-11(1:20)2015.
S. Chakraborty, T. A. Henzinger, A. Sezgin, and V. Vafeiadis, “Aspect-oriented linearizability proofs,” Logical Methods in Computer Science, vol. 11, no. 1, p. 20, 2015.
Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. 2015. Aspect-oriented linearizability proofs. Logical Methods in Computer Science. 11(1), 20.
Chakraborty, Soham, et al. “Aspect-Oriented Linearizability Proofs.” Logical Methods in Computer Science, vol. 11, no. 1, International Federation of Computational Logic, 2015, p. 20, doi:10.2168/LMCS-11(1:20)2015.
All files available under the following license(s):
Creative Commons License:
CC-BY-NDCreative Commons Attribution-NoDerivates (CC BY-ND 4.0)
Main File(s)
Access Level
OA Open Access
Last Uploaded
2018-12-12T10:11:27Z


Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar