@inproceedings{dcd80b5bd6274b7aa43e56b9eaaa556b,
title = "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.",
keywords = "Concurrency, Linearizability, Model Checking",
author = "Ahmed Bouajjani and Constantin Enea and Chao Wang",
note = "Publisher Copyright: {\textcopyright} Ahmed Bouajjani, Constantin Enea, and Chao Wang.; 28th International Conference on Concurrency Theory, CONCUR 2017 ; Conference date: 05-09-2017 Through 08-09-2017",
year = "2017",
month = aug,
day = "1",
doi = "10.4230/LIPIcs.CONCUR.2017.16",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Roland Meyer and Uwe Nestmann",
booktitle = "28th International Conference on Concurrency Theory, CONCUR 2017",
}