Skip to Main content Skip to Navigation
Conference papers

Faster Linearizability Checking via P-Compositionality

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.
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-01767332
Contributor : Hal Ifip <>
Submitted on : Monday, April 16, 2018 - 10:18:58 AM
Last modification on : Monday, April 16, 2018 - 10:20:24 AM

File

978-3-319-19195-9_4_Chapter.pd...
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

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⟩

Share

Metrics

Record views

181

Files downloads

236