Faster Linearizability Checking via P-Compositionality - Formal Techniques for Distributed Objects, Components, and Systems
Conference Papers Year : 2015

Faster Linearizability Checking via P-Compositionality

Alex Horn
  • Function : Author
  • PersonId : 1030895

Abstract

Linearizability is a well-established consistency and correctness criterion for concurrent data types. An important feature of linearizability is Herlihy and Wing’s locality principle, which says that a concurrent system is linearizable if and only if all of its constituent parts (so-called objects) are linearizable. This paper presents P-compositionality, which generalizes the idea behind the locality principle to operations on the same concurrent data type. We implement P-compositionality in a novel linearizability checker. Our experiments with over nine implementations of concurrent sets, including Intel’s TBB library, show that our linearizability checker is one order of magnitude faster and/or more space efficient than the state-of-the-art algorithm.
Fichier principal
Vignette du fichier
978-3-319-19195-9_4_Chapter.pdf (228.74 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-01767332 , version 1 (16-04-2018)

Licence

Identifiers

Cite

Alex Horn, Daniel Kroening. Faster Linearizability Checking via P-Compositionality. 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2015, Grenoble, France. pp.50-65, ⟨10.1007/978-3-319-19195-9_4⟩. ⟨hal-01767332⟩
123 View
88 Download

Altmetric

Share

More