文章基本信息

标题：Checking Linearizability of Concurrent Priority Queues
本地全文：下载
作者：Ahmed Bouajjani ; Constantin Enea ; Chao Wang 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2017
卷号：85
页码：16:1-16:16
DOI：10.4230/LIPIcs.CONCUR.2017.16
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Concurrency; Linearizability; Model Checking