Bouajjani, Ahmed
[Verfasser:in];
Emmi, Michael
[Verfasser:in];
Enea, Constantin
[Verfasser:in];
Hamza, Jad
[Verfasser:in]
;
Ahmed Bouajjani and Michael Emmi and Constantin Enea and Jad Hamza
[Mitwirkende:r]
Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk)
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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 object-method invocations, implementors avoid blocking operations like lock acquisition, allowing methods to execute concurrently. However, concurrency risks unintended inter-operation 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 finite-state and object specifications are also finite-state, and when a fixed number of threads (invoking methods in parallel) is considered, the linearizability problem is EXPSPACE-complete, 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, PSPACE-complete and EXPSPACE-complete 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 ...