Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates

Dragoi, Cezara and Gupta, Ashutosh and Henzinger, Thomas A (2013) Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013., 8044. pp. 174-190. ISSN 978-3-642-39798-1

[img] Text
cav13.pdf - Accepted Version
Available under License All rights reserved.
[IST-2014-195-v1+1]
Download (230Kb)
Official URL: http://link.springer.com/chapter/10.1007/978-3-642...

Abstract

An execution containing operations performing queries or updating a concurrent object is linearizable w.r.t an abstract implementation (called specification) iff for each operation, one can associate a point in time, called linearization point, such that the execution of the operations in the order of their linearization points can be reproduced by the specification. Finding linearization points is particularly difficult when they do not belong to the operations’s actions. This paper addresses this challenge by introducing a new technique for rewriting the implementation of the concurrent object and its specification such that the new implementation preserves all executions of the original one, and its linearizability (w.r.t. the new specification) implies the linearizability of the original implementation (w.r.t. the original specification). The rewriting introduces additional combined methods to obtain a library with a simpler linearizability proof, i.e., a library whose operations contain their linearization points. We have implemented this technique in a prototype, which has been successfully applied to examples beyond the reach of current techniques, e.g., Stack Elimination and Fetch&Add.

Item Type: Article
DOI: 10.1007/978-3-642-39799-8_11
Subjects: 000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems
000 Computer science, knowledge & general works > 000 Computer science, knowledge & systems > 004 Data processing & computer science
Research Group: Henzinger Group
Depositing User: Cezara Dragoi
Date Deposited: 28 Apr 2014 09:08
Last Modified: 26 Apr 2017 13:46
URI: https://repository.ist.ac.at/id/eprint/195

Actions (login required)

View Item View Item