Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Linearizability Is Not Always a Safety Property
 
conference paper

Linearizability Is Not Always a Safety Property

Guerraoui, Rachid  
•
Ruppert, Eric
Noubir, Guevara
•
Raynal, Michel
2014
Proceedings of the Second International Conference, NETYS
Second International Conference, NETYS

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.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

Line_saf_prop_F978-3-319-09581-3_5.pdf

Type

Preprint

Version

Submitted version (Preprint)

Access type

openaccess

Size

229.42 KB

Format

Adobe PDF

Checksum (MD5)

41d2411b453d86e80192ef6072653b9d

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés