Linearizability Is Not Always a Safety Property

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.


Editor(s):
Noubir, Guevara
Raynal, Michel
Published in:
Proceedings of the Second International Conference, NETYS, 8593, 57-69
Presented at:
Second International Conference, NETYS, Marrakech, Morocco, May 15-17, 2014
Year:
2014
Publisher:
Cham, Springer International Publishing
Laboratories:




 Record created 2015-05-28, last modified 2018-09-13

Preprint:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)