Abstract
We show that, in contrast to the general belief in the distributed computing community, linearizability, the celebrated consistency property, is not always a safety property. More specifically, we give an object for which it is possible to have an infinite history that is not linearizable, even though every finite prefix of the history is linearizable. The object we consider as a counterexample has infinite nondeterminism. We show, however, that if we restrict attention to objects with finite nondeterminism, we can use König’s lemma to prove that linearizability is indeed a safety property. In the same vein, we show that the backward simulation technique, which is a classical technique to prove linearizability, is not sound for arbitrary types, but is sound for types with finite nondeterminism.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
For example, an erroneous claim is made in two recent papers [1, 11] that explicitly permit nondeterministic objects and make no restriction that the nondeterminism of the objects should be finite. The latter paper states that “linearizability is a safety property, so its violation can be detected with a finite prefix of an execution history.” Using the definitions given in that paper, this statement is false. However, this does not affect the correctness of that paper’s main results because those results are about objects with finite nondeterminism.
- 2.
In the context of implementations of shared object of type \(T\), observable events are just invocations and responses on the object of type \(T\).
References
Adhikari, K., Street, J., Wang, C., Liu, Y., Zhang, S.J.: Verifying a quantitative relaxation of linearizability via refinement. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 24–42. Springer, Heidelberg (2013)
Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181–185 (1985)
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987)
Apt, K.R., Plotkin, G.D.: A cook’s tour of countable nondeterminism. In: Even, S., Kariv, O. (eds.) Automata, Languages and Programming. LNCS, vol. 115, pp. 479–494. Springer, Heidelberg (1981)
Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set algorithm. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 475–488. Springer, Heidelberg (2006)
Dijkstra, E.W.: On nondeterminacy being bounded. In: Dijkstra, E.W. (ed.) A Discipline of Programming, Chap. 9. Prentice-Hall, Englewood Cliffs (1976)
Doherty, S., Moir, M.: Nonblocking algorithms and backward simulation. In: Keidar, I. (ed.) DISC 2009. LNCS, vol. 5805, pp. 274–288. Springer, Heidelberg (2009)
Herlihy, M.P.: Wait-free synchronization. ACM Trans. Program. Lang. Syst. 13(1), 123–149 (1991)
Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)
König, D.: Über eine Schlussweise aus dem Endlichen ins Unendliche. Acta Litterarum ac Scientiarum Regiae Universitatis Hungaricae Francisco-Josephinae: Sectio Scientiarum Mathematicarum 3, 121–130 (1927). also in chapter VI of Dénes König. Theory of Finite and Infinite Graphs, Birkhäuser, Boston, 1990
Liu, Y., Chen, W., Liu, Y.A., Sun, J., Zhang, S.J., Dong, J.S.: Verifying linearizability via optimized refinement checking. IEEE Trans. Softw. Eng. 39(7), 1018–1039 (2013)
Lynch, N.: Distributed Algorithms, Chap. 13. Morgan Kaufmann, San Mateo (1996)
Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations. Inf. Comput. 121(2), 214–233 (1995)
Schenk, E.: The consensus hierarchy is not robust. In: Proceedings of 16th ACM Symposium on Principles of Distributed Computing, p. 279 (1997)
Acknowledgements
The model section and definition of linearizability are based on lecture notes written by the first author with Michel Raynal and then with Petr Kuznetsov. The proof of Theorem 2 is inspired by a proof by Petr Kuznetsov, itself inspired by a proof by Nancy Lynch [12]. We thank Franck van Breugel for helpful discussions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Guerraoui, R., Ruppert, E. (2014). Linearizability Is Not Always a Safety Property. In: Noubir, G., Raynal, M. (eds) Networked Systems. NETYS 2014. Lecture Notes in Computer Science(), vol 8593. Springer, Cham. https://doi.org/10.1007/978-3-319-09581-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-09581-3_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-09580-6
Online ISBN: 978-3-319-09581-3
eBook Packages: Computer ScienceComputer Science (R0)