Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Bouajjani, Ahmed; Enea, Constantin; Wang, Chao License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-78079

; ;

Checking Linearizability of Concurrent Priority Queues



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

  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 =		{},
  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: 2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI