%0 Conference Proceedings
%T Faster Linearizability Checking via P-Compositionality
%+ University of Oxford
%A Horn, Alex
%A Kroening, Daniel
%Z Part 1: Ensuring Properties of Distributed Systems
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Grenoble, France
%Y Susanne Graf
%Y Mahesh Viswanathan
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9039
%P 50-65
%8 2015-06-02
%D 2015
%R 10.1007/978-3-319-19195-9_4
%K Model Check
%K Decision Procedure
%K Concurrent System
%K Locality Principle
%K Sequential History
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01767332/document
%2 https://inria.hal.science/hal-01767332/file/978-3-319-19195-9_4_Chapter.pdf
%L hal-01767332
%U https://inria.hal.science/hal-01767332
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9039