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
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, April 16, 2018 - 10:18:58 AM
Last modification on : Monday, April 16, 2018 - 10:20:24 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



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⟩



Record views


Files downloads