License
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://drops.dagstuhl.de/opus/volltexte/2017/7807/
Go to the corresponding LIPIcs Volume Portal


Bouajjani, Ahmed ; Enea, Constantin ; Wang, Chao

Checking Linearizability of Concurrent Priority Queues

pdf-format:
LIPIcs-CONCUR-2017-16.pdf (0.7 MB)


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
Seminar: 28th International Conference on Concurrency Theory (CONCUR 2017)
Issue Date: 2017
Date of publication: 25.08.2017


DROPS-Home | Fulltext Search | Imprint Published by LZI