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. © 2014 Springer International Publishing.
CITATION STYLE
Guerraoui, R., & Ruppert, E. (2014). Linearizability is not always a safety property. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8593 LNCS, pp. 57–69). Springer Verlag. https://doi.org/10.1007/978-3-319-09581-3_5
Mendeley helps you to discover research relevant for your work.