License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2017.16
URN: urn:nbn:de:0030-drops-78079
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7807/
Bouajjani, Ahmed ;
Enea, Constantin ;
Wang, Chao
Checking Linearizability of Concurrent Priority Queues
Abstract
Efficient implementations of concurrent objects such as atomic collections are essential to modern computing. Unfortunately their correctness criteria — linearizability with respect to given ADT specifications — are hard to verify. Verifying linearizability is undecidable in general, even on classes of implementations where the usual control-state reachability is decidable. In this work we consider concurrent priority queues which are fundamental to many multi-threaded applications like task scheduling or discrete event simulation, and show that verifying linearizability of such implementations is reducible to control-state reachability. This reduction entails the first decidability results for verifying concurrent priority queues with an unbounded number of threads, and it enables the application of existing safety-verification tools for establishing their correctness.
BibTeX - Entry
@InProceedings{bouajjani_et_al:LIPIcs:2017:7807,
author = {Ahmed Bouajjani and Constantin Enea and Chao Wang},
title = {{Checking Linearizability of Concurrent Priority Queues}},
booktitle = {28th International Conference on Concurrency Theory (CONCUR 2017)},
pages = {16:1--16:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-048-4},
ISSN = {1868-8969},
year = {2017},
volume = {85},
editor = {Roland Meyer and Uwe Nestmann},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7807},
URN = {urn:nbn:de:0030-drops-78079},
doi = {10.4230/LIPIcs.CONCUR.2017.16},
annote = {Keywords: Concurrency, Linearizability, Model Checking}
}
Keywords: |
|
Concurrency, Linearizability, Model Checking |
Collection: |
|
28th International Conference on Concurrency Theory (CONCUR 2017) |
Issue Date: |
|
2017 |
Date of publication: |
|
01.09.2017 |