Bouajjani, Ahmed ;
Emmi, Michael ;
Enea, Constantin ;
Hamza, Jad
Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk)
Abstract
Efficient implementations of concurrent objects such as semaphores, locks, and atomic collections including stacks and queues are vital to modern computer systems. Programming them is however error prone. To minimize synchronization overhead between concurrent objectmethod invocations, implementors avoid blocking operations like lock acquisition, allowing methods to execute concurrently. However, concurrency risks unintended interoperation interference. Their correctness is captured by observational refinement which ensures conformance to atomic reference implementations. Formally, given two libraries L_1 and L_2 implementing the methods of some concurrent object, we say L_1 refines L_2 if and only if every computation of every program using L_1 would also be possible were L_2 used instead.
Linearizability, being an equivalent property, is the predominant proof technique for establishing observational refinement: one shows that each concurrent execution has a linearization which is a valid sequential execution according to a specification, given by an abstract data type or atomic reference implementation.
However, checking linearizability is intrinsically hard. Indeed, even in the case where method implementations are finitestate and object specifications are also finitestate, and when a fixed number of threads (invoking methods in parallel) is considered, the linearizability problem is EXPSPACEcomplete, and it becomes undecidable when the number of threads is unbounded. These results show in particular that there is a complexity/decidability gap between the problem of checking linearizability and the problem of
checking reachability (i.e., the dual of checking safety/invariance properties), the latter being, PSPACEcomplete and EXPSPACEcomplete in the above considered cases, respectively.
We address here the issue of investigating cases where tractable reductions of the observational refinement/linearizability problem to the reachability problem, or dually to invariant checking, are possible. Our aim is (1) to develop algorithmic approaches that avoid a systematic exploration of all possible linearizations of all computations, (2) to exploit existing techniques and tools for
efficient invariant checking to check observational refinement, and (3) to establish decidability and complexity results for significant classes of concurrent objects and data structures.
We present two approaches that we have proposed recently. The first approach introduces a parameterized approximation schema for detecting observational refinement violations. This approach exploits a fundamental property of sharedmemory library executions: their histories are interval orders, a special case of partial orders which admit canonical representations in which each operation o is mapped to a positiveintegerbounded interval I(o). Interval orders are equipped with a natural notion of length, which corresponds to the smallest integer constant for which an interval mapping exists. Then, we define a notion of boundedintervallength analysis, and demonstrate its efficiency, in terms of complexity, coverage, and scalability, for detecting observational refinement bugs.
The second approach focuses on a specific class of abstract data types, including common concurrent objects and data structures such as stacks and queues. We show that for this class of objects, the linearizability problem is actually as hard as the controlstate reachability problem. Indeed, we prove that in this case, the
existence of linearizability violations (i.e., finite computations that are not linearizable), can be captured completely by a finite number of finitestate automata, even when an unbounded number of parallel operations is allowed (assuming that libraries are dataindependent).
BibTeX  Entry
@InProceedings{bouajjani_et_al:LIPIcs:2015:5663,
author = {Ahmed Bouajjani and Michael Emmi and Constantin Enea and Jad Hamza},
title = {{Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk)}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897972},
ISSN = {18688969},
year = {2015},
volume = {45},
editor = {Prahladh Harsha and G. Ramalingam},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5663},
URN = {urn:nbn:de:0030drops56638},
doi = {10.4230/LIPIcs.FSTTCS.2015.2},
annote = {Keywords: Concurrent objects, linearizability, verification, bug detection}
}
2015
Keywords: 

Concurrent objects, linearizability, verification, bug detection 
Seminar: 

35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Issue date: 

2015 
Date of publication: 

2015 