LIPIcs.CONCUR.2023.30.pdf
- Filesize: 0.83 MB
- 16 pages
Document
Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack
Authors
Jesús Domínguez 
,
Aleksandar Nanevski
-
Part of:
Volume:
34th International Conference on Concurrency Theory (CONCUR 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-09-07
File
Document Identifiers
Author Details
Cite As Get BibTex
Jesús Domínguez and Aleksandar Nanevski. Visibility and Separability for a Declarative Linearizability Proof of the Timestamped Stack. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.30
Abstract
Linearizability is a standard correctness criterion for concurrent algorithms, typically proved by establishing the algorithms' linearization points (LP). However, LPs often hinder abstraction, and for some algorithms such as the timestamped stack, it is unclear how to even identify their LPs. In this paper, we show how to develop declarative proofs of linearizability by foregoing LPs and instead employing axiomatization of so-called visibility relations. While visibility relations have been considered before for the timestamped stack, our study is the first to show how to derive the axiomatization systematically and intuitively from the sequential specification of the stack. In addition to the visibility relation, a novel separability relation emerges to generalize real-time precedence of procedure invocation. The visibility and separability relations have natural definitions for the timestamped stack, and enable a novel proof that reduces the algorithm to a simplified form where the timestamps are generated atomically.
Subject Classification
ACM Subject Classification
- Theory of computation → Program verification
Keywords
- Linearizability
- Visibility Relations
- Timestamped Stack
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Suha Orhun Mutluergil. Proving linearizability using forward simulations. In Computer Aided Verification (CAV), pages 542-563, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_28.
- Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. Aspect-oriented linearizability proofs. Logical Methods in Computer Science (LMCS), 11(1), 2015. URL: https://doi.org/10.2168/LMCS-11(1:20)2015.
- Mike Dodds, Andreas Haas, and Christoph M. Kirsch. A scalable, correct time-stamped stack. In Symposium on Principles of Programming Languages (POPL), pages 233-246, 2015. URL: https://doi.org/10.1145/2676726.2676963.
- Jesús Domínguez and Aleksandar Nanevski. Declarative linearizability proofs for descriptor-based concurrent helping algorithms. URL: https://arxiv.org/abs/2307.04653.
- Jesús Domínguez and Aleksandar Nanevski. Visibility and separability for a declarative linearizability proof of the timestamped stack: Extended version. URL: https://arxiv.org/abs/2307.04720.
- Michael Emmi and Constantin Enea. Weak-consistency specification via visibility relaxation. Proc. ACM Program. Lang., 3(POPL):60:1-60:28, 2019. URL: https://doi.org/10.1145/3290373.
- Andreas Haas. Fast Concurrent Data Structures Through Timestamping. PhD thesis, University of Salzburg, 2015. URL: https://www.cs.uni-salzburg.at/~ahaas/papers/thesis.pdf.
- Timothy L. Harris, Keir Fraser, and Ian A. Pratt. A practical multi-word compare-and-swap operation. In International Symposium on Distributed Computing (DISC), pages 265-279, 2002. URL: https://doi.org/10.1007/3-540-36108-1_18.
- Danny Hendler, Nir Shavit, and Lena Yerushalmi. A scalable lock-free stack algorithm. In Symposium on Parallelism in Algorithms and Architectures (SPAA), pages 206-215, 2004. URL: https://doi.org/10.1145/1007912.1007944.
- Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. Aspect-oriented linearizability proofs. In International Conference on Concurrency Theory (CONCUR), pages 242-256, 2013. URL: https://doi.org/10.1007/978-3-642-40184-8_18.
- Maurice P. Herlihy and Jeannette M. Wing. Linearizability: a correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems (TOPLAS), 12(3):463-492, 1990. URL: https://doi.org/10.1145/78969.78972.
- Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew Parkinson. Proving linearizability using partial orders. In European Symposium on Programming (ESOP), pages 639-667, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_24.
- Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. Repairing sequential consistency in C/C++11. In Conference on Programming Language Design and Implementation (PLDI), pages 618-632, 2017. URL: https://doi.org/10.1145/3062341.3062352.
- Joakim Öhman and Aleksandar Nanevski. Visibility reasoning for concurrent snapshot algorithms. Proc. ACM Program. Lang., 6(POPL):33:1-33:30, 2022. URL: https://doi.org/10.1145/3498694.
- Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis. On library correctness under weak memory consistency: Specifying and verifying concurrent libraries under declarative consistency models. Proc. ACM Program. Lang., 3(POPL), 2019. URL: https://doi.org/10.1145/3290381.
- Gerhard Schellhorn, John Derrick, and Heike Wehrheim. A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Logic, 15(4), 2014. URL: https://doi.org/10.1145/2629496.
- Paolo Viotti and Marko Vukolić. Consistency in non-transactional distributed storage systems. ACM Comput. Surv., 49(1):19:1-19:34, 2016. URL: https://doi.org/10.1145/2926965.