Checking Linearizability of Concurrent Priority
Queues
Ahmed Bouajjani1 , Constantin Enea1 , and Chao Wang1
1

Institut de Recherche en Informatique Fondamentale,
{abou,cenea,wangch}@irif.fr

arXiv:1707.00639v1 [] 3 Jul 2017

Abstract
Efficient implementations of concurrent objects such as atomic collections are essential to modern computing. Programming such objects is error prone: in minimizing the synchronization overhead between
concurrent object invocations, one risks the conformance to sequential specifications – or in formal terms,
one risks violating linearizability. Unfortunately, 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 such as
task scheduling or discrete event simulation, and show that verifying linearizability of such implementations can be reduced to control-state reachability. This reduction entails the first decidability results for
verifying concurrent priority queues in the context of an unbounded number of threads, and it enables the
application of existing safety-verification tools for establishing their correctness.
Digital Object Identifier 10.4230/LIPIcs...

1

Introduction

Modern computer software is increasingly concurrent. Interactive applications and services necessitate reactive asynchronous operations to handle requests immediately as they happen, rather than
waiting for long-running operations to complete. Furthermore, as processor manufacturers approach
clock-speed limits, performance improvements are more-often achieved by parallelizing operations
across multiple processor cores.
Multithreaded software is typically built with specialized “concurrent objects” like atomic integers, queues, maps, priority queues. These objects’ methods are designed to confom to better
established sequential specifications, a property known as linearizability [14], despite being optimized to avoid blocking and exploit parallelism, e.g., by using atomic machine instructions like
compare-and-swap. Intuitively, linearizability asks that every individual operation appears to take
place instantaneously at some point between its invocation and its return. Verifying linearizability
is intrinsically hard, and undecidable in general [4]. However, recent work [5] has shown that for
particular classes of objects, i.e., registers, mutexes, queues, and stacks, the problem of verifying
linearizability becomes decidable (for finite-state implementations).
In this paper, we consider another important object, namely the priority queue, which is essential
for applications such as task scheduling and discrete event simulation. Numerous implementations
have been proposed in the research literature, e.g., [2, 7, 16, 20, 19], and concrete implementations
exist in many modern languages like C++ or Java. Priority queues are collections providing put and
rm methods for adding and removing values. Every value added is associated to a priority and a
remove operation returns a minimal priority value. For generality, we consider a partially-ordered
set of priorities. Values with incomparable priorities can be removed in any order, and values having
the same priority are removed in the FIFO order. Implementations like the PriorityBlockingQueue in
Java where same priority values are removed in an arbitrary order can be modeled in our framework
by renaming equal priorities to incomparable priorities (while preserving the order constraints).
licensed under Creative Commons License CC-BY
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

XX:2

Checking Linearizability of Concurrent Priority Queues

Compared to previously studied collections like stacks and queues, the main challenge in dealing
with priority queues is that the order in which values are removed is not fixed by the happens-before
between add/remove operations (e.g., in the case of a queue, the values are removed in the order
in which they were inserted), but by parameters of the put operations (the priorities) which come
from an unbounded domain. For instance, the sequential behavior put(a, p1 ) · put(b, p3 ) · put(c, p2 ) ·
rm(a, p1 )·rm(c, p2 ) where the priority p1 is less than p2 which is less than p3 , is not admitted neither
by the regular queue nor the stack.
Following the approach in [5], we give a characterization of concurrent priority queue behaviors
violating linearizability in terms of automata. This characterization enables a reduction of checking
linearizability for arbitrary implementations to reachability or invariant checking, and implies decidability for checking linearizability of finite-state implementations. However, differently from the
case of stacks and queues where finite-state automata are sufficient, we show that the case of priority
queues needs register automata where registers are used to store and compare priorities.
This characterization is obtained in several steps. We first define a recursive procedure which
recognizes valid sequential executions which is then extended to recognize linearizable concurrent
executions. Intuitively, for an input execution e, this procedure handles values occurring in e one by
one, starting with values of maximal priority (which are to be removed the latest). For each value x,
it checks whether e satisfies some property “local” to that value, i.e., which is agnostic to how the
operations adding or removing other values are ordered between them (w.r.t. the happens-before),
other than how they are ordered w.r.t. the operations on x. When this property holds, the same
is done for the rest of the execution, without the operations on x. This procedure works only for
executions where a value is added at most once, but this is not a limitation for data-independent
implementations whose behavior doesn’t depend on the values that are added or removed. In fact,
all the implementations that we are aware of are data-independent.
Next, we show that checking whether an execution violates this “local” property for a value x
can be done using a class of register automata [15, 8, 18] (transition systems where the states consist
of a fixed set of registers that can receive values and be compared). Actually, only two registers
are needed: one register r1 for storing a priority guessed at the initial state, and one register r2
for reading priorities as they occur in the execution and comparing them with the one stored in r1 .
We show that registers storing values added to or removed from the priority queue are not needed,
since any data-independent implementation admits a violation to linearizability whenever it admits
a violation where the number of values is constant, and at most 5 (the number of priorities can still
be unbounded).
The remainder of this article is organized as follows. Section 2 describes the priority queue
ADT, lists several semantic properties like data-independence that are satisfied by implementations
of this ADT, and formalizes the notion of linearizability. Sections 3 defines a recursive procedure
for checking linearizability of concurrent priority queue behaviors. Section 4 gives an automata
characterization of the violations to linearizability, and Section 5 discusses related work.

2

The Priority Queue ADT

We consider priority queues whose interface contains two methods put and rm for adding and respectively, removing a value. Each value is assigned with a priority when being added to the data
structure (using a call to put) and the remove method rm removes a value with a minimal priority.
For generality, we assume that the set of priorities is partially-ordered. Incomparable priorities can
be removed in any order. In case multiple values are assigned with the same priority, rm returns the
least recent value (according to a FIFO semantics). Also, when the set of values stored in the priority
queue is empty, rm returns the distinguished value empty. Concurrent implementations of the prior-

Ahmed Bouajjani, Constantin Enea, and Chao Wang

XX:3

ity queue allow the methods put and rm to be called concurrently from different threads. However,
every method invocation should give the illusion that it takes place instantaneously at some point
between its invocation and its return. We formalize (concurrent) executions and implementations in
Section 2.1, Section 2.2 introduces a set of properties satisfied by all the implementations we are
aware of, and Section 2.3 defines the standard correctness criterion for concurrent implementations
of ADTs known as linearizability [14].

2.1

Executions

We fix a (possibly infinite) set D of data values, a (possibly infinite) set P of priorities, a partial order
≺ among elements in P, and an infinite set O of operation identifiers. The latter are used to match
call and return actions of the same invocation. Call actions callo (put, a, p) and callo (rm, a0 ) with
a ∈ D, a0 ∈ D ∪ {empty}, p ∈ P, and o ∈ O, combine a method name and a set of arguments
with an operation identifier. The return value of a remove is transformed to an argument value for
uniformity 1 . The return actions are denoted in a similar way as reto (put, a, p) and respectively,
reto (rm, a0 ).
An execution e is a sequence of call and return actions which satisfy the following well-formedness
properties: each return is preceded by a matching call (i.e., having the same operation identifier),
and each operation identifier is used in at most one call/return. We assume every set of executions is
closed under isomorphic renaming of operation identifiers. An execution is called sequential when
no two operations overlap, i.e., each call action is immediately followed by its matching return action, and concurrent otherwise. To ease the reading, we write a sequential execution as a sequence
of put(a, p) and rm(a) symbols representing a pair of actions callo (put, a, p) · reto (put, a, p) and
callo (rm, a) · reto (rm, a), respectively (where o ∈ O). For example, given two priorities p1 ≺ p2 ,
put(a, p2 ) · put(b, p1 ) · rm(b) is a sequential execution of the priority queue (rm returns b because it
has smaller priority).
We define SeqPQ, the set of sequential priority queue executions, semantically via labelled transition system (LT S). An LTS is a tuple A = (Q, Σ, →, q0 ), where Q is a set of states, Σ is an alphabet
of transition labels, →⊆ Q × Σ × Q is a transition relation and q0 is the initial state. We model
priority queue as an LTS PQ defined as follows: each state of the LTS PQ is a mapping associating
priorities in P with sequences of values in D representing a snapshot of the priority queue (for each
priority, the values are ordered as they were inserted); the transition labels are put(a, p) and rm(a)
rm(empty)

operations; Each transition modifies the state as expected. For example, q1 −−−−−→ q2 if q1 = q2 ,
and q1 and q2 map each priority to the empty sequence . Then, SeqPQ is the set of traces of PQ.
The detailed definition of PQ can be found in Appendix A.
An implementation I is a set of executions. Implementations represent libraries whose methods
are called by external programs. In the remainder of this work, we consider only completed executions, where each call action has a corresponding return action. This simplification is sound when
implementation methods can always make progress in isolation: formally, for any execution e with
pending operations, there exists an execution e0 obtained by extending e only with the return actions
of the pending operations of e. Intuitively this means that methods can always return without any
help from outside threads, avoiding deadlock.

1

Method return values are guessed nondeterministically, and validated at return points. This can be handled using
the assume statements of typical formal specification languages, which only admit executions satisfying a given
predicate.

XX:4

Checking Linearizability of Concurrent Priority Queues

2.2

Semantic Properties of Priority Queues

We define two properties which are satisfied by priority queue implementations and which are important for the results that follow: (1) data independence [23, 1] states that priority queue behaviors
do not depend on the actual values which are added to the queue, and (2) closure under projection [5] states that intuitively, remove operations can return the same values no matter how many
other different values are in the queue, assuming they don’t have more important priorities.
An execution e is data-differentiated if every value is added at most once, i.e., for each d ∈ D, e
contains at most one action callo (put, d, p) with o ∈ O and p ∈ P. Note that this property concerns
only values, a data-differentiated execution e may contain more than one value with the same priority.
The subset of data-differentiated executions of a set of executions E is denoted by E6= .
A renaming function r is a function from D to D. Given an execution e, we denote by r(e)
the execution obtained from e by replacing every data value x by r(x). Note that r renames only
the values and keep the priorities unchanged. Intuitively, renaming values has no influence on the
behavior of the priority queue, contrary to renaming priorities.
I Definition 1. A set of executions E is data independent iff
- for all e ∈ E, there exists e0 ∈ E6= and a renaming function r, such that e = r(e0 ),
- for all e ∈ E and for all renamings r, r(e) ∈ E.
The following lemma is a direct consequence of definitions.
I Lemma 2. SeqPQ is data independent.
Beyond the sequential executions, every (concurrent) implementation of the priority queue that
we are aware of is data-independent. Therefore, from now on, we consider only data-independent
implementations. This assumption enables a reduction from checking the correctness of an implementation I to checking the correctness of only its data-differentiated executions in I6= .
Besides data independence, the sequential behaviors of the priority queue satisfy the following
closure property: a behavior remains valid when removing all the operations with an argument
in some set of values D ⊆ D and any rm(empty) operation (since they are read-only and they
don’t affect the queue’s state). In order to distinguish between different rm(empty) operations while
simplifying the technical exposition, we assume that they receive as argument a value, i.e., call
actions are of the form callo (rm, empty, a) for some a ∈ D. We will make explicit this argument
only when needed in our technical development. The projection e|D of an execution e to a set of
values D ⊆ D is obtained from e by erasing all call/return actions with an argument not in D. We
write e \ x for the projection e|D\{x} . Let proj(e) be the set of all projections of e to a set of values.
The proof of the following lemma can be found in Appendix B.
I Lemma 3. SeqPQ is closed under projection, i.e., proj(e) ⊆ SeqPQ for each e ∈ SeqPQ.

2.3

Linearizability

We recall the notion of linearizability [14] which is the de facto standard correctness condition for
concurrent data structures. Given an execution e, the happen-before relation <hb between operations 2 is defined as follows: o1 <hb o2 , if the return action of o1 occurs before the call action of o2
in e. The happens-before relation is an interval order [6]: for distinct o1 , o2 , o3 , o4 , if o1 <hb o2 and
o3 <hb o4 , then either o1 <hb o4 , or o3 <hb o2 . Intuitively, this comes from the fact that concurrent
threads share a notion of global time.

2

In general, we refer to operations using their identifiers.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

XX:5

Given a (concurrent) execution e and a sequential execution s, we say that e is linearizable w.r.t
s, denoted e v s, if there is a bijection f : O1 → O2 , where O1 and O2 are the set of operations
of e and s, respectively, such that (1) o and f (o) is the same operation3 , and (2) if o1 <hb o2 , then
f (o1 ) <hb f (o2 ). A (concurrent) execution e is linearizable w.r.t a set S of sequential executions,
denoted e v S, if there exists s ∈ S such that e v s. A set of concurrent executions E is linearizable
w.r.t S, denoted E v S, if e v S for all e ∈ E.
The following lemma states that by data-independence, it is enough to consider only datadifferentiated executions when checking linearizability (see Appendix B). This is similar to that in
[1, 5], where they use the notion of data-independence in [23]. Section 3 will focus on characterizing
linearizability for data-differentiated executions.
I Lemma 4. A data-independent implementation I is linearizable w.r.t a data-independent set S
of sequential executions, if and only if I6= is linearizable w.r.t. S6= .

3

Checking Linearizability of Priority Queue Executions

We define a recursive procedure for checking linearizability of an execution w.r.t. SeqPQ. To
ease the exposition, Section 3.1 introduces a recursive procedure for checking whether a datadifferentiated sequential execution is admitted by the priority queue which is then extended to the
concurrent case in Section 3.2.

3.1

Characterizing Data-Differentiated Sequential Executions

Checking whether a data-differentiated sequential execution belongs to SeqPQ could be implemented by checking membership into the set of traces of the LTS P Q. The recursive procedure
Check-PQ-Seq outlined in Algorithm 1 is an alternative to this membership test. Roughly, it selects
one or two operations in the input execution, checks whether their return values are correct by ignoring the order between the other operations other than how they are ordered w.r.t. the selected ones,
and calls itself recursively on the execution without the selected operations.
We explain how the procedure works on the following execution:
put(c, p2 ) · put(a, p1 ) · rm(a) · rm(c) · rm(empty) · put(d, p2 ) · put(f, p3 ) · rm(f ) · put(b, p1 )

(1)

where p1 , p2 , p3 are priorities such that p1 ≺ p2 and p1 ≺ p3 , and p2 and p3 are incomparable.
Since the rm(empty) operations are read-only (they don’t affect the state of the queue), they are
selected first. Ensuring that an operation o = rm(empty) is correct boils down to checking that every
put(x, p) operation before o is matched to a rm(x) operation which also occurs before o. This is true
in this case for x ∈ {a, c}. Therefore, the correctness of (1) reduces to the correctness of
put(c, p2 ) · put(a, p1 ) · rm(a) · rm(c) · put(d, p2 ) · put(f, p3 ) · rm(f ) · put(b, p1 )
When there are no more rm(empty) operations, the procedure selects a put operation adding a value
with maximal priority which is not removed, and then a pair of put and rm operations adding and
removing the same maximal priority value. For instance, since p2 is a maximal priority, it selects
the operation put(d, p2 ). This operation is correct if d is the last value with priority p2 , and the
correctness of (1) reduces to the correctness of
put(c, p2 ) · put(a, p1 ) · rm(a) · rm(c) · put(f, p3 ) · rm(f ) · put(b, p1 )

3

An m(a)-operation in an execution e is an operation identifier o s.t. e contains the actions callo (m, a), reto (m, a).

XX:6

Checking Linearizability of Concurrent Priority Queues

Algorithm 1: Check-PQ-Seq
Input: A data-differentiated sequential execution e
Output: true iff e ∈ SeqPQ
1 if e =  then
2
return true;
3 if Has-EmptyRemoves(e) then
4
if ∃ o = rm(empty) ∈ e such that EmptyRemove-Seq(e, o) holds then
5
return Check-PQ-Seq(e \ o);
6 else if Has-UnmatchedMaxPriority(e) then
7
if ∃ x ∈ values(e) such that UnmatchedMaxPriority-Seq(e, x) holds then
8
return Check-PQ-Seq(e \ x);
9 else
10
if ∃ x ∈ values(e) such that MatchedMaxPriority-Seq(e, x) holds then
11
return Check-PQ-Seq(e \ x);
12
else
13
return false;

Since there is no other value of maximal priority which is not removed, the procedure selects a pair
of put/rm operations with an argument of maximal priority p2 , for instance, put(c, p2 ) and rm(c).
The value returned by rm is correct if all the values of priority smaller than p2 added before rm(c)
are also removed before rm(c). In this case, a is the only value of priority smaller than p2 and it
satisfies this property. Applying a similar reasoning for all the remaining values, it can be proved
that this execution is correct.
In formal terms, the operations which are selected depend on the following set of predicates on
executions:
Has-EmptyRemoves(e) = true iff e contains a rm(empty) operation
Has-UnmatchedMaxPriority(e) = true iff p ∈ unmatched-priorities(e) for a maximal priority
p ∈ priorities(e)

where priorities(e), resp., unmatched-priorities(e), is the set of priorities occurring in put operations
of e, resp., in put operations of e for which there is no rm operation removing the same value.
We call the latter unmatched put operations. A put operation which is not unmatched is called
matched. For simplicity, we consider the following syntactic sugar Has-MatchedMaxPriority(e) =
¬Has-EmptyRemoves(e) ∧ ¬Has-UnmatchedMaxPriority(e). By an abuse of notation, we also
assume that Has-UnmatchedMaxPriority(e) ⇒ ¬Has-EmptyRemoves(e) (this is sound by the order
of the conditionals in Check-PQ-Seq).
The predicates defining the correctness of the selected operations are defined as follows:
EmptyRemove-Seq(e, o) = true iff e = u · o · v and matched(u)
UnmatchedMaxPriority-Seq(e, x) = true iff e = u · put(x, p) · v, p 6≺ priorities(u · v), and p 6∈ priorities(v)
MatchedMaxPriority-Seq(e, x) = true iff e = u · put(x, p) · v · rm(x) · w, p 6≺ priorities(u · v · w),
p 6 unmatched-priorities(u · v · w), matched≺ (u · v, p),
and p 6∈ priorities(v · w)

where p ≺ priorities(e) when p ≺ p0 for some p0 ∈ priorities(e) (and similarly for p ≺ unmatched-p
riorities(e) or p  unmatched-priorities(e)), matched≺ (e, p) holds when each value with priority
strictly smaller than p is removed in e, and matched(e) holds when matched≺ (e, p) holds for each

Ahmed Bouajjani, Constantin Enea, and Chao Wang

p ∈ P. Compared to the example presented at the beginning of the section, these predicates take into
consideration that multiple values with the same priority are removed in FIFO order: the predicate
MatchedMaxPrioritySeq(e, x) holds when x is the last value with priority p added in e.
When o is a rm(empty) operation, we write e \ o for the maximal subsequence of e which doesn’t
contain o. For an execution e, values(e) is the set of values occurring in call/return actions of e.
The following lemma states the correctness of Check-PQ-Seq (see Appendix A for the proof).
I Lemma 5. Check-PQ-Seq(e) = true iff e ∈ SeqPQ, for every data-differentiated sequential
execution e.

3.2

Checking Linearizability of Data-Differentiated Concurrent
Executions

The extension of Check-PQ-Seq to concurrent executions, checking whether they are linearizable
w.r.t. SeqPQ, is obtained by replacing every predicate Γ-Seq with
Γ-Conc(e, α) = true iff there exists a sequential execution s such that e v s and Γ-Seq(s, α)
for each Γ ∈ {EmptyRemove, UnmatchedMaxPriority, MatchedMaxPriority}. Let Check-PQ-Conc
denote the thus obtained procedure (we assume recursive calls are modified accordingly).
The following lemma states the correctness of Check-PQ-Conc. Completeness follows easily
from the properties of SeqPQ. Thus, if Check-PQ-Conc(e) = false, then there exists a set D of
values s.t. either EmptyRemove-Conc(e|D) is false, or UnmatchedMaxPriority-Conc(e|D, x) is
false for all the values x of maximal priority that are not removed (and there exists at least one such
value), or MatchedMaxPriority-Conc(e|D, x) is false for all the values x of maximal priority (and
these values are all removed in e|D). It can be easily seen that we get e|D 6v SeqPQ in all cases,
which by the closure under projection of SeqPQ implies, e 6v SeqPQ (since every linearization of e
includes as a subsequence a linearization of e|D).
I Lemma 6. Check-PQ-Conc(e) = true iff e v SeqPQ, for every data-differentiated execution e.
Proving soundness is highly non-trivial and one of the main technical contributions of this paper
(see Appendix C.4 for a complete proof). The main technical difficulty is showing that for any
execution e, any linearization of e \ x for some maximal priority value x can be extended to a
linearization of e provided that UnmatchedMaxPriority or MatchedMaxPriority holds (depending
on whether there are values with the same priority as x in e which are not removed).
We explain the proof of this property on the execution e in Figure 1(a) where p1 ≺ p, p1 ≺
p2 , and the predicate Has-MatchedMaxPriority(e) holds. Assume that there exist two sequential
executions l and l0 such that e v l = u · put(x, p) · v · rm(x) · w, MatchedMaxPriority-Seq(l, x)
holds, and e \ x v l0 ∈ SeqPQ. Let u = , w be any sequence containing the set of operations
put(z2 , p2 ) and rm(z1 ) (we distinguish them by adding the suffix −w to their name, e.g., rm(z1 )−w),
and v be any sequence containing the remaining operations. In general, the linearization l0 can be
defined by choosing for each operation, a point in time between its call and return actions, called
linearization point. The order between the linearization points defines the sequence l0 . Figure 1(a)
draws linearization points for the operations in e \ x defining the linearization l0 4 . We show how to
construct a sequence l00 = l100 · put(x, p) · l200 · rm(x) · l300 ∈ SeqPQ such that e v l00 .

4

In general, there may exist multiple ways of choosing linearization points to define the same linearization. Our
construction is agnostic to this choice.

XX:7

XX:8

Checking Linearizability of Concurrent Priority Queues
put(x, p)

rm(x)

put(x2 , p)

put(x, p)

rm(x2 )

put(z1 , p2 )

put(z2 , p2 ) − w

rm(x)

put(x2 , p)

rm(x2 )

put(y1 , p1 )

put(y1 , p1 )

rm(y1 )

rm(y1 )

rm(z1 ) − w

put(z1 , p2 )

put(z2 , p2 )

rm(z2 )
(a)

rm(z1 )

rm(z2 )
(b)

Figure 1 The process of obtaining linearization of e

- An operation is called p-comparable (resp., p-incomparable) when it receives as argument a value
of priority comparable to p (resp., incomparable to p). We could try to define l100 , l200 and l300 as
the projection of l0 to the operations in u, v and w, respectively. However, this is incorrect, since
MatchedMaxPriority-Seq(l, x) imposes no restriction on p-incomparable operations in u · v, and
thus, there is no guarantee that the projection of l0 to p-incomparable operations in u·v is correct.
In this example, this projection is put(z1 , p2 ) · rm(z2 ) which is incorrect.
- We define the sets of operations U 0 , V 0 and W 0 such that l100 , l200 and l300 are the projections of l0 to
U 0 , V 0 , and W 0 , respectively. This is done in two steps:
- The first step is to define W 0 . The p-comparable operations in W 0 are the same as in w. To
identify the p-incomparable operations in W 0 , we search for a p-incomparable operation o which
either happens before some p-comparable operation in w, or whose linearization point occurs
after ret(rm, x). We add to W 0 the operation o and all the p-incomparable operations occurring
after o in l0 . In this example, o is rm(z1 ) and the only p-incomparable operation occurring after
o in l0 is rm(z2 ) (they are surrounded by boxes in the figure). In this process, whether a pincomparable operation is in W 0 or not only relies on whether it is before or after such an o in
l0 .
- The second step is to define U 0 and V 0 . U 0 contains two kinds of operations: (1) operations
whose linearization points are before ret(put, x, p), and (2) other put operations with priority p.
V 0 contains the remaining operations. In this example, U 0 contains put(z1 , p2 ) and put(x2 , p).
- In conclusion, we have that l100 = put(z1 , p2 ) · put(x2 , p), l200 = put(z2 , p2 ) · rm(x2 ) · put(y1 , p1 ) ·
rm(y1 ), and l300 = rm(z1 ) · rm(z2 ). Figure 1(b) draws linearization points for each operation in e
defining the linearization l00 .
Section 4 introduces a characterization of concurrent priority queue violations using a set of
non-recursive automata (i.e., whose states consist of a fixed number of registers) whose standard
synchronized product is equivalent to Check-PQ-Conc (modulo renaming of values which is possible by data-independence). Since SeqPQ is closed under projection (Lemma 3), the recursion in
Check-PQ-Conc can be eliminated by checking that each projection of a given execution e passes a
non-recursive version of Check-PQ-Conc where every recursive call is replaced by true. More precisely, every occurrence of return Check-PQ-Conc is replaced by return true. Let Check-PQ-ConcNonRec be the thus obtained procedure.
I Lemma 7. Given a data-differentiated execution e, e v SeqPQ if and only if for each e0 ∈
proj(e), Check-PQ-Conc-NonRec(e0 ) returns true.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

4

XX:9

Reducing Linearizability of Priority Queues to Reachability

We show that the set of executions for which some projection fails the test Check-PQ-Conc-NonRec
can be characterized using a set of register automata, modulo a value renaming. The possibility
of renaming values (which is complete for checking data independent implementations) allows to
simplify the reasoning about projections. Thus, we assume that all the operations which are not in
the projection failing this test use the same distinguished value >, different from those used in the
projection. Then, it is enough to find an automata characterization for the set of executions e for
which Check-PQ-Conc-NonRec fails, or equivalently, for which one of the following three formulas
is false:
Γ(e) := Has-Γ(e) ⇒ ∃α. Γ-Conc(e, α) with Γ ∈ {EmptyRemove, UnmatchedMaxPriority, MatchedMaxPriority}
Intuitively, Γ(e) states that e is linearizable w.r.t. the set of sequential executions described by Γ-Seq
(provided that Has-Γ(e) holds). Therefore, by an abuse of terminology, an execution e satisfying
Γ(e) is called linearizable w.r.t. Γ, or Γ-linearizable. Extending the automaton characterizing executions which are not Γ-linearizable, with self-loops that allow any operation with parameter >
results in an automaton satisfying the following property called Γ-completeness.
I Definition 8. For Γ ∈ {EmptyRemove, UnmatchedMaxPriority, MatchedMaxPriority}, an
automaton A is called Γ-complete when for each data-independent implementation I:
A∩I =
6 ∅ if and only if there exists e ∈ I and e0 ∈ proj(e) such that e0 is not Γ-linearizable.
Section 4.1 describes a MatchedMaxPriority-complete automaton, the other automata being
defined in Appendix D.1 and Appendix D.7. Therefore, the following holds.
I Lemma 9. There exists a Γ-complete automaton for each Γ ∈ {EmptyRemove, UnmatchedMax
Priority, MatchedMaxPriority}.
When defining Γ-complete automata, we assume that every implementation I behaves correctly,
i.e., as a FIFO queue, when only values with the same priority are observed. More precisely, we
assume that for every execution e ∈ I and every priority p ∈ P, the projection of e to values with
priority p is linearizable (w.r.t. SeqPQ). This property can be checked separately using register
automata obtained from the finite automata in [5] for FIFO queue (see Appendix D.1 for more
details). Note that this assumption excludes some obvious violations, such as a rm(a) operation
happens before a put(a, p) operation, for some p.
Also, we consider Γ-complete automata for Γ ∈ {UnmatchedMaxPriority, MatchedMaxPriority},
recognizing executions which contain only one maximal priority. This is possible because any
data-differentiated execution for which Γ(e) is false has such a projection. Formally, given a datadifferentiated execution e and p a maximal priority in e, e|p is the projection of e to the set of values
with priorities smaller than p. Then,
I Lemma 10. Let Γ ∈ {UnmatchedMaxPriority, MatchedMaxPriority} and e a data-differentiated
execution. Then, e is Γ-linearizable iff e|p is Γ-linearizable for some maximal priority p in e.
Proof. (Sketch) To prove the only if direction, let e be a data-differentiated execution linearizable
w.r.t. l = u·put(x, p)·v·rm(x)·w ∈ MatchedMaxPriority-Seq(s, x). Since MatchedMaxPriority-Seq
(s, x) imposes no restriction on the operations in u, v and w with priorities incomparable to p, erasing all these operations results in a sequential execution which still satisfies this property. Similarly,
for Γ = UnmatchedMaxPriority.
The if direction follows from the fact that if the projection of an execution to a set of operations
O1 has a linearization l1 and the projection of the same execution to the remaining set of operations

XX:10

Checking Linearizability of Concurrent Priority Queues

has a linearization l2 , then the execution has a linearization which is defined as an interleaving of l1
and l2 (see Appendix D.2 for more details).
Thus, let e be an execution such that e|p is linearizable w.r.t. l = u · put(x, p) · v · rm(x) ·
w ∈ MatchedMaxPriority-Seq(s, x). By the property above, we know that e has a linearization
l0 = u0 · put(x, p) · v 0 · rm(x) · w0 , such that the projection of l0 to values of priority comparable to p is
l. Since MatchedMaxPriority-Seq(s, x) does not have a condition on values of priority incomparable
to p, we obtain that l0 ∈ MatchedMaxPriority-Seq(s, α).
J
The following shows that Γ-complete automata enable an effective reduction of checking linearizability of concurrent priority queue implementations to state reachability. It is a direct consequence
of the above definitions. Section 4.2 discusses decidability results implied by this reduction.
I Theorem 11. Let I be a data-independent implementation, and A(Γ) be a Γ-complete automaton for each Γ. Then, I v SeqPQ if and only if I ∩ A(Γ) = ∅ for all Γ.

4.1

A MatchedMaxPriority-complete automaton

A differentiated execution e is not MatchedMaxPriority-linearizable when all the put operations
in e using the maximal priority p are matched, and e is not linearizable w.r.t. the set of sequential
executions satisfying MatchedMaxPriority-Seq(e, x) for each value x of priority p. We consider two
cases depending on whether e contains exactly one value with priority p or at least two values. We
denote by MatchedMaxPriority> the strengthening of MatchedMaxPriority with the condition that
all the values other than x have a priority strictly smaller than p (corresponding to the first case), and
by MatchedMaxPriority= the strengthening of the same formula with the negation of this condition
(corresponding to the second case). We use particular instances of register automata [15, 8, 18]
whose states include only two registers, one for storing a priority guessed at the initial state, and one
for storing the priority of the current action in the execution. The transitions can check equality or
the order relation ≺ between the values stored in the two registers. Instead of formalizing the full
class of register automata, we consider a simpler class which suffices our needs. More precisely,
we consider a class of labeled transition systems whose states consist of a finite control part and a
register r interpreted to elements of P. The transition labels can be one of the following:
r = ∗ for storing an arbitrary value to r,
call(rm, a) and ret(rm, a) for reading call/return actions of a remove,
call(put, d, g) where g ∈ {= r, ≺ r, true} is a guard, for reading a call action call(put, d, p) of a
put and checking whether p is either equal to or smaller than the value stored in r, or arbitrary,
ret(put, d, true) for reading a return action ret(put, d, p) for any p.
The set of words accepted by such a transition system can be defined as usual.

4.1.1

A MatchedMaxPriority> -complete automaton

We give a typical example of an execution e which is not MatchedMaxPriority> -linearizable in
Figure 2. Intuitively, this is a violation because during the whole execution of rm(b), the priority
queue stores a smaller priority value (which should be removed before b). To be more precise, we
define the interval of a value x as the time interval from the return of a put ret(put, x, p) to the
call of the matching remove call(rm, x), or to the end of the execution if such a call action doesn’t
exist. Intuitively, it represents the time interval in which a value is guaranteed to be stored into the
concurrent priority queue. Concretely, for a standard indexing of actions in an execution, a time
interval is a closed interval between the indexes of two actions in the execution. In Figure 2, we
draw the interval of each value by dashed line. Here we assume that p1 ≺ p4 , p2 ≺ p4 , and p3 ≺ p4 .
We can not find a sequence s where e v s and MatchedMaxPriority-Seq(s, b) holds, since each

Ahmed Bouajjani, Constantin Enea, and Chao Wang

time point from call(rm, b) to ret(rm, b) is included in the interval of some smaller priority value,
and rm(b) can’t take effect in the interval of a smaller priority value.
put(b, p4 )

rm(b)

put(d, p1 )

rm(d)

put(e, p2 )
put(f, p3 )

rm(e)
rm(f )

Figure 2 An execution that is not MatchedMaxPriority> -linearizable. We represent each operation as a
time interval whose left, resp., right, bound corresponds to the call, resp., return action. Operations adding and
removing the same value are aligned vertically.

To formalize the scenario in Figure 2 we use the notion of left-right constraint defined below.
I Definition 12. Let e be a data-differentiated execution which contains only one maximal priority
p, and only one value x of priority p (and no rm(empty) operations). The left-right constraint of x is
the graph G where:
the nodes are the values occurring in e,
there is an edge from d1 to x, if put(d1 , _) <hb put(x, p) or put(d1 , _) <hb rm(x),
there is an edge from x to d1 , if rm(x) <hb rm(d1 ) or rm(d1 ) does not exists,
there is an edge from d1 to d2 , if put(d1 , _) <hb rm(d2 , _).
The execution in Figure 2 is not MatchedMaxPriority> -linearizable because the left-right constraint of the maximal priority value b contains a cycle: f → e → d → b → f . The presence of
such a cycle is equivalent to the execution not being MatchedMaxPriority> -linearizable (see Appendix D.3), as indicated by the following lemma:
I Lemma 13. Given a data-differentiated execution e where Has-MatchedMaxPriority(e) holds,
let p be its maximal priority and put(x, p), rm(x) are only operations of priority p in e. Let G be the
graph representing the left-right constraint of x. e is MatchedMaxPriority-linearizable, if and only
if G has no cycle going through x.
When the left-right constraint of the maximal priority value x contains a cycle of the form d1 →
. . . → dm → x → d1 for some d1 ,. . .,dn ∈ D, we say that x is covered by d1 , . . . , dm . The
shape of such a cycle (i.e., the alternation between call/return actions of put/rm operations) can be
detected using our class of automata, the only complication being the unbounded number of values
d1 ,. . .,dn . However, by data independence, whenever an implementation contains such an execution
it also contains an execution where all the values d1 ,. . .,dn are renamed to the same value a, and x
is renamed to b. Therefore, our automata can be defined over a fixed set of values a, b, and > (recall
that > is used for the operations outside of the non-linearizable projection).
To define a MatchedMaxPriority> -complete automaton we need to consider several cases depending on the order between the call/return actions of the put/rm operations that add and respectively, remove the value b. For example, the case where the put happens-before the remove (as in
Figure 2) is pictured in Figure 3. This automaton captures the three possible ways of ordering the
first action ret(put, a, _) w.r.t. the actions with value b, which are pictured in Figure 4 (a) (this
action cannot occur after call(rm, b, _) since b must be covered by the a-s). The paths corresponding to these three possible orders are: q1 → q2 → q3 . . . → q7 , q1 → q2 → q3 . . . → q10 and
q1 → q9 → q10 . . . → q7 . In Figure 4, we show all the four orders of the call/return actions of
adding and removing b, and also possible orders of the first ret(put, a, _) w.r.t the actions with value
b. In Appendix D.3, three register automata is constructed according to the cases of Figure 4 (b), (c)
and (d), respectively.

XX:11

XX:12

Checking Linearizability of Concurrent Priority Queues
C2

q2
C2

C2

qinit r = ∗

C2
ret(put, b, = r)

call(put, b, = r) ret(put, a, < r)

q1

C2
ret(put, a, < r)

q3

C3
cal(rm, b)

q4

q5

C1
ret(rm, b)

q7

C2 cal(rm, b)

C2

q10

ret(put, b, = r)

q11

cal(rm, a)

ret(put, a, < r) cal(rm, a)
C3

C1

q6

q8

C2
ret(put, a, < r)
call(put, b, = r)
q9

Figure 3 Register automaton A1l-lar . We use the following notations: C1 = C ∪ {ret(rm, a)}, C2 =
C ∪ {call(put, a, = r)}, C3 = C2 ∪ {ret(rm, a)}, where C = {call(put, >, true), ret(put, >, true), call(rm, d),
ret(rm, d), call(rm, empty), ret(rm, empty)}.
put(b, p)

rm(b)

put(b, p)

put(a, )

put(b, p)

rm(b)
put(a, )

put(a, )
put(a, )

put(a, )

(a)

(b)

put(b, p)

rm(b)
put(a, )

rm(b)
put(a, )

put(a, )

put(a, )
(c)

(d)

Figure 4 Four cases of ordering actions with value b, and possible orders of the first ret(put, a, _) w.r.t the
actions with value b

4.1.2

A MatchedMaxPriority= -complete automaton

When an execution contains at least two values of maximal priority, the acyclicity of the left-right
constraints (for all the maximal priority values) is not enough to conclude that the execution is
MatchedMaxPriority-linearizable. Intuitively, there may exist a value a which is added before another value b such that all the possible linearization points of rm(b) are disabled by the position of
rm(a) in the happens-before. We give an example of such an execution e in Figure 5. This execution
is not linearizable w.r.t. MatchedMaxPriority (or MatchedMaxPriority= ) even if neither a nor b
are covered by values with smaller priority. Since put(a, p4 ) <hb put(b, p4 ) and values of the same
priority are removed in FIFO order, rm(a) should be linearized before rm(b) (i.e., this execution
should be linearizable w.r.t. a sequence where rm(a) occurs before rm(b)). Since rm(b) cannot take
effect during the interval of a smaller priority value, it could be linearized only in one of the two time
intervals pictured with dotted lines in Figure 5. However, each of these time intervals ends before
call(rm, a), and thus rm(a) cannot be linearized before rm(b).
put(b, p4 )rm(b)
put(a, p4 )
put(c, p1 ) rm(c) put(d, p1 )

rm(a)
rm(d) put(e, p1 )rm(e) put(f, p1 )rm(f )

Figure 5 An execution that is not linearizable w.r.t MatchedMaxPriority= .

To recognize the scenarios in Figure 5, we introduce an order <pb between values which intuitively, can be thought of as “a value a is put before another value b”. Thus, given a data-differentiated

Ahmed Bouajjani, Constantin Enea, and Chao Wang

execution e and two values a and b of maximal priority, a <pb b if one of the following holds:
(1) put(a, _) <hb put(b, _), (2) rm(a) <hb rm(b), or (3) rm(a) <hb put(b, _). Sometimes we use
B
C
∗
a <A
pb b, a <pb b and a <pb b to explicitly distinguish between these three cases. Let <pb be the
transitive closure of <pb .
Then, to model the time intervals in which a remove operation like rm(b) in Figure 5, can be
linearized (outside of intervals of smaller priority values) we introduce the notion of gap-point. Here
we assume that the index of actions of an execution starts from 0.
I Definition 14. Let e be a data-differentiated execution which contains only one maximal priority
p, and put(x, p) and rm(x) two operations in e. An index i ∈ [0, |e| − 1] is a gap-point of x if i is
greater than or equal to the index of both call(put, x, p) and call(rm, x), smaller than the index of
ret(rm, x), and it is not included in the interval of some value with priority smaller than p.
The case of Figure 5 can be formally described as follows: a <∗pb b while the right-most gappoint of b is before call(rm, a) or call(put, a, p4 ). The following lemma states that these conditions
are enough to characterize non-linearizability w.r.t MatchedMaxPriority= (see Appendix D.4).
I Lemma 15. Let e be a data-differentiated execution which contains only one maximal priority p
such that Has-MatchedMaxPriority(e) holds. Then, e is not linearizable w.r.t MatchedMaxPriority=
iff e contains two values x and y of maximal priority p such that y <∗pb x, and the rightmost gap-point
of x is strictly smaller than the index of call(put, y, p) or call(rm, y).
To characterize violations to linearizability w.r.t. MatchedMaxPriority= using an automaton
that tracks a bounded number of values, we show that the number of values needed to witness that
y <∗pb x for some x and y is bounded.
I Lemma 16. Let e be a data-differentiated execution such that a <pb a1 <pb . . . <pb am <pb b
holds for some set of values a, a1 ,. . .,am , b. Then, one of the following holds:
B
C
- a <A
pb b, a <pb b, or a <pb b,
B
B
A
- a <A
pb ai <pb b or a <pb ai <pb b, for some i.
To characterize violations to linearizability w.r.t. MatchedMaxPriority= , one has to consider all
the possible orders between call/return actions of the operations on values a, b, and ai in Lemma 16,
and the right-most gap point of b. Excluding the inconsistent cases, we are left with 5 possible orders
that are shown in Figure 6, where o denotes the rightmost gap-point of b. For each case, we define
an automaton recognizing the induced set of violations. For instance, the register automata for the
case of Figure 6(a) is shown in Figure 7. In this case, the conditions in Lemma 15 are equivalent to
the fact that intuitively, the time interval from call(rm, a) to ret(rm, b) is covered by lower priority
values (and thus, there is no gap-point of b which occurs after call(rm, a)). Using again the dataindependence property, these lower priority values can all be renamed to a fixed value d, and the
other values to a fixed value >.

4.2

Decidability Result

We describe a class C of data-independent implementations for which linearizability w.r.t. SeqPQ is
decidable. The implementations in C allow an unbounded number of values but a bounded number of
priorities. Each method manipulates a finite number of local variables which store Boolean values,
or data values from D. Methods communicate through a finite number of shared variables that
also store Boolean values, or data values from D. Data values may be assigned, but never used
in program predicates (e.g., in the conditions of if-then-else and while statements) so as to ensure
data independence. This class captures typical implementations, or finite-state abstractions thereof,
e.g., obtained via predicate abstraction. Since the Γ-complete automata A(Γ) uses a fixed set D =

XX:13

XX:14

Checking Linearizability of Concurrent Priority Queues

put(b, )

put(b, )

rm(b)

rm(b)

rm(b)

put(a, )

rm(a)

rm(a1 )

put(a, )

put(a1 , )

rm(a)
put(a, )

o

rm(a)

o

(a)

o

(b)

(c)

rm(b)

rm(b)

rm(a1 )

rm(a1 )

put(a1 , )

put(a1 , )

put(a, )

rm(a)

put(a, )

rm(a)

o

o

(d)

(e)

Figure 6 Five cases that need to be considered.

C1

C1

qinit r = ∗

q1

C1
call(put, a, = r)

C2
cal(rm, b)

q5

q2

C1
ret(put, a, = r)

C2
ret(put, d, < r)

q6

q3

C2
cal(put, b, = r)

C3
call(rm, a)

q7

ret(put, d, < r) C3

q4

C4
ret(rm, b)

call(rm, d)

q8

C4
cal(rm, d)

q9

ret(rm, a)
C4

q11

q10

Figure 7 A case in deriving a MatchedMaxPriority= -complete automaton. We use the following notations: C = {call(put, >, true), ret(put, >, true), call(rm, >), ret(rm, >), call(rm, empty), ret(rm, empty)},
C1 = C ∪{call(put, d, < r)}, C2 = C1 ∪{ret(put, b, = r)}, C3 = C2 ∪{ret(rm, d)}, C4 = C ∪{ret(put, b, =
r), ret(rm, d)}.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

{a, b, a1 , d, e, >} of values, we have that C ∩ A(Γ) 6= ∅ for some Γ iff CD ∩ A(Γ) 6= ∅ where CD is
the subset of C that uses only values in D.
The set of executions CD can be represented by a Vector Addition Systems with States (VASS),
since both values and priorities are finite, which implies that each thread and register automata can
be transformed into finite-state automata. To obtain this transformation, the states of the VASS
represent the global variables of CD , while each counter of the VASS then represents the number of
threads which are at a particular control location within a method, with a certain valuation of the local
variables. In this way we transform linearizability problem of priority queue into state-reachability
problem of VASS, which is EXPSPACE-complete. When we consider only finite number of threads,
the value of counters are bounded and then this problem is PSPACE [10].
On the other hand, we can mimic transitions of VASS by a priority queue implementation. To
obtain this, we keep rm unchanged, while in each put method, we first put a value into priority queue,
and then either simulate one step of transitions or record one increase/decrease of a counter, similarly
as that in [4]. In this way we transform the state-reachability problem of VASS into linearizability
problem of priority queue. Based on above discussion, we have the following complexity result. The
detailed proof can be found in Appendix D.8.
I Theorem 17. Verifying whether an implementation in C is linearizable w.r.t. SeqPQ is PSPACEcomplete for a fixed number of threads, and EXPSPACE-complete otherwise.

5

Related work

The theoretical limits of checking linearizability have been investigated in previous works. Checking linearizability of a single execution w.r.t. an arbitrary ADT is NP-complete [11] while checking
linearizability of all the executions of a finite-state implementation w.r.t. an arbitrary ADT specification (given as a regular language) is EXPSPACE-complete when the number of program threads is
bounded [3, 12], and undecidable otherwise [4].
Existing automated methods for proving linearizability of a concurrent object implementation
are also based on reductions to safety verification, e.g., [1, 13, 22]. The approach in [22] considers
implementations where operations’ linearization points are manually specified. Essentially, this approach instruments the implementation with ghost variables simulating the ADT specification at
linearization points. This approach is incomplete since not all implementations have fixed linearization points. Aspect-oriented proofs [13] reduce linearizability to the verification of four simpler
safety properties. However, this approach has only been applied to queues, and has not produced
a fully automated and complete proof technique. The work in [9] proves linearizability of stack
implementations with an automated proof assistant. Their approach does not lead to full automation
however, e.g., by reduction to safety verification.
Our previous work [5] shows that checking linearizability of finite-state implementations of concurrent queues and stacks is decidable. Roughly, we follow the same schema: the recursive procedure in Section 3.1 is similar to the inductive rules in [5], and its extension to concurrent executions
in Section 3.2 corresponds to the notion of step-by-step linearizability in [5]. Although similar in
nature, defining these procedures and establishing their correctness require proof techniques which
are specific to the priority queue semantics. The order in which values are removed from a priority
queue is encoded in their priorities which come from an unbounded domain, and not in the happensbefore order as in the case of stacks and queues. Therefore, the results we introduce in this paper
cannot be inferred from those in [5]. At a technical level, characterizing the priority queue violations
requires a more expressive class of automata (with registers) than the finite-state automata in [5].

XX:15

XX:16

Checking Linearizability of Concurrent Priority Queues

References
1

Parosh Aziz Abdulla, Frédéric Haziza, Lukás Holík, Bengt Jonsson, and Ahmed Rezine. An integrated specification and verification technique for highly concurrent data structures. In TACAS,
pages 324–338, 2013.

2

Dan Alistarh, Justin Kopinsky, Jerry Li, and Nir Shavit. The spraylist: a scalable relaxed priority queue. In Albert Cohen and David Grove, editors, Proceedings of the 20th ACM SIGPLAN
Symposium on Principles and Practice of Parallel Programming, PPoPP 2015, San Francisco,
CA, USA, February 7-11, 2015, pages 11–20. ACM, 2015. URL: http://doi.acm.org/10.
1145/2688500.2688523, doi:10.1145/2688500.2688523.

3

Rajeev Alur, Kenneth L. McMillan, and Doron Peled. Model-checking of correctness conditions
for concurrent objects. Inf. Comput., 160(1-2):167–188, 2000.

4

Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. Verifying concurrent programs against sequential specifications. In ESOP ’13, volume 7792 of LNCS, pages 290–309.
Springer, 2013.

5

Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. On reducing linearizability
to state reachability. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina
Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium,
ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes
in Computer Science, pages 95–107. Springer, 2015. URL: http://dx.doi.org/10.1007/
978-3-662-47666-6_8, doi:10.1007/978-3-662-47666-6_8.

6

Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. Tractable refinement checking
for concurrent objects. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd
Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
2015, Mumbai, India, January 15-17, 2015, pages 651–662. ACM, 2015. URL: http://doi.
acm.org/10.1145/2676726.2677002, doi:10.1145/2676726.2677002.

7

Irina Calciu, Hammurabi Mendes, and Maurice Herlihy. The adaptive priority queue with elimination and combining. In Fabian Kuhn, editor, Distributed Computing - 28th International Symposium, DISC 2014, Austin, TX, USA, October 12-15, 2014. Proceedings, volume 8784 of Lecture
Notes in Computer Science, pages 406–420. Springer, 2014. URL: http://dx.doi.org/10.
1007/978-3-662-45174-8_28, doi:10.1007/978-3-662-45174-8_28.

8

Karlis Cerans. Deciding properties of integral relational automata. In Serge Abiteboul and
Eli Shamir, editors, Automata, Languages and Programming, 21st International Colloquium,
ICALP94, Jerusalem, Israel, July 11-14, 1994, Proceedings, volume 820 of Lecture Notes in
Computer Science, pages 35–46. Springer, 1994. URL: http://dx.doi.org/10.1007/
3-540-58201-0_56, doi:10.1007/3-540-58201-0_56.

9

Mike Dodds, Andreas Haas, and Christoph M. Kirsch. A scalable, correct time-stamped stack. In
POPL ’15. ACM, 2015.

10

Javier Esparza. Decidability and complexity of petri net problems - an introduction. In Lectures on
Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course
on Petri Nets, held in Dagstuhl, September 1996, volume 1491 of Lecture Notes in Computer
Science, pages 374–428. Springer, 1996.

11

Phillip B. Gibbons and Ephraim Korach. Testing shared memories. SIAM J. Comput., 26(4):1208–
1244, 1997.

12

Jad Hamza. On the complexity of linearizability. In NETYS ’15. Springer, 2015.

13

Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. Aspect-oriented linearizability proofs. In
CONCUR, pages 242–256, 2013.

14

Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent
objects. ACM Trans. Program. Lang. Syst., 12(3):463–492, 1990.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

15

16

17

18

19

20

21

22
23

Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329–
363, 1994. URL: http://dx.doi.org/10.1016/0304-3975(94)90242-9, doi:10.
1016/0304-3975(94)90242-9.
Jonatan Lindén and Bengt Jonsson. A skiplist-based concurrent priority queue with minimal
memory contention. In Roberto Baldoni, Nicolas Nisse, and Maarten van Steen, editors, Principles
of Distributed Systems - 17th International Conference, OPODIS 2013, Nice, France, December 16-18, 2013. Proceedings, volume 8304 of Lecture Notes in Computer Science, pages 206–
220. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-319-03850-6_15,
doi:10.1007/978-3-319-03850-6_15.
Yujie Liu and Michael F. Spear. A lock-free, array-based priority queue. In Proceedings of the 17th
ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPOPP 2012,
New Orleans, LA, USA, February 25-29, 2012, pages 323–324, 2012.
Luc Segoufin and Szymon Toruńczyk. Automata based verification over linearly ordered data
domains. In Thomas Schwentick and Christoph Dürr, editors, 28th International Symposium on
Theoretical Aspects of Computer Science, STACS 2011, March 10-12, 2011, Dortmund, Germany, volume 9 of LIPIcs, pages 81–92. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2011.81, doi:10.
4230/LIPIcs.STACS.2011.81.
Nir Shavit and Itay Lotan. Skiplist-based concurrent priority queues. In Proceedings of the 14th
International Parallel & Distributed Processing Symposium (IPDPS’00), Cancun, Mexico, May
1-5, 2000, pages 263–268. IEEE Computer Society, 2000. URL: http://dx.doi.org/10.
1109/IPDPS.2000.845994, doi:10.1109/IPDPS.2000.845994.
Nir Shavit and Asaph Zemach. Scalable concurrent priority queue algorithms. In Brian A.
Coan and Jennifer L. Welch, editors, Proceedings of the Eighteenth Annual ACM Symposium
on Principles of Distributed Computing, PODC, ’99Atlanta, Georgia, USA, May 3-6, 1999,
pages 113–122. ACM, 1999. URL: http://doi.acm.org/10.1145/301308.301339,
doi:10.1145/301308.301339.
Håkan Sundell and Philippas Tsigas. Fast and lock-free concurrent priority queues for multi-thread
systems. In 17th International Parallel and Distributed Processing Symposium (IPDPS 2003), 2226 April 2003, Nice, France, CD-ROM/Abstracts Proceedings, page 84. IEEE Computer Society,
2003.
Viktor Vafeiadis. Automatically proving linearizability. In CAV ’10, volume 6174 of LNCS, pages
450–464.
Pierre Wolper. Expressing interesting properties of programs in propositional temporal logic. In
POPL ’86: Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, pages 184–193. ACM Press, 1986.

XX:17

XX:18

Checking Linearizability of Concurrent Priority Queues

A

Definition of SeqPQ and Proof of Lemma 5

A labelled transition system (LT S) is a tuple A = (Q, Σ, →, q0 ), where Q is a set of states, Σ is an
alphabet of transition labels, →⊆ Q × Σ × Q is a transition relation and q0 is the initial state.
Let us model priority queue as an LTS PQ = (Q, Σ, →, q0 ) as follows:
-

Each state of Q is a function from P into a finite sequence over D.
The initial state q0 is a function that maps each element in P into .
Σ = {put(a, p), rm(a), rm(empty)|a ∈ D, p ∈ P}.
The transition relation → is defined as follows:
put(a,p)

- q1 −−−−−→ q2 , if q1 maps p into some finite sequence l, and q2 is the same as q1 , except for
p, where it maps p into a · l.
rm(a)

- q1 −−−→ q2 , if q1 maps p into l · a for some finite sequence l, and q2 is the same as q1 , except
for p, where it maps p into l. We also require that for each priority p0 such that p0 ≺ p, q1 and
q2 map p0 into .
rm(empty)

- q1 −−−−−→ q2 , if q1 = q2 , and they maps each element in P into .
β1

β2

βk

A path of an LTS is a finite transition sequence q0 −→ q1 −→ . . . −→ qk for k ≥ 0, where
q0 is the initial state of the LTS. A trace of an LTS is a finite sequence β1 · β2 · . . . · βk , where
β1

β2

βk

k ≥ 0 if there exists a path q0 −→ q1 −→ . . . −→ qk of the LTS. Let SeqPQ be the set of
traces of PQ. The following lemma states that SeqPQ is indeed the set of sequences obtained
by renaming sequences accepted by Check-PQ-Seq. Given Γ ∈ {EmptyRemove, Unmatched−
Γ
MaxPriority, MatchedMaxPriority}, let us use l2 −
→ l1 to mean that when we use Check-PQ-Seq to
check l2 , we choose the branch of Has-Γ and finally recursively call Check-PQ-Seq to check l1 .

Lemma 5: Check-PQ-Seq(e) = true iff e ∈ SeqPQ, for every data-differentiated sequential execution e.
Proof. Let SeqPQf be the set of data-differentiated sequences, such that e ∈ SeqPQf , if Check-PQSeq(e) = true. We need to prove that SeqPQf = SeqPQ6= . We prove SeqPQf ⊆ SeqPQ6= by
induction.
- It is obvious that  ∈ SeqPQ.
MatchedMaxPriority

- If l1 ∈ SeqPQ6= and l2 −−−−−−−−−−−→ l1 . Then we need to prove that l2 ∈ SeqPQ. We know
that l1 = u · v · w, such that MatchedMaxPriority-Seq(l2 , x) holds and l2 = u · put(x, p) · v ·
rm(x) · w.
Assume that u = α1 · . . . · αi , v = αi+1 · . . . · αj and w = αj+1 · . . . · αm . Assume that
αj+1
αj
α
α1
αi
α
q0 −→
q1 . . . −→
qi −−i+1
→ qi+1 . . . −→ qj −−→ qj+1 . . . −−m
→ qm is the path of l1 on PQ. For
each i ≤ k ≤ j, let qk0 be the same as qk , except that qk0 maps p into x · lk and qk maps p into lk
for some finite sequence lk .
α

α

put(x,p)

1
i
We already know that q0 −→
q1 . . . −→
qi , and it is obvious that qi −−−−−→ qi0 . Since (1) all
put with priority p is in u, and (2) in u · v, only values with priority either incomparable, or
less, or equal than p is removed, we can see that it is safe to add to each qk (1 ≤ k ≤ j) with
αj
α
0
a newest x with priority p. Or we can say, qi0 −−i+1
→ qi+1
. . . −→ qj0 are transitions of PQ. Since
matched≺ (u · v, p) holds, we can see that qj maps each priority that is smaller than p into  and
maps p into , and qj0 maps each priority that is smaller than p into  and maps p into x. Then,

Ahmed Bouajjani, Constantin Enea, and Chao Wang

XX:19

αj+1

rm(x)

α

→ qm . Therefore, we
we can see that qj0 −−−→ qj . We already know that that qj −−→ qj+1 . . . −−m
can see that l2 = u · put(x, p) · v · rm(x) ∈ SeqPQ.
UnmatchedMaxPriority

- If l1 ∈ SeqPQ6= and l2 −−−−−−−−−−−−−→ l1 . Then we need to prove that l2 ∈ SeqPQ. We
know that l1 = u · v, such that UnmatchedMaxPriority-Seq(l2 , x) holds and l2 = u · put(x, p) · v.
α
αi
α1
qi −−i+1
→
q1 . . . −→
Assume that u = α1 · . . . · αi and v = αi+1 · . . . · αm . Assume that q0 −→
αm
0
qi+1 . . . −−→ qm is the path of l1 on PQ. For each i ≤ k ≤ m, let qk be the same as qk , except
that qk0 maps p into x · lk and qk maps p into lk for some finite sequence lk .
put(x,p)

α

α

i
1
qi , and it is obvious that qi −−−−−→ qi0 . Since (1) all put
q1 . . . −→
We already know that q0 −→
with priority p is in u, (2) in u · v, only values with priority either incomparable, or less, or equal
than p is removed, we can see that it is safe to add to each qk (1 ≤ k ≤ m) with a newest x with
α
α
0
0
→ qm
are transitions of PQ. Therefore, we can see
priority p. Or we can say, qi0 −−i+1
→ qi+1
. . . −−m
that l2 = u · put(x, p) · v ∈ SeqPQ.

EmptyRemove

- If l1 ∈ SeqPQ6= and l2 −−−−−−−−→ l1 . Then we need to prove that l2 ∈ SeqPQ. We know
that l1 = u · v, such that EmptyRemove-Seq(l2 , o) holds, and l2 = u · rm(empty) · v with
o = rm(empty).
α
αi
α1
qi −−i+1
→
q1 . . . −→
Assume that u = α1 · . . . · αi and v = αi+1 · . . . · αm . Assume that q0 −→
αm
qi+1 . . . −−→ qm is the path of l1 on PQ.
α1
αi
We already know that q0 −→
q1 . . . −→
qi . Since matched(u) holds, we can see that qi maps
rm(empty)

α

α

each element in P into , and then qi −−−−−→ qi . We already know that qi −−i+1
→ qi+1 . . . −−m
→ qm .
Therefore, we can see that l2 = u · rm(empty) · v ∈ SeqPQ.
To prove that SeqPQ6= ⊆ SeqPQf , we show that given l2 ∈ SeqPQ6= , how to construct a
Γ

sequence l1 , such that l2 −
→ l1 for some Γ, and l1 ∈ SeqPQ. Based on this, we can decompose a
sequence of SeqPQ into , and this process ensures that this sequence is in SeqPQf . Note that from
a l2 we may construct more than one l1 , and this does not influence the correctness of our proof.
- If Has-EmptyRemoves(l2 ): Assume that l2 = u · rm(empty) · v. It is easy to see that matched(u)
EmptyRemove

holds. Let l1 = u·v. It is easy to see that l2 −−−−−−−−→ l1 , and UnmatchedMaxPriority-Seq(l2 , o)
holds for some o = rm(empty).
α1
αi
Assume that u = α1 ·. . .·αi and v = αi+1 ·. . .·αm . Since We already know that q0 −→
q1 . . . −→
rm(empty)

α

α

qi −−−−−→ qi0 −−i+1
→ qi+1 . . . −−m
→ qm is transitions of PQ. It is easy to see that qi = qi0 , and they
α
α1
αi
α
map each element in P into . Then we can see that q0 −→
q1 . . . −→
qi −−i+1
→ qi+1 . . . −−m
→ qm
is transitions of PQ, and l1 ∈ SeqPQ.
- If Has-UnmatchedMaxPriority(l2 ): Assume that l2 = u · put(x, p) · v, such that all put with
priority p of u · v is in u. Let l1 = u · v. According to construction of PQ, we can see that
UnmatchedMaxPriority

UnmatchedMaxPriority-Seq(l2 , x) holds, and l2 −−−−−−−−−−−−−→ l1 .
α1
Assume that u = α1 · . . . · αi and v = αi+1 · . . . · αm . We already know that pa = q0 −→
put(x,p)

α

α

α

i
q1 . . . −→
qi −−−−−→ qi+ −−i+1
→ qi+1 . . . −−m
→ qm are transitions of PQ. For each i+1 ≤ k ≤ m,
0
let qk be the same as qk , except that qk maps p into some x · lk for some finite sequence lk , and
qk0 maps p into lk . Since (1) all put with priority p of u · v is in u and (2) p is one of maximal
priority of l2 , it is safe to remove x without influence other transitions of pa. Or we can say,
α
α1
αi
α
0
0
q0 −→
q1 . . . −→
qi −−i+1
→ qi+1
. . . −−m
→ qm
are transitions of PQ. Therefore, l1 ∈ SeqPQ.
- If Has-MatchedMaxPriority(l2 ): Assume that l2 = u · put(x, p) · v · rm(x) · w, such that all put
with priority p of u · v · w is in u. Let l1 = u · v · w. According to construction of PQ, we can

MatchedMaxPriority

see that MatchedMaxPriority-Seq(l2 , x) holds, and l2 −−−−−−−−−−−→ l1 .
Assume that u = α1 · . . . · αi , v = αi+1 · . . . · αj and w = αj+1 · . . . · αm . We already know
α

α

put(x,p)

α

αj

rm(x)

αj+1

α

1
i
that q0 −→
q1 . . . −→
qi −−−−−→ qi+ −−i+1
→ qi+1 . . . −→ qj −−−→ qj+ −−→ qj+1 . . . −−m
→ qm .

XX:20

Checking Linearizability of Concurrent Priority Queues

For each i+1 ≤ k ≤ j, let qk0 be the same as qk , except that qk maps p into x · lk for some
finite sequence lk , and qk0 maps p into lk . Since (1) p is one of maximal priority in l2 , (2) x
is the newest value with priority p in l2 , and (3) x is not removed until rm(x), we know that
whether we keep x or remove it will not influence transitions from qi+1 to qj . Then we can see
αj+1
αj
α
α
αi
α1
0
→ qm are transitions of PQ.
qi −−i+1
→ qi+1
. . . −→ qj0 −−→ qj+1 . . . −−m
q1 . . . −→
that q0 −→
Therefore, l1 ∈ SeqPQ.
This completes the proof of this lemma.

B

J

J

Proofs in Section 2

Lemma 3: SeqPQ is closed under projection, i.e., proj(e) ⊆ SeqPQ for each e ∈ SeqPQ.
Proof. By Lemma 5, SeqPQ is equivalent to the set of sequences obtained by renaming sequences
accepted by Check-PQ-Seq. It is easy to see that for the predicates of Check-PQ-Seq, if a sequential
execution satisfy it, then its sub-sequence also satisfy it. For example, if matched(u) holds, then
matched(u|D) holds for each set D of values. This completes the proof of this lemma.
J
J
Lemma 4: A data-independent implementation I is linearizable w.r.t a data-independent set S of
sequential executions, if and only if I6= is linearizable w.r.t. S6= .
Proof. To prove the only if direction, given a data-differentiated execution e ∈ I6= . By assumption, it is linearizable with respect to a sequential execution l ∈ S, and the bijection between the
operations of e and the operations of l ensures that l is differentiated and belongs to S6= .
To prove the if direction, given an execution e ∈ I. By data independence of I, we know that
there exists e0 ∈ I6= and a renaming function r, such that r(e0 ) = e. By assumption, e0 is linearizable
with respect to a sequential execution l0 ∈ S6= . Let l = r(l0 ). By data independence of S it is easy
to see that l ∈ S, and it is easy to see that e v l using the same bijection used for e0 v l0 . J J

C
C.1

Proofs in Section 3
Definition of Step-by-Step linearizablity

We introduce the notion of step-by-step linearizability, which means that from a linearization of
e \ x that satisfy the requirements of priority queue, we can obtain a linearization of e that satisfy
the requirements of priority queue. Its formal definition is as follows:
I Definition 18. Given Γ ∈ {EmptyRemove, UnmatchedMaxPriority, MatchedMaxPriority}, Γ
is step-by-step linearizability, if for each data-differentiated execution e where Γ-Conc(e, α) for
some α, then e \ α v SeqPQ ⇒ e v SeqPQ.
SeqPQ is step-by-step linearizability, if each Γ is step-by-step linearizability.
Our notion of step-by-step linearizability is inspired by the step-by-step linearizability in [5].
Given a data-differentiated execution e, we can obtain a sequence e0 from e by adding put(a, p)
(resp., rm(a), rm(empty)) between each pair of call(put, a, p) and ret(put, a, p) (resp., call(rm, a)
and ret(rm, a), call(rm, empty) and ret(rm, empty)). Such e0 is called an execution with linearization
points, and we call the projection of e0 into m(a, b) the linearization of e.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

C.2

XX:21

Obtaining New Sequences while Ensuring that they are in SeqPQ

Before we prove the step-by-step linearizability of SeqPQ, we introduce several lemmas, which are
used to ensure some sub-sequences of SeqPQ still belongs to SeqPQ. Given a data-differentiated
sequence l and one of its maximal priority p, let Oc (l, p) and Oi (l, p) be the set of operations with
priorities comparable with p and incomparable with p in l, respectively. Similarly we can define
Dc (l, p) and Di (l, p) for se of values instead of set of operations. We can see that each priority of
values in Oi (l, p) is either larger or incomparable with priorities of values in Oc (l, p).
The following lemma shows that if a new sequence is generated by erasing some operations in
Oc (l, p) while keeping the remaining Oc (l, p) sub-sequences in SeqPQ, then this new sequence is
still in SeqPQ. Note that this is different from projection on value.
I Lemma 19. Given a data-differentiated sequential execution l ∈ SeqPQ and a maximal priority
p in l, where l does not contain rm(empty). Let l0 be generated from l by discarding some operations
in Oc (l, p), and l0 |Oc (l,p) ∈ SeqPQ. Then, l0 ∈ SeqPQ.
o

o

1
→ qm be the path of l in PQ. Assume that l0 is
q1 . . . −−m
Proof. Let l = o1 · . . . · om , and q0 −→
generated from l by discarding oind1 , . . . , oindn . Let D be the set such that D contains a, if put(a, _)
is in oind1 , . . . , oindn . For each i, let qi0 be generated from qi by erasing values in D.
oj+1
0
For each qj0 with j 6= ind_-1, if oj+1 is put, then it is obvious that qj0 −−→ qj+1
. Else, assume
oj+1 = rm(a),

- If rm(a) ∈ Oc (l, p): By assumption, l0 |Oc (l,p) ∈ SeqPQ. Therefore, a is in qj0 and is the
should-be-removed value in Oc (l, p). Since each priority of values in Oi (l, p) is either larger
or incomparable with priorities of values in Oc (l, p), we can removed ac from qj0 , and then
oj+1

0
qj0 −−→ qj+1
.
rm(a)

- If rm(a) ∈ Oi (l, p): By assumption we know that qj −−−→ qj+1 . Since qj0 contains the same
oj+1

0
Di (l, p) values as qj and qj0 contains less Dc (l, p) values than qj , we can see that qj0 −−→ qj+1
.
0
0
0
For each qindj-1
, it is easy to see that qindj-1
= qindj
. Therefore, we can see that l0 = o1 · . . . oind1-1 ·
oind1+1 · . . . ∈ SeqPQ.
J
J

The following lemma shows that if a new sequence is generated by from some time point, erasing
operations in Oi (l, p), then this new sequence is still in SeqPQ.
I Lemma 20. Given a data-differentiated sequential execution l ∈ SeqPQ and a maximal priority
p in l, where l does not contain rm(empty). Let l0 be generated from l by discarding operations in
Oi (l, p) from some time point, then, l0 ∈ SeqPQ.
o

o

1
Proof. Let l = o1 · . . . · om , and q0 −→
q1 . . . −−m
→ qm be the path of l in PQ. Assume that l0 is
generated from l by discarding all operations oi if (1) oi ∈ Oi (l, p) and (2) i ≥ k for a specific index
k. Let D be a set such that a ∈ D, if put(a, _) is in l and not in l0 . For each 0 ≤ i ≤ m, let qi0 be
generated from qi by erasing values in D.
Let l0 = o01 · . . . · o0n , and let f be a function, such that f (i) = j, if o0i = oj .

o

o

1
0
→ qk-1
.
- We can see that f maps each 0 ≤ i ≤ k-1 into i, and q00 −→
q10 . . . −−k-1
0
0
0
0
- It is easy to see that qk-1 = qf (k)−1 , and for each i > k, qf (k) = qf (k+1)−1 .

o

k
- If of (k) is a put operation, then it is obvious that qf0 (k)−1 −→
qf0 (k) . Else, if of (k) = rm(a), we
0
0
can see a is in qf (k)−1 , and since (1) qf (k)−1 contains the same Dc (l, p) values as qf (k)−1 and
qf0 (k)−1 contains less Di (l, p) values than qf (k)−1 , and (2) each priority of values in Oi (l, p) is

o

k
either larger or incomparable with priorities of values in Oc (l, p), we can see that qf0 (k)−1 −→
qf0 (k) . Similarly we can prove the case of of (j) with j > k.

XX:22

Checking Linearizability of Concurrent Priority Queues

J

This completes the proof of this lemma.

J

The following lemma shows that we can make put with maximal priority to happen earlier.
I Lemma 21. Given a data-differentiated sequential execution l ∈ SeqPQ and a maximal priority
p in l, where l does not contain rm(empty). Let l = l1 · l2 . Let l3 be the projection of l2 into
{put(_, p)}, and l4 be the projection of l2 into other operations. Then, l0 = l1 · l3 · l4 ∈ SeqPQ.
o

o

1
→ qm be the path of l in PQ. Let l1 = o1 · . . . · on ,
Proof. Let l = o1 · . . . · om , and q0 −→
q1 . . . −−m
let l2 = on+1 · . . . · om , let l3 = o0n+1 · . . . · o0k , let l4 = o0k+1 · . . . · o0m . Let f be a function, such that
f (i) = j, if o0i = oj .
Let qi0 be constructed as follows:

- For 0 ≤ i ≤ n, let qi0 = qi .
- For n+1 ≤ i ≤ k, let qi0 be obtained from qn by adding values in o0n+1 · . . . · o0i with priority p and
in the same order.
- For k+1 ≤ i ≤ m, let qi0 be obtained from qf (i) by adding values which are (1) with priority p,
(2) in o0n+1 · . . . · o0i and not removed by o1 · . . . · of (i) . The order of adding them is the same as
o0n+1 · . . . · o0i .
Then, our proof proceeds as follows:
o

o

o

o

n+1
1
n
k
0
- It is obvious that q00 −→
q10 . . . −→
qn0 and qn0 −−
→ qn+1
. . . −→
qk0 .

of (k+1)

0
- For qk+1
: We already know that qf (k+1)−1 −−−−−→ qf (k+1) , and it is easy to see that qf (k+1)−1
is obtained from qn by adding values in on+1 · . . . · of (k+1)−1 .
0
is obtained
We can see that qk0 is obtained from qn by adding values in o0n+1 · . . . · o0k , and qk+1
0
0
from qf (k+1) by adding values which are (1) with priority p, (2) in on+1 · . . . · oi and not removed
by o1 · . . . · of (k+1) .

0
- If of (k+1) is an operation of non-p values, then qk+1
is obtained from qf (k+1) by adding
0
0
values in on+1 · . . . · oi . Since non-p priority is either smaller or incomparable with p, we can
of (k+1)

0
see that qk0 −−−−−→ qk+1
.
- Otherwise, it is only possible that of (k+1) = rm(a) for some value a with priority p. We can
0
see that qk+1
is obtained from qf (k+1) by adding values in o0n+1 · . . . · o0k and then remove
of (k+1)

a. Since qf (k+1)−1 −−−−−→ qf (k+1) , in qf (k+1)−1 ( and also in qk0 ), there is no value with
priority less than p, and a is the first-input value of priority p. Therefore, we can see that
of (k+1)
0
qk0 −−−−−→ qk+1
.
of (k+i)

0
- For qk+i
with i > 1: We already know that qf (k+i)−1 −−−−→ qf (k+i) , and qf (k+i)−1 is obtained
from qf (k+i−1) by adding values in of (k+i−1)+1 · . . . · of (k+i)−1 .
0
0
We can see that qk+i−1
(resp., qk+i
) is obtained from qf (k+i−1) (resp., qf (k+i) ) by adding values
which are (1) with priority p, (2) in o0n+1 · . . . · o0i and not removed by o1 · . . . · of (k+i−1) (resp.,
o1 · . . . · of (k+i) ).

0
- If of (k+i) is an operation of non-p values, then qk+i
is obtained from qf (k+i) by adding values
0
0
which are (1) with priority p, (2) in on+1 · . . . · oi and not removed by o1 · . . . · of (k+i−1) . Since
of (k+i)

0
0
non-p priority is either smaller or incomparable with p, we can see that qk+i-1
−−−−→ qk+i
.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

XX:23

- Otherwise, it is only possible that of (k+i) = rm(a) for some value a with priority p. We can
0
see that qk+i
is obtained from qf (k+i) by adding values in o0n+1 · . . . · o0k and then remove
of (k+i)

0
a. Since qf (k+i)−1 −−−−→ qf (k+i) , in qf (k+i)−1 ( and also in qk+i-1
), there is no value with
priority less than p, and a is the first-input value of priority p. Therefore, we can see that
of (k+i)
0
0
−−−−→ qk+i
.
qk+i-1

J

This completes the proof of this lemma.

J

The following lemma shows that if a new sequence is generated by make some Oi (l, p) behaviors
to happen earlier, then this new sequence is still in SeqPQ.
I Lemma 22. Given a data-differentiated sequential execution l ∈ SeqPQ and a maximal priority
p in l, where l does not contain rm(empty). Let l|Oi (l,p) = l1 · l2 , let l0 = l1 · l3 , where l3 is the
projection of l into non-l1 operations. Then, l0 ∈ SeqPQ.
o

o

1
→ qm be the path of l in PQ. Let l1 = o01 · . . . · o0n ,
Proof. Let l = o1 · . . . · om , and q0 −→
q1 . . . −−m
let l3 = o0n+1 · . . . · o0m . Let f be a function, such that f (i) = j, if o0i = oj . Let D be the set of values
which are added and not removed in o01 · . . . · o0n .
Let qi0 be constructed as follows:

o0

o0

1
n
- It is easy to see that l1 ∈ SeqPQ, and let q00 −→
q10 . . . −→
qn0 be the path of l1 in PQ.
0
- For n+1 ≤ i ≤ m, let qi be obtained from qf (i) by adding values in D. The order of adding
them is the same as o01 · . . . · o0n .

Then, our proof proceeds as follows:
o0

o0

1
n
- We already know that q00 −→
q10 . . . −→
qn0 .

of (n+i)

0
- For qn+i
: We already know that qf (n+i)−1 −−−−−→ qf (n+i) , and it is easy to see that qf (n+i)−1
is obtained from qf (n+i−1) by adding D-values in of (n+i−1)+1 · . . . · qf (n+i)−1 .
0
0
) is obtained from qf (n+i−1) (resp., qf (n+i) ) by adding remanWe can see that qn+i−1
(resp., qn+i
ning values in D.

- If of (n+1) is an operation of Oc (l, p) values, since priority in Oi (l, p) is either larger or inof (n+1)

0
comparable with priority in Oc (l, p), we can see that qn0 −−−−−→ qn+1
.
- Otherwise, it is only possible that of (k+1) = rm(a) for some value a in Oc (l, p). Since
of (n+i)

0
qf (n+i)−1 −−−−−→ qf (n+i) , in qf (n+i)−1 ( and also in qn+i-1
), there is no value with priority
of (n+i)

0
less than p, and a is the first-input value of priority p. Therefore, we can see that qn+i-1
−−−−−→
0
qn+i
.

This completes the proof of this lemma.

J

J

The following lemma shows that if a new sequence is generated by replacing a prefix with another one which make the priority queue has same content, then this new sequence is still in SeqPQ.
I Lemma 23. Given a data-differentiated sequential execution l ∈ SeqPQ. Let l = l1 · l2 .
Given l3 ∈ SeqPQ. Assume that the priority queue has same content after executing l1 and l3 . Let
l0 = l3 · l2 . Then, l0 ∈ SeqPQ.

XX:24

Checking Linearizability of Concurrent Priority Queues
o

o

1
→ qm be the path of l in PQ. Let l1 = o1 · . . . · lk ,
q1 . . . −−m
Proof. Let l = o1 · . . . · om and let q0 −→

o01

o0n

l3 = o01 · . . . · o0n and let q0 −→ q10 . . . −→ qn0 be the path of l3 in PQ.

o0

o0

o

k+1
1
n
By assumption we know that qk = qn0 . Then it is not hard to see that q0 −→
q10 . . . −→
qn0 −−
→
om
0
0
qk+1 . . . −−→ qm is a path in PQ, and then l ∈ SeqPQs . By Lemma 5, we know that l ∈ SeqPQ.
J
J

C.3

Proving Step-by-Step Linearizability of SeqPQ

With the help of Lemma 19, Lemma 20, Lemma 21, Lemma 22 and Lemma 23, we can now prove
that MatchedMaxPriority is step-by-step linearizability. Here we use call(o) and ret(o) as the call
and return action of operation o, respectively.
I Lemma 24. For each data-differentiated execution e where MatchedMaxPriority-Conc(e, x) for
some x, then e \ x v SeqPQ ⇒ e v SeqPQ.
Proof. By assumption we know that there exists l, such that e v l and MatchedMaxPriority-Seq(l, x)
holds. Let p be the priority of x, then l = u · put(x, p) · v · rm(x) · w for some u, v and w. Let
e0 = e \ x. By assumption there exists sequence l0 , such that e0 v l0 ∈ SeqPQ. Let elp be an
execution with linearization points of e and the linearization points is added according to l0 . Or we
can say, elp is generated from e by instrumenting linearization points, and the projection of elp into
operations is l0 . Let lv0 be the shortest prefix of l0 that contains all operation of u · v.
Let U , V and W be the set of operations of u, v and w, respectively. Let us change Oi (l, p)
elements in U , V and W , while keep Oc (l, p) elements unchanged. We proceed by a loop: In the
first round of the loop, we start from the first Oi (l, p)-value of lv0 , and let it be oh ,
- Case 1: If in elp , the linearization point of oh is before ret(rm, x), and no Oc (l, p)-value in W
happens before oh . Then, oh is in the new version of U ∪ V .
- Case 2: Else, if in elp , the linearization point of oh is before ret(rm, x), and there exists Oc (l, p)value ow in W , such that ow <hb oh . Then, in lv0 , we put oh and all Oi (l, p)-value whose
linearization points is after the linearization point of oh into new version of W , and then stop the
process of changing U , V and W .
- Case 3: Else, if in elp , the linearization point of oh is after ret(rm, x). Then, in lv0 , we put oh
and all Oi (l, p)-value whose linearization points is after the linearization point of oh into new
version of W , and then stop the process of changing U , V and W .
In the next round of the loop, we consider the second Oi (l, p)-value of lv0 , and so on. Our process
proceed, until either all element in lv0 are in new version of U ∪ V , or case 2 or case 3 happens and
this process terminates. Let U 0 ∪ V 0 and W 0 be the new version of U ∪ V and W after the process
terminates, respectively. Let O+ be the set of operations that are moved into U 0 ∪ V 0 in the process,
and let O− be the set of operations that are moved into W 0 in the process.
0
Let lu’v’
be the projection of l0 into U 0 ∪ V 0 , let Ox be the set of put(_, p) while the value is
0
not x in h. Let la00 be the longest prefix of lu’v’
, where linearization of each operation of la00 is before
00
0
ret(put, b) in elp . Let ld be the projection of l into operations of Ox that are not in la00 . Let l100 = la00 ·ld00 .
0
that are not in l100 . Let l300 be the projection of l0
Let l200 be the projection of l0 into operations of lu’v’
0
00
00
into operations which are not in lu’v’ . Let l = l1 · put(x, p) · l200 · rm(x) · l300 .
To prove e v l00 , we define a graph G whose nodes are the operations of h and there is an edge
from operation o1 to o2 , if one of the following case holds
- o1 happens-before o2 in h,
- the operation corresponding to o1 in l00 is before the one corresponding to o2 .

Ahmed Bouajjani, Constantin Enea, and Chao Wang

Assume there is a cycle in G. According the the property of interval order and the fact that the
order of l00 is total, we know that there must exists o1 and o2 , such that o1 happens-before o2 in h,
but the corresponding operations are in the opposite order in l00 . Then, we consider all possible case
of o1 and o2 as follows: Let Oa and Od be the set of operations in la00 and ld00 , respectively.
- If o2 ∈ l100 ∧ o1 ∈ l100 :
- If o1 , o2 ∈ Oa or o1 , o2 ∈ Od : Then l0 contradicts with happen before relation of h.
- If o2 ∈ Oa ∧ o1 ∈ Od : Then the order of linearization points of elp contradicts with happen
before relation of h.
- If o2 ∈ l100 ∧ o1 = put(x, p):
- If o2 ∈ Oa : This is impossible, since the linearization point of operations in Oa is before
ret(put, x, p) in elp .
- If o2 ∈ Od : Then l contradicts with happen before relation of h.
- If o2 ∈ l100 ∧ o1 ∈ l200 :
- If o2 ∈ Oa : This violates the order of linearization point in elp .
- If o2 ∈ Od : According to l, we can see that put(x, p) does not happen before any operation
in Ox . Then we can see that the linearization point of o1 is before ret(put, x, p) and o1 ∈ Oa .
This violates that o1 ∈ l200 .
- If o2 ∈ l100 ∧ o1 = rm(x):
- If o2 ∈ U ∪ V : Then l contradicts with happen before relation of h.
- If o2 ∈ O+ : This is impossible, since the linearization point of operations in O+ is before
ret(rm, x) in elp .
- If o2 ∈ l100 ∧ o1 ∈ l300 :
- If o1 ∈ W ∧ o2 ∈ U ∪ V : Then l contradicts with happen before relation of h.
- If o1 ∈ W ∧ o2 ∈ O+ :
- If o1 ∈ Oi (l, p): Then according to the construction process of U 0 ∪ V 0 and W 0 , we can
see that o1 ∈ O+ and then o1 ∈ U 0 ∪ V 0 , which contradicts that o1 ∈ l300 .
- If o1 ∈ Oc (l, p): Then according to the construction process of U 0 ∪ V 0 and W 0 , we can
see that o2 ∈ O− , which contradicts that o2 ∈ O+ .
- If o1 ∈ O− ∧ o2 ∈ U ∪ V :
- If the reason of o1 ∈ O− is case 2: Let oh be as in case 2. Then there exists Oc (l, p)-value
ow ∈ W , and in elp , ret(ow ) is before call(oh ), the linearization point of oh is before
the linearization point of o1 , and ret(o1 ) is before call(o2 ). Therefore, we can see that
ow <hb o2 , and then l contradicts with happen before relation of h.
- If the reason of o1 ∈ O− is case 3: Let oh be as in case 3. Then in elp , ret(rm, x) is before
the linearization point of oh , the linearization point of oh is before the linearization point
of o1 , and ret(o1 ) is before call(o2 ). Therefore, we can see that rm(x) <hb o2 , and then l
contradicts with happen before relation of h.
- If o1 ∈ O− ∧ O2 ∈ O+ : This is impossible, since in elp , the linearization points of operations
in O+ is before the linearization points of operations in O− .
- If o2 = put(x, p) ∧ o1 ∈ l200 : This is impossible, since in elp , the linearization points of operations
in l200 is after ret(put, x, p).
- If o2 = put(x, p) ∧ o1 = rm(x): Then l contradicts with happen before relation of h.
- If o2 = put(x, p) ∧ o1 ∈ l300 :
- If o1 ∈ W : Then l contradicts with happen before relation of h.
- If o1 ∈ O− :

XX:25

XX:26

Checking Linearizability of Concurrent Priority Queues

-

-

- If the reason of o1 ∈ O− is case 2: Let oh be as in case 2. Then there exists Oc (l, p)-value
ow ∈ W , and in elp , ret(ow ) is before call(oh ), the linearization point of oh is before the
linearization point of o1 , and ret(o1 ) is before call(put, x, p). Therefore, we can see that
ow <hb put(x, p), and then l contradicts with happen before relation of h.
- If the reason of o1 ∈ O− is case 3: Let oh be as in case 3. Then in elp , ret(rm, x) is before
the linearization point of oh , the linearization point of oh is before the linearization point
of o1 , and ret(o1 ) is before call(put, x, p). Therefore, we can see that rm(x) <hb put(x, p),
and then l contradicts with happen before relation of h.
If o2 ∈ l200 ∧ o1 ∈ l200 : Then l0 contradicts with happen before relation of h.
If o2 ∈ l200 ∧ o1 = rm(x): We can prove this similarly as the case of o2 ∈ l100 ∧ o1 = rm(x).
If o2 ∈ l200 ∧ o1 ∈ l300 : We can prove this similarly as the case of o2 ∈ l100 ∧ o1 ∈ l300 .
If o2 = rm(x) ∧ o1 ∈ l300 :
- If o1 ∈ W : Then l contradicts with happen before relation of h.
- If o1 ∈ O− :
- If the reason of o1 ∈ O− is case 2: Let oh be as in case 2. Then there exists Oc (l, p)-value
ow ∈ W , and in elp , ret(ow ) is before call(oh ), the linearization point of oh is before the
linearization point of o1 .
Since l is consistent with the happen before order of h, we can see that call(rm, x) is before
ret(ow ). Therefore, we can see that the linearization point of o1 is after call(rm, x), and
then it is impossible that o1 <hb rm(x).
- If the reason of o1 ∈ O− is case 3: Let oh be as in case 3. Then in elp , ret(rm, x) is before
the linearization point of oh , and the linearization point of oh is before the linearization
point of o1 . Therefore, we can see that the linearization point of o1 is after ret(rm, x), and
then it is impossible that o1 <hb rm(x).
If o2 ∈ l300 ∧ o1 ∈ l300 : Then l0 contradicts with happen before relation of h.
Therefore, we know that G is acyclic, and then we know that h v l00 .
It remains to prove that l00 ∈ SeqPQ. The process for proving l00 ∈ SeqPQ is as follows:

- Since l0 ∈ SeqPQ and lv0 is a prefix of l0 , it is obvious that lv0 ∈ SeqPQ.
0
- lu’v’
can be obtained from lv0 as follows:
- Discard Oc (l, p)-value that are in W and keep Oc (l, p)-value in U ∪ V unchanged.
- From some time point, discard all the Oi (l, p) operations after this time point.
From matched≺ (u · v, p), we can see that Oc (l, p)-value in U · V is matched, and then it is easy
to see that the projection of lv0 in to Oc (l, p)-value in U · V is still in SeqPQ. By Lemma 19 and
0
Lemma 20, we can see that lu’v’
∈ SeqPQ.
00
00
0
- l1 · l2 can be obtained from lu’v’
as follows: Execute until reaching some time point t, then first
execute all Ox operations after t, and then execute remanning operations. By Lemma 21, we can
see that l100 · l200 ∈ SeqPQ.
- Let le0 be obtained from l0 by discarding Oc (l, p)-value in U · V . By Lemma 3, we can see that
le0 ∈ SeqPQ.
- Let le0 |Oi (l,p) = lf0 · lg0 , where lf0 is the projection of Oi (l, p)-value in U · V . Let lh0 be obtained
from le0 by discarding operations in lf0 . By Lemma 22, we can see that lf0 · lh0 ∈ SeqPQ.
- By Lemma 3, it is obvious that lf0 ∈ SeqPQ. From matched≺ (u · v, p), we can see that the
content of priority queue after executing l100 · l200 is the same as after executing lf0 . By Lemma 23,
we can see that l100 · l200 · lh0 ∈ SeqPQ. It is easy to see that lh0 = l300 , and then l100 · l200 · l300 ∈ SeqPQ.
- Since MatchedMaxPriority-Seq(l, x) holds, it is easy to see that l00 = l100 ·put(x, p)·l200 ·rm(x)·l300 ∈
SeqPQ.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

Therefore, we prove that e v l00 ∈ SeqPQ. This completes the proof of this lemma.

XX:27

J

J

I Lemma 25. For each data-differentiated execution e where UnmatchedMaxPriority-Conc(e, x)
for some x, then e \ x v SeqPQ ⇒ e v SeqPQ.
Proof. By assumption we know that there exists l, such that e v l and UnmatchedMaxPriority-Seq(l, x)
holds. Let p be the priority of x, then l = u · put(x, p) · v for some u and v. Let e0 = e \ x. By
assumption there exists sequence l0 , such that e0 v l0 ∈ SeqPQ. Let elp be an execution with linearization points of e and the linearization points is added according to l0 . Or we can say, elp is
generated from e by instrumenting linearization points, and the projection of elp into operations is l0 .
Let lv0 be the shortest prefix of l0 that contains all operations of u · v.
Let la00 be the longest prefix of l0 such that linearization point of each operation of la00 is before
ret(put, x, p) in elp . Let Ox be the set of put(_, p) while the value is not x in h. Let ls00 be the
projection of l0 into operations of Ox that are not in la00 . Let l100 = la00 · ls00 . Let l200 be the projection of
l0 into operations of l0 that are not in l100 . Let l00 = l100 · put(x, p) · l200 .
To prove h v l00 , we define graph G as in Lemma 24. Assume that there is a cycle in G, then
there must exists o1 and o2 , such that o1 happens-before o2 in h, but the corresponding operations
are in the opposite order in l00 . Then, we consider all possible case of o1 and o2 as follows: Let Oa
and Os be the set of operations in la00 and ls00 , respectively.
- If o2 ∈ l100 ∧ o1 ∈ l100 :
- If o1 , o2 ∈ Oa or o1 , o2 ∈ Os : Then l0 contradicts with happen before relation of h.
- If o2 ∈ Oa ∧ o1 ∈ Os : It is not hard to see that put(x, p) <hb o2 . Then, it is impossible to
locate the linearization point of o2 before ret(put, x, p) in elp .
- If o2 ∈ l100 ∧ o1 = put(x, p):
- If o2 ∈ Oa : This is impossible, since in elp , the linearization point of o1 is before ret(put, x, p).
- If o2 ∈ Os : This is impossible, since o2 = put(_, p), and l is consistent with happen before
relation of h.
- If o2 ∈ l100 ∧ o1 ∈ l200 :
- If o2 ∈ Oa : This is impossible, since in elp , the linearization point of operation in la00 is before
the linearization point of operations in l200 .
- If o2 ∈ Os : Since no put(_, p) happens before put(x, p) in h, call(o2 ) is before ret(put, x, p).
Since o1 <hb o2 , we can see that ret(o1 ) is before call(o2 ), and then ret(o1 ) is before
ret(put, x, p). Then the linearization point of o1 can only be before ret(put, x, p), and o1 ∈ la00 ,
which contradicts that o1 ∈ l200 .
- If o2 = put(x, p) ∧ o1 ∈ l200 : Then since the linearization point of o1 can only be before
ret(put, x, p), we can see that o1 ∈ la00 , which contradicts that o1 ∈ l200 .
- If o2 ∈ l200 ∧ o1 ∈ l200 : Then l0 contradicts with happen before relation of h.
Therefore, we know that G is acyclic, and then we know that e v l00 .
It remains to prove that l00 ∈ SeqPQ. la00 · ls00 · l200 can be obtained from l0 as follows: Execute until reaching some time point t, then first execute all Ox operations after t, and then execute
remanning operations. By Lemma 21, we can see that l100 · l200 = la00 · ls00 · l200 ∈ SeqPQ. Since
UnmatchedMaxPriority-Seq(l, x) holds, it is easy to see that l00 = l100 · put(x, p) · l200 ∈ SeqPQ.
Therefore, we prove that e v l00 ∈ SeqPQ. This completes the proof of this lemma.
J
J
I Lemma 26. For each data-differentiated execution e where EmptyRemove-Conc(e, x) for some
o = rm(empty), then e \ o v SeqPQ ⇒ e v SeqPQ.

XX:28

Checking Linearizability of Concurrent Priority Queues

Proof. By assumption we know that there exists l, such that e v l and EmptyRemove-Seq(l, o)
holds. Then l = u · o · v for some u and v. Let e0 = e \ o. By assumption there exists sequence l0 ,
such that e0 v l0 ∈ SeqPQ.
0
Let EL be the set of operations in u and ER be the set of operations in v. Let lL
= l0 |EL and
0
0
00
0
0
lR = l |ER . Let sequence l = lL · o · LR . Since priority queue is closed under projection (Lemma
0
3) and all the put operations and rm in u are matched, we know that lL
∈ SeqPQ and the the priority
0
0
0
queue is empty after executing lL . Then we know that lL · rm(empty) ∈ SeqPQ. Since lR
is obtained
0
0
from l by discarding pairs of matched put and rm operations, it is easy to see that LR ∈ SeqPQ,
0
and then we know that l00 = lL
· o · L0R ∈ SeqPQ.
It remains to prove that h v l00 . To prove h v l00 , we define graph G as in Lemma 24. Assume
that there is a cycle in G, then there must exists o1 and o2 , such that o1 happens-before o2 in h, but
the corresponding operations are in the opposite order in l00 . Then, we consider all possible case of
o1 and o2 as follows:
0
0
- o1 , o2 ∈ lL
, or o1 , o2 ∈ lR
: Then l0 contradicts with happen before relation of h.
0
0
0
0
- If o1 = o ∧ o2 ∈ lL , or o1 ∈ lR
∧ o2 ∈ lL
, or o1 ∈ lR
∧ o2 = o, then l contradicts with happen
before relation of h.

Therefore, we know that G is acyclic, and then we know that h v SeqPQ.

J

J

The following lemma states that SeqPQ is step-by-step linearizability, which is a direct consequence of Lemma 24, Lemma 25 and Lemma 26.
I Lemma 27. SeqPQ is step-by-step linearizability.
Proof. This is a direct consequence of Lemma 24, Lemma 25 and Lemma 26.

C.4

J

J

Proof of Lemma 6

Lemma 6: Check-PQ-Conc(e) = true iff e v SeqPQ, for every data-differentiated execution e.
Proof. To prove the if direction, given a data-differentiated e v l ∈ SeqPQ. Then we being a loop
as follows,
- If Has-EmptyRemoves(e) holds, then l = u · o · v for some o = rm(empty). It is not hard to see
that EmptyRemove-Seq(l, o) holds. Let e0 be the projection of e into operations of u · v. It is
easy to see that e0 v u · v and then e0 v SeqPQ. Then we start the next round and choose e0 to
be the “e in the next round”.
- If Has-UnmatchedMaxPriority(e) holds, then there exists a maximal priority p in e, such that
p has unmatched put. Let l = u · put(x, p) · v, where in v there is no put with priority p. It is
not hard to see that UnmatchedMaxPriority-Seq(l, x) holds. Let e0 be the projection of e into
operations of u · v. It is easy to see that e0 v u · v and then e0 v SeqPQ. Then we start the next
round and choose e0 to be the “e in the next round”.
- If Has-MatchedMaxPriority(e) holds, then there exists a maximal priority p in e, such that p has
only matched put. Let l = u · put(x, p) · v · rm(x) · w, where in v · w there is no put with priority
p. It is not hard to see that MatchedMaxPriority-Seq(l, x) holds. Let e0 be the projection of e
into operations of u · v · w. It is easy to see that e0 v u · v · w and then e0 v SeqPQ. Then we
start the next round and choose e0 to be the “e in the next round”.
The loop terminates when at some round e = . This process ensures that Check-PQ-Conc(e) =
true.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

To prove the only if direction, given a data-differentiated execution e and assume that Check-PQΓ
Γ1
→ em with e0 = e and em = . Assume that
e1 . . . −−m
Conc(e) = true. Then we have e −→
for each i, we found Γ-Seq(ei , αi ) holds for some αi . From Γ-Seq(em-1 , αm-1 ) holds and em =
em-1 \ αm-1 v SeqPQ, by Lemma 27, we can see that em-1 v SeqPQ. Similarly, we can prove that
em-2 , . . . , e0 = e v SeqPQ.
J
J

C.5

Proof of Lemma 7

Lemma 7: Given a data-differentiated execution e, e v SeqPQ if and only if for each e0 ∈ proj(e),
Check-PQ-Conc-NonRec(e0 ) returns true.
Proof. To prove the only if direction, assume that e v l ∈ SeqPQ. Given e0 = e|D and l0 = l|D ,
it is easy to see that e0 v l0 , and by Lemma 3, we can see that l0 ∈ SeqPQ. Then it is obvious that
Check-PQ-Conc-NonRec(e0 ) returns true.
To prove the if direction, assume that for each e0 ∈ proj(e), Check-PQ-Conc-NonRec(e0 ) returns
true. Then similarly as by Lemma 6, we can implies that Check-PQ-Conc(e) = true, and then by
Lemma 6, we know that e v SeqPQ.
J
J

D

Proofs and Definitions in Section 4

To facilitate our proof, we consider two cases of MatchedMaxPriority-Seq(e, x) depending on
whether e contains exactly one value with priority p or at least two values. We denote by MatchedMax−
Priority> (e, x) the strengthening of MatchedMaxPriority(e, x) with the condition that all the values
other than x have a priority strictly smaller than p, and by MatchedMaxPriority= (e, x) the strengthening of the same formula with the negation of this condition.
Similarly, we consider two cases of UnmatchedMaxPriority-Seq(e, x) depending on whether
e some values of priority p has matched put. We denote by UnmatchedMaxPriority> (e, x) the
strengthening of UnmatchedMaxPriority(e, x) with the condition that non value of priority p has
matched put, and by UnmatchedMaxPriority= (e, x) the strengthening of the same formula with the
negation of this condition.

D.1

Lemma and Register Automata For FIFO of Single-Priority
Executions

Before we go to investigate Γ-linearizable, we can use the result in [5] to simplify our work. [5]
states that checking linearizability w.r.t queue can be reduced into checking emptiness of intersection
between I and a set of automata. Given a data-differentiated execution e, let e|i be an execution
generated from e by erasing call and return actions of values that does not use priority i (does not
influence rm(empty)). We call a extended priority queue execution with only one priority a singlepriority execution. Let transToQueue(e) be an execution generated from e by transforming put and
rm into enq and deq, respectively, and then discarding priorities. We can see that for each e ∈ SeqPQ
and each priority i, transToQueue(e|i ) satisfy FIFO (first in first out) property.
Given an execution of queue, we say that it is differentiated, if each value is enqueued at most
once. [5] states that, given a differentiated queue execution e without deq(empty), e is not linearizable with respect to queue, if one of the following cases holds for some a, b: (1) deq(b) <hb enq(b),
(2) there are no enq(b) and at least one deq(b), (3) there are one enq(b) and more than one deq(b),
and (4) enq(a) <hb enq(b), and deq(b) <hb deq(a), or deq(a) does not exists. For each such case,
we can construct a register automata for extended priority queue.

XX:29

XX:30

Checking Linearizability of Concurrent Priority Queues

We generate register automata A1SinPri for the first case, and it is shown in Figure 8. Here C1 =
{call(put, a, true), ret(put, a, true), call(rm, a), ret(rm, a), call(rm, b), call(rm, empty), ret(rm, empty)},
C2 = C1 ∪ {ret(rm, b)}, C3 = C2 ∪ {ret(put, b, true)}.
C1

qinit

C2
ret(rm, b)

q2

C3
call(put, b, rue)

q3

Figure 8 Automaton A1SinPri

We generate register automata A2SinPri for the second case, and it is shown in Figure 9. Here C1 =
{call(put, a, true), ret(put, a, true), call(rm, a), ret(rm, a), call(rm, empty), ret(rm, empty)}, C2 = C1 ∪
{call(rm, b) + ret(rm, b)}.
C1

qinit

C2
call(rm, b)

q2

Figure 9 Automaton A2SinPri

We generate register automata A3SinPri for the third case, and it is shown in Figure 10. Here C1 =
{call(put, a, true), ret(put, a, true), call(rm, a), ret(rm, a), call(rm, empty), ret(rm, empty)}, C2 = C1 ∪
{ret(put, b, true)}, C3 = C2 ∪ {ret(rm, b)}, C4 = C3 ∪ {call(rm, b)}, C5 = C1 ∪ {ret(rm, b)},
C6 = C5 ∪ {call(rm, b)}.
C1

qinit

C2
call(put, b, true)

q2

C3
call(rm, b)

C5

call(rm, b)

q4

C3 call(rm, b)

call(rm, b)
q5

q3

C4

call(put, b, true)

q6
call(put, b, true)
C6

call(rm, b)
q7

Figure 10 Automaton A3SinPri

We generate register automata A4SinPri for the forth case, and it is shown in Figure 11. Here
C1 = C ∪ {call(rm, b)}, and C2 = C ∪ {ret(put, b, = r), call(rm, a), ret(rm, a)}, where C =
{call(put, d, true), ret(put, d, true), call(rm, d), ret(rm, d), call(rm, empty), ret(rm, empty)}.
Let AsinPri be the union of A1SinPri , A2SinPri , A3SinPri , A4SinPri . Let us prove Lemma 28.
I Lemma 28. Given a data-independent implementations I of extended priority queue, I ∩
AsinPri 6= ∅, if and only if there exists e ∈ I6= , e0 ∈ proj(e), such that e0 is single-priority without
rm(empty), and transToQueue(e0 ) does not linearizable to queue.

Ahmed Bouajjani, Constantin Enea, and Chao Wang
c1

c1

qinit1 r = ∗

q1

c1
call(put, a, = r)

q2

c1
ret(put, a, = r)

q3

call(rm, b)

call(rm, b)

call(rm, b)

c1

c1

c1

q4

call(put, a, = r)

q5

XX:31

ret(put, a)

q6

c2
call(put, b, = r)

q7

c3
ret(rm, b)

q8

Figure 11 Automaton A4SinPri

Proof. [5] states that, given a differentiated queue execution e without deq(empty), e is not linearizable with respect to queue, if one of the following cases holds for some va , vb : (1) deq(vb ) <hb
enq(vb ), (2) there are are no enq(vb ) and at least one deq(vb ), (3) there are are one enq(vb ) and
more than one deq(vb ), and (4) enq(va ) <hb enq(vb ), and deq(vb ) <hb deq(va ), or deq(va ) does not
exists.
Let us prove the only if direction. Assume that there exists execution e0 ∈ I and e0 is accepted
by A1SinPri , A2SinPri , A3SinPri or A4SinPri . By data-independence, we can see that there exists a datadifferentiated e ∈ I and renaming function, such that e0 = r(e). Let e0 be obtained from e by first
removing rm(empty), and then,
- If e0 is accepted by A1SinPri , A2SinPri or A3SinPri : Then remove all values that are not renamed into
b by r.
- If e0 is accepted by A4SinPri : Then remove all values that are not renamed into a or b by r.
It is obvious that e0 ∈ proj(e). It is easy to see that transToQueue(e0 ) satisfies one of above
conditions, and then transToQueue(e0 ) is not linearizable w.r.t queue.
Let us prove the if direction. Assume that exists e ∈ I6= , e0 ∈ proj(e), such that e0 is singlepriority without rm(empty), and transToQueue(e0 ) does not linearizable to queue. Then we construct
a renaming function r as follows:
- If this is because case 1, case 2 or case 3: r maps vb into b and maps all other values into a.
- If this is because case 4: r maps va and vb into a and b, respectively, and maps all other values
into d.
Then it is not hard to see that r(e) ∈ I and it is accepted by A1SinPri , A2SinPri , A3SinPri or A4SinPri .
This completes the proof of this lemma.
J
J

D.2

Proof of Lemma 10

The following lemma states that, from linearization of sub-histories, we can merge them and obtain
a linearization (regardless of whether it belongs to sequential specification) of the whole history.
I Lemma 29. Given an execution e, operation sets S1 , S2 and sequences l1 and l2 . Let e1 = e|S1
and e2 = e|S2 . Assume that e1 v l1 , e2 v l2 , and S1 ∪ S2 contains all operations of e. Then, there
exists a sequence l, such that e v l, l|S1 = l1 and l|S2 = l2 .
Proof. Given an execution e and a operation o ∈ S2 , let MB(o) = {o0 |o0 ∈ S1 and o0 happens
before o in h}, let SBI(o) = min{i|l1 [0, i] contains all elements of MB(o)}.
Let l = s1 · l2 [1] · . . . · l2 [n] · sn+1 be generated as follows, where n = |l2 |:

XX:32

Checking Linearizability of Concurrent Priority Queues

- s1 = l1 [0, SBI(l2 [1])],
- If s1 · l2 [1] · . . . · l2 [i] already contains l1 (SBI(l2 [i+1])), then si+1 = . Otherwise, si+1 is a
subsequence of l1 , which starts from the next of last elements of s1 · l2 [1] · . . . · l2 [i] in l1 and
ends in l1 (SBI(l2 [i+1])).
It is obvious that l|S1 = l1 and l|S2 = l2 , and it remains to prove that e v l. We prove this by
contradiction. Assume that e 6v l. Then there must be two operations o1 , o2 of e, such that o1 <hb o2
in e but o2 before 01 in l. Since l|S1 = l1 , l|S2 = l2 , and h1 v l1 , h2 v l2 , it is easy to see that it is
impossible that o1 , o2 ∈ S1 or o1 , o2 ∈ S2 . There are only two possibilities:
- o1 ∈ S1 ∧ o2 ∈ S2 . Then we can see that o2 = l2 [i] and o1 ∈ sj for some i < j. Since
o1 <hb o2 , we know that o1 ∈ SBI(o2 ). By the construction of l, we know that o1 must be in sk
for some k ≤ i, contradicts that o1 ∈ sj with i < j.
- o1 ∈ S2 ∧ o2 ∈ S1 . Then we can see that o2 ∈ si and o1 = l2 [j] for some i ≤ j. It is easy to see
that this leads to contradiction when i = j. For the case of i 6= j, we need to satisfy the following
requirements: (1) o1 (l2 [j]) does not happen before l2 [i], (2) l2 [i] does not happen before o2 , (3)
o2 is either overlap or happens before o0 ∈ MB(l2 [i]), and (4) o0 <hb l2 [i]. By enumeration we
can see that it is impossible that above four conditions be satisfied while o1 <hb o2 .
This completes the proof of this lemma.

J

J

With Lemma 29, we can now prove Lemma 10.

Lemma 10: Let Γ ∈ {UnmatchedMaxPriority, MatchedMaxPriority} and e a data-differentiated
execution. Then, e is Γ-linearizable iff e|p is Γ-linearizable for some maximal priority p in e.
Proof. We deal with the case of Γ = MatchedMaxPriority> , and other cases can be similarly dealt
with.
To prove the only if direction, assume that e v l, MatchedMaxPriority-Seq(l, x) holds and p is
the priority of x. We can see that e v u · put(x, p) · v · rm(x) · w. Let u0 , v 0 and w0 be obtained from
u, v and w by erasing all values with priority incomparable with p, respectively. Since the predicates
in MatchedMaxPriority-Seq(l, x) does not restrict the values of priorities incomparable with p, is
not hard to see that e v l0 and MatchedMaxPriority-Seq(l0 , x) holds, where l0 = u0 · put(x, pri) · v 0 ·
rm(x) · w0 .
To prove the if direction, given e0 = e|≺p . By assumption, e0 v l, MatchedMaxPriority-Seq(l, x)
holds and p is the priority of x, and then we can see that e0 v l1 = u·put(x, p)·v·rm(x)·w. Let Oc be
the set of operations in e that have priorities comparable with p, and Let Oi be the set of operations in
e that have priorities incomparable with p. It is obvious that l1 is the linearization of e|Oc . By Lemma
29, there exists sequence l, such that e v l, and l|Oc = l1 . Then l = u0 · put(x, p) · v 0 · rm(x) · w0 ,
where u0 |Oc = u, v 0 |Oc = v and w0 |Oc = w. Since p is one of maximal priorities in e, and the
predicates in MatchedMaxPriority-Seq(l, x) does not restrict the values with priority Oi , it is easy
to see that MatchedMaxPriority-Seq(l, x) holds.
J
J
Therefore, from now on, it is safe to consider only the data-differentiated sequences with only
one maximal priority.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

D.3

Proofs, Definitions and Register Automata in Subsection 4.1.1

Let us introduce UVSet(e, x), which intuitively contains all pairs of operations that should be putted
before rm(x) when construction linearization of x according to MatchedMaxPriority. Let UVSet1 (e,
x) = o| either o < hbput(x, _) or rm(x), or there exists o0 with the same value of o, such that
o0 < hbput(x) or rm(x)}. For each i > 1, let UVSeti+1 (e, x) = o| o ∈
/ UVSetk for each k ≤ i, and
0
either o happens before some operation o ∈ UVSeti (e, x), or there exists o00 with the same value of
o, and o00 happens before some operation o0 ∈ UVSeti (e, x)}. Let UVSet(e, x) = UVSet1 (e, x)∪. . ..
Note that it is possible that UVSeti (e, x) ∩ UVSetj (e, x) = ∅ for any i 6= j.
The following lemma states that UVSet(e, x) contains only matched put and rm.
I Lemma 30. Given a data-differentiated execution e where Has-MatchedMaxPriority(e) holds,
let p be its maximal priority and put(x, p), rm(x) are only operations of priority p in e. Let G be the
graph representing the left-right constraint of x. Assume that G has no cycle going through x. Then,
UVSet(e, x) contains only matched put and rm.
Proof. We prove this lemma by contradiction. Assume that there exists a value, such that UVSet(e, x)
contains only its put and does not contain its rm. Then we can see that there exists d1 , . . . , dj . Intuitively, d1 , . . . , dj are elements in UVSet1 (e, x), . . . , UVSeti (e, x), respectively. UVSet(e, x) contains
put(dj , _) and does not contain rm(dj ). And each di is the reason of di+1 ∈ UVSeti+1 (e, x). Formally, we require that
- For each 1 ≤ i ≤ j, operations of di belongs to UVSeti (e, x).
- For each i 6= j, put(di , _), rm(di ) ∈ UVSeti (e, x). put(dj , _) ∈ UVSetj (e, x), and e does not
contain rm(dj ).
- An operation of d1 happens before an operations of x. For each 1 < i ≤ j, an operation of di
happens an operation of di-1 .
- For each k and ind, if k > ind+1, then no operation of dk happens before operation of dind .
According to the definition of UVSet(e, x), it is easy to see that such d1 , . . . , dj exists. Let us
prove the following fact:
fact1 : Given 1 ≤ i < j, it can not be the case that put(di , _) and rm(di ) overlap.
Proof of fact1 : We prove fact1 by contradiction. Assume that for some i 6= j, put(di , _) and
rm(di ) overlap. Since put(di , _), rm(di ) ∈ UVSeti (h, x), we know that an operation oi of di happens before operation oi-1 of di-1 . Moreover, since put(di , _) and rm(di ) overlap, it is not hard to
see that the call action of put(di , _) and the call action of rm(di ) is before the call action of oi-1 .
Since operations of di+1 is in UVSeti+1 (e, x), we know that an operation o0i+1 of di+1 happens before
operation o0i of di . Then, it is not hard to see that o0i+1 also happens before oi-1 , which contradicts
that for each k > ind+1, no operation of dk happens before operation of dind .
We already know that an operation of d1 happens before an operation of x. By fact1 , we can
ensure that put(d1 , _) happens before an operation of x, and then d1 → x in G. For each 1 < i ≤ j,
we know that an operation oi of di happens before an operation oi-1 of di-1 . By fact1 , we can ensure
that oi = put(di , _) and oi-1 = rm(di-1 ), and then di → di-1 in G. Since h contains put(dj , _)
and does not contain rm(dj ), we know that x → dj in G. Then G has a cycle going through x,
contradicts that G has no cycle going through x.
J
J
The following lemma states that UVSet(e, x) does not happen before rm(x) when the left-right
constraint has no cycle going through x.
I Lemma 31. Given a data-differentiated execution e where Has-MatchedMaxPriority(e) holds,
let p be its maximal priority and put(x, p), rm(x) are only operations of priority p in e. Let G be the

XX:33

XX:34

Checking Linearizability of Concurrent Priority Queues

graph representing the left-right constraint of x. Assume that G has no cycle going through x. Then,
rm(x) does not happen before any operation in UVSet(e, x).
Proof. We prove this lemma by induction, and prove that rm(x) does not happen before any operation in UVSet1 (e, x), in UVSet2 (e, x), . . .. Note that, by Lemma 30, UVSet(e, x) contains only
matched put and rm, and it is easy to see that for each i, UVSeti (e, x) contains only matched put and
rm.
(1) Let us prove that rm(x) does not happen before any operation in UVSet1 (e, x) by contradiction.
Assume that rm(x) <hb o, where o ∈ UVSet1 (e, x) is an operation of value d.
We use a triple (t1 , t2 , t3 ) to represent related information. t1 , t2 , t3 are chosen from {put, rm}.
t1 represents whether o is a put operation or a rm operation. t2 and t3 is used for the reason of
o ∈ UVSet1 (e, x): o ∈ UVSet1 (e, x), since an operation (of kind t2 ) of d happens before an operation
(of kind t3 ) of x. Let us consider all the possible cases of (t1 , t2 , t3 ):
- (put, put, put): Then rm(x) <hb put(d, _) <hb put(x, p), contradicts that rm(x) does not happen
before put(x, p).
- (put, put, rm): Then rm(x) <hb put(d, _) <hb rm(x), contradicts that rm(x) does not happen
before rm(x).
- (put, rm, put): Then (rm(x) <hb put(d, _)) ∧ (rm(d) <hb put(x, p)). By interval order, we know
that (rm(x) <hb put(x, p)) ∨ (rm(d) <hb put(d, _)), which is impossible.
- (put, rm, rm): Then (rm(x) <hb put(d, _)) ∧ (rm(d) <hb rm(x)). We can see that rm(d) <hb
rm(x) <hb put(d, _), which contradicts that rm(d) does not happen before put(d, _).
- (rm, put, put): Then (rm(x) <hb rm(d)) ∧ (put(d, _) <hb put(x, p)). We can see that x and d
has circle in G, contradicts that G has no cycle going through x.
- (rm, put, rm): Then (rm(x) <hb rm(d)) ∧ (put(d, _) <hb rm(x)). We can see that x and d has
circle in G, contradicts that G has no cycle going through x.
- (rm, rm, put): Then rm(x) <hb rm(d) <hb put(x, p), contradicts that rm(x) does not happen
before put(x, p).
- (rm, rm, rm): Then rm(x) <hb rm(d) <hb rm(x), contradicts that rm(x) does not happen before
rm(x).
This completes the proof for UVSet1 (e, x).
(2) Assume we already prove that for some j ≥ 1, rm(x) does not happen before any operation in
UVSet1 (e, x) ∪ . . . ∪ UVSetj (e, x). Let us prove that rm(x) does not happen before any operation
in UVSetj+1 (e, x) by contradiction. Assume that rm(x) <hb o, where o ∈ UVSetj+1 (e, x) is an
operation of value dj+1 . We use a triple (t1 , t2 , t3 ) to represent related information. t1 , t2 , t3 are
chosen from {put, rm}. t1 represents whether o is a put operation or a rm operation. t2 and t3 is
used for the reason of o ∈ UVSetj+1 (e, x): o ∈ UVSetj+1 (e, x), since an operation (of kind t2 ) of
dj+1 happens before an operation (of kind t3 ) of dj , where put(dj , _), rm(dj ) ∈ UVSetj (e, x). Let
us consider all the possible cases of (t1 , t2 , t3 ):
- (put, put, put): Then rm(x) <hb put(dj+1 , _) <hb put(dj , _). We can see that (rm(x) <hb
put(dj , _)) ∧ (put(dj , _) ∈ UVSetj (e, x)), which contradicts that rm(x) does not happen before
any operation in UVSet1 (e, x) ∪ . . . ∪ UVSetj (e, x).
- (put, put, rm): Then rm(x) <hb put(dj+1 , _) <hb rm(dj , _). We can see that (rm(x) <hb
rm(dj , _)) ∧ (rm(dj ) ∈ UVSetj (e, x)), which contradicts that rm(x) does not happen before
any operation in UVSet1 (e, x) ∪ . . . ∪ UVSetj (e, x).
- (put, rm, put): Then (rm(x) <hb put(dj+1 , _)) ∧ (rm(dj+1 ) <hb put(dj , _)). By interval order,
we know that (rm(x) <hb put(dj , _)) ∨ (rm(dj+1 ) <hb put(dj+1 , _)), which is impossible.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

XX:35

- (put, rm, rm): Then (rm(x) <hb put(dj+1 , _)) ∧ (rm(dj+1 ) <hb rm(dj )). By interval order, we
know that (rm(x) <hb rm(dj )) ∨ (rm(dj+1 ) <hb put(dj+1 , _)), which is impossible.
- (rm, put, put): Then (rm(x) <hb rm(dj+1 )) ∧ (put(dj+1 , _) <hb put(dj , _)). Let us consider the
reason of put(dj , _), rm(dj ) ∈ UVSetj (e, x):
- If (j > 1)∧(put(dj , _) <hb o00 ), where o00 is an operation of value dj-1 and put(dj-1 , _), rm(dj-1 ) ∈
UVSetj-1 (e, x): Then since (put(dj+1 , _) <hb put(dj , _)) ∧ (put(dj , _) <hb o00 ), we can see
that put(dj+1 , _) <hb o00 , and then operations of dj+1 is in UVSetj (e, x), contradicts that operations of dj+1 is in UVSetj+1 (e, x).
- If (j = 1) ∧ (put(dj , _) <hb o00 ), where o00 is an operation of x: Similar to above case.
- If (j > 1)∧(rm(dj ) <hb o00 ), where o00 is an operation of value dj-1 and put(dj-1 , _), rm(dj-1 ) ∈
UVSetj-1 (e, x): Then since (put(dj+1 , _) <hb put(dj , _)) ∧ (rm(dj ) <hb o00 ), we can see that
(put(dj+1 , _) <hb o00 ) ∨ (rm(dj ) <hb put(dj , _)), which is impossible.
- If (j > 1) ∧ (rm(dj ) <hb o00 ), where o00 is an operation of x: Similar to above case.
- (rm, put, rm): Let Tind be the set of sentences {rm(x) <hb rm(dj+1 ), put(dj+1 , _) <hb rm(dj ), . . . , put(dind+1 , _) <hb
rm(dind )}. Here each di is a value of some operation in UVSeti (e, x). Let us prove that from Tj
we can obtain contradiction by induction:
Base case 1: From T1 we can obtain contradiction.
Let us prove base case 1:
- If put(d1 , _) happens o, and o is an operation of x. Then there is a cycle x → dj+1 → . . . →
d1 → x in G, contradicts that G has no cycle going through x.
- If rm(d1 ) happens before o, and o is an operation of x. Then since put(d2 , _) <hb rm(d1 )
and rm(d1 ) <hb o, we can see that put(d2 , _) <hb o, and then put(d2 , _) ∈ UVSet1 (e, x),
contradicts that put(d2 , _) ∈ UVSet2 (e, x).
Base case 2: From T2 we can obtain contradiction.
Let us prove base case 2: If rm(d2 ) <hb o, and o is an operation of d1 , then since (put(d3 , _) <hb
rm(d2 )) ∧ (rm(d2 ) <hb o), we know that put(d3 , _) <hb o. This implies that put(d3 , _) ∈
UVSet2 (e, x), contradicts that rm(d3 , _) ∈ UVSet3 (e, x). Therefore, it is only possible that
put(d2 , _) happens before an operation of d1 .
- If put(d2 , _) <hb put(d1 , _) and put(d1 , _) happens before operations of x, then we know that
put(d2 , _) happens before operation of x, which is impossible.
- If put(d2 , _) <hb put(d1 , _) and rm(d1 ) happens before operations of x, then by interval
order, we know that put(d2 , _) happens before operation of x, or rm(d1 ) <hb put(d1 , _),
which is impossible.
- If put(d2 , _) <hb rm(d1 ) and put(d1 , _) happens before operations of x, then x → dj+1 →
. . . → d1 → x in G, contradicts that G has no cycle going through x.
- If put(d2 , _) <hb rm(d1 ) and rm(d1 ) happens before operations of x, then we know that
put(d2 , _) happens before operation of x, which is impossible.
induction step: Given ind ≥ 3, if from Tind-1 we can obtain contradiction, then from Tind we can
also contain contradiction.
Prove of the induction step: Similarly as base case 2, we can prove that it is only possible that
put(dind , _) happens before operations of dind-1 .
- If put(dind , _) <hb put(dind-1 , _) and put(dind-1 , _) happens before operations of dind-2 , then we
know that put(dind ) happens before operation of dind-2 , which is impossible.

XX:36

Checking Linearizability of Concurrent Priority Queues

- If put(dind , _) <hb put(dind-1 , _) and rm(dind-1 ) happens before operations of dind-2 , then by
interval order, we know that put(dind , _) happens before operation of dind-2 , or rm(dind-1 ) <hb
put(dind-1 , _), which is impossible.
- If put(dind , _) <hb rm(dind-1 ), then we obtain Tind-1 , which already contain contradiction.
By base case 1, base case 2 and the induction step, it is easy to see that for each i, Ti contains
contradiction. Therefore, Tj , the case of (rm, put, rm), contains contradiction.
- (rm, rm, put): Then (rm(x) <hb rm(dj+1 )) ∧ (rm(dj+1 ) <hb put(dj , _)). We can see that
(rm(x) <hb put(dj , _)) ∧ (put(dj , _) ∈ UVSetj (e, x)), which contradicts that rm(x) does not
happen before any operation in UVSet1 (e, x) ∪ . . . ∪ UVSetj (e, x).
- (rm, rm, rm): Then (rm(x) <hb rm(dj+1 ))∧(rm(dj+1 ) <hb rm(dj )). We can see that (rm(x) <hb
rm(dj )) ∧ (rm(dj ) ∈ UVSetj (e, x)), which contradicts that rm(x) does not happen before any
operation in UVSet1 (e, x) ∪ . . . ∪ UVSetj (e, x).
This completes the proof for UVSetj+1 (e, x). Therefore, rm(x) does not happen before any
operation in UVSet(e, x) = UVSet1 (e, x) ∪ UVSet2 (e, x) ∪ . . ..
J
J
With Lemma 30 and Lemma 31, we can now prove Lemma 13, which give the equivalent characterization of non MatchedMaxPriority-linearizable executions.
Lemma 13: Given a data-differentiated execution e where Has-MatchedMaxPriority(e) holds, let
p be its maximal priority and put(x, p), rm(x) are only operations of priority p in e. Let G be the
graph representing the left-right constraint of x. e is MatchedMaxPriority-linearizable, if and only
if G has no cycle going through x.
Proof. To prove the only if direction, assume that e v l and MatchedMaxPriority-Seq(l, x) holds.
Then l = u · put(x, p) · v · rm(x) · w, and let U , V and W be the set of operations of u, v and w,
respectively. Assume by contradiction that, there is a cycle d1 → d2 → . . . → dm → x → d1 in G.
It is obvious that the priority of each di is smaller than p. Then our proof proceeds as follows:
According to the definition of left-right constraint, there are two possibilities. The first possibility
is that, rm(x) happens before rm(d1 ). It is obvious that rm(d1 ) ∈ W , and then since U ∪ V contains
matched put and rm, we can see that put(d1 ), rm(d1 ) ∈ W . Then,
- Since d1 → d2 , by definition of G, we know that put(d1 ) happens before rm(d2 ). Since
put(d1 ) ∈ W and U ∪ V contains matched put and rm, we know that put(d2 ), rm(d2 ) ∈ W .
Similarly, for each 1 ≤ i ≤ m, we know that put(di ), rm(di ) ∈ W .
- Since dm → x,
- if put(dm ) happens before put(x), then we can see that put(dm ) ∈ U , which contradicts that
put(dm ) ∈ W .
- if put(dm ) happens before rm(x), then we can see that put(dm ) ∈ U ∪ V , which contradicts
that put(dm ) ∈ W .
The second possibility is that, e contains one put(d1 , _) and no rm(d1 ). Note that for each j > 1,
e contains put(dj , _) and rm(dj ). Since dm → x, is is obvious that put(dm ) ∈ U ∪ V . Since U ∪ V
contains matched put and rm, we know that put(dm ), rm(dm ) ∈ U ∪ V . Then, since dm-1 → dm ,
by definition of G, we know that put(dm-1 ) happens before rm(dm ). Since rm(dm ) ∈ U ∪ V and
U ∪ V contains matched put and rm, we know that put(dm-1 ), rm(dm-1 ) ∈ U ∪ V . Similarly, for each
1 < i ≤ m, we know that put(di ), rm(di ) ∈ U ∪ V , and also put(d1 ) ∈ U ∪ V . However, there is
one put(d1 , _) and no rm(d1 ) in e, contradicts that U ∪ V contains matched put and rm.
This completes the proof of the only if direction.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

XX:37

To prove the if direction, assume that G has no cycle going through x. Let Eu be the set of
operations that happen before put(x) in e. It is easy to see that Eu ⊆ UVSet(e, x). Let Ev =
UVSet(e, x) \ Eu . Let Ee be the set of operations of e, and let Ew = Ee \ UVSet(e, x).
By Lemma 30, we can see that Eu ∪ Ev contains matched put and rm operations. It remains
to prove that for Eu , {put(x, p)}, Ev , {rm(x)}, Ew , no elements of the latter set happens before
elements of the former set. We prove this by showing that all the following cases are impossible:
- Case 1: Some operation ow ∈ Ew happens before rm(x). Then we know that ow ∈ UVSet(e, x) =
Eu ∪ Ev , which contradicts that ow ∈ Ew .
- Case 2: Some operation ow ∈ Ew happens before some operation ouv ∈ Eu ∪ Ev . Then we
know that ow ∈ UVSet(e, x) = Eu ∪ Ev , which contradicts that ow ∈ Ew .
- Case 3: Some operation ow ∈ Ew happens before put(x). Then we know that ow ∈ UVSet(e, x) =
Eu ∪ Ev , which contradicts that ow ∈ Ew .
- Case 4: rm(x) happens before some ouv ∈ UVSet(e, x) = Eu ∪ Ev . By Lemma 31 we know that
this is impossible.
- Case 5: rm(x) happens before put(x). This contradicts that each single-priority projection satisfy
the FIFO property.
- Case 6: Some operation ov ∈ Ev happens before put(x). Then we know that ov ∈ Eu , which
contradicts that ov ∈ Ev .
- Case 7: Some operation ov ∈ Ev happens before some operation ou ∈ Eu . Then we know that
ov ∈ Eu , which contradicts that ov ∈ Ev .
- Case 8: put(x) happens before some operation ou ∈ Eu . This is impossible.
This completes the proof of the if direction.
J

J

Let us begin to represent register automata that is used for capture the existence of a datadifferentiated execution e, let p be a maximal priority of e, and e0 be the projection of e into values
with priorities comparable with p. We also require that Has-MatchedMaxPriority(e0 ) holds and
there exists a cycle going through the value with maximal priority in e0 . By data-independence, we
can obtain er from e by renaming function, which maps such value to be b, maps values that cover it
to be a, and maps other values into d. There are four possible enumeration of call and return actions
of put(b, p) and rm(b). For each of them, we generate a register automaton.
For the case when er |b = call(put, b, p)·ret(put, b, p)·call(rm, b)·ret(rm, b), we generate register
automaton A1l-lar , as shown in Figure 12. Here C1 = C ∪{ret(rm, a)}, C2 = C ∪{call(put, a, < r)},
C3 = C2 ∪ {ret(rm, a)}, where C = {call(put, >, true), ret(put, >, true), call(rm, >), ret(rm, >),
call(rm, empty), ret(rm, empty). The differentiated branch in A1l-lar comes from the positions of the
first ret(put, a, _).
A1l-lar is used to recognize conditions in Figure 13. Here for simplicity, we only draw operation
of b, and the first ret(put, a, _).
For the case when er |b = call(put, b, p) · call(rm, b) · ret(put, b, p) · ret(rm, b), we generate
register automaton A2l-lar , as shown in Figure 14. Here C1 , C2 , C3 is the same as that in A1l-lar . The
differentiated branch in A2l-lar comes from the positions of the first ret(put, a, _).
A2l-lar is used to recognize conditions in Figure 15. Here for simplicity, we only draw operation
of b, and the first ret(put, a, _).
For the case when er |b = call(rm, b) · call(put, b, p) · ret(put, b, p) · ret(rm, b), we generate
register automaton A3l-lar , as shown in Figure 16. Here C1 , C2 , C3 is the same as that in A1l-lar . The
differentiated branch in A3l-lar comes from the positions of the first ret(put, a, _).

XX:38

Checking Linearizability of Concurrent Priority Queues

C2

q2
C2

C2

qinit r = ∗

C2
ret(put, b, = r)

call(put, b, = r) ret(put, a, < r)

q1

q3

C2
ret(put, a, < r)

cal(rm, b)

C1

q5

ret(rm, b)

C2 cal(rm, b)

C2

q10

q4

C3

ret(put, b, = r)

q11

q7

cal(rm, a)

ret(put, a, < r) cal(rm, a)
C3

C1

q6

q8

C2
ret(put, a, < r)
call(put, b, = r)
q9

Figure 12 Automaton A1l-lar

put(b, p)

rm(b)

put(b, p)

put(a, )

rm(b)

put(b, p)

put(a, )

e1

rm(b)

put(a, )

e1

e1

Figure 13 Conditions recognized by A1l-lar

C2

q2
C2

qinit

r=∗

C2
cal(put, b, = r)

ret(put, a, < r)

cal(rm, b)

q3

q4

ret(put, a, < r)
C2

C3

ret(put, b, = r)

q5

ret(put, a, < r)C

ret(put, b, = r)

Figure 14 Automaton A2l-lar

put(b, p)

rm(b)

rm(b)
put(a, )

e1
Figure 15 Conditions recognized by A2l-lar

e2

3

q10

q8

put(b, p)

ret(rm, b)

cal(rm, a)

q9

put(a, )

C1

C3

ret(put, a, < r) cal(rm, a)

q1
call(put, b, = r)

C3

q6

cal(rm, a)
C1

q7

Ahmed Bouajjani, Constantin Enea, and Chao Wang

C2
qinit r = ∗

C2

C2

q2

call(rm, b) q
3

retl(put, a, < r)

C3
cal(put, b, = r)

q4

C3
ret(put, = r)

q5

C1
ret(rm, b)

q6

C1
cal(rm, a)

q7

call(rm, a)

ret(put, a, < r) call(rm, a)

ret(put, a, < r)
C3

C3

q1
call(rm, b)

XX:39

ret(put, a, < r)

C2

q9

q10
ret(put, = r)

q8

Figure 16 Automaton A3l-lar

put(b, p)

put(b, p)

rm(b)

rm(b)

put(a, )

put(a, )

e1

e2

Figure 17 Conditions recognized by A3l-lar

A3l-lar is used to recognize conditions in Figure 17. Here for simplicity, we only draw operation
of b, and the first ret(put, a, _).
For the case when er |b = call(rm, b) · call(put, b, p) · ret(rm, b) · ret(put, b, p), we generate
register automaton A4l-lar , as shown in Figure 18. Here C1 , C2 , C3 is the same as that in A1l-lar , and
C4 = C1 ∪ {ret(put, b, = r)}. The differentiated branch in A4l-lar comes from the positions of the
first ret(put, a, _).

C2
qinit r = ∗

C2

C2

q2

call(rm, b) q
3

C3
cal(put, b, = r)

q4

C4
ret(rm, b)

q5

C4
cal(rm, a)

q6

retl(put, a, < r)
ret(put, a, < r)
C3

q1
call(rm, b)

C2

cal(rm, a)

ret(put, a, < r)
q8

q7

Figure 18 Automaton A4l-lar

A4l-lar is used to recognize conditions in Figure 19. Here for simplicity, we only draw operation
of b, and the first ret(put, a, _).
Let A1-lar be the union of A1l-lar , A2l-lar , A3l-lar and A4l-lar . The following lemma states that A1-lar is
MatchedMaxPriority> -complete.
I Lemma 32. A1-lar is MatchedMaxPriority> -complete.
Proof. We need to prove that, given a data-independent implementation I. A1-lar ∩ I =
6 ∅ if and

XX:40

Checking Linearizability of Concurrent Priority Queues
put(b, p)
rm(b)
put(a, )

put(b, p)
rm(b)
put(a, )

e1

e2

Figure 19 Conditions recognized by A4l-lar

only if there exists e ∈ I and e0 ∈ proj(e) such that e0 is not MatchedMaxPriority> -linearizable.
By Lemma 10 and Lemma 13, we need to prove the following fact:
fact1 : Given a data-independent implementation I. A1-lar ∩ I =
6 ∅ if and only if there exists e ∈ I
and e0 ∈ proj(e), Has-MatchedMaxPriority(e0 ) holds, x is the value with maximal priority in e0 , e0
has only one maximal priority, and there is a cycle going through x in G, where G is the left-right
constraint of x in e0 .
The only if direction: Let us consider the case of A1l-lar . Assume that e1 ∈ I is accepted by A1l-lar . By
data-independence, there exists data-differentiated execution e ∈ I and renaming function r1 , such
that e1 = r1 (e). Assume that r1 maps d into b and maps f1 , . . . , fm into a. Let e0 be obtained from
e by projection into {d, f1 , . . . , fm }. Assume that the priority of b is p. It is easy to see that e0 has
only one maximal priority, Has-MatchedMaxPriority(e0 ) holds, and there is a cycle going through
d in G, where G is the left-right constraint of e0 . The case of A2l-lar , A3l-lar and A4l-lar can be similarly
proved.
The if direction: Given such e, e0 and x. Let renaming function r maps x into b, maps values cover x
into a, and maps other values into d. By data-independence, r(e) ∈ I. Then depending on the cases
of r(e)|b , we can see that r(e) is accepted by A1l-lar , A2l-lar , A3l-lar or A4l-lar .
J
J

D.4

Proofs, Definitions and Register Automata in Subsection 4.1.2

Let Items(e, p) be the set of values with priority p in execution e. The following lemma states a
method to build the linearization of e w.r.t MatchedMaxPriority= .
I Lemma 33. Given a data-differentiated execution e where Has-MatchedMaxPriority= (e) holds
and p is its maximal priority. If there exists a value x with priority p, such that for each y ∈
Items(e, p), (1) x 6<pb y, and (2) the right-most gap-point of x is after call(put, y, p) and call(rm, y).
Then e is MatchedMaxPriority= -linearizable.
Proof. Let o be the right-most gap-point of x. We locate linearization points of each operation as
follows:
- Locate the linearization point of rm(x) at o,
- If put(x, p) overlaps with rm(x), then locate the linearization point of put(x, p) just before the
linearization point of rm(x). Otherwise, put(x, p) <hb rm(x), and we locate the linearization
point of put(x, p) just before its return action.
- Locate linearization points of operation of each y ∈ Items(e, p) (except for x) just after the call
action of the operation.
- For value z with priority smaller than p. If both call(put, z, _) and call(rm, z) is before o,
then locate the linearization points of put(z, _) and rm(z) just after their call actions. If both
ret(put, z) and ret(rm, z) (if exists) is after o, then locate the linearization points of put(z, _) and

Ahmed Bouajjani, Constantin Enea, and Chao Wang

XX:41

rm(z) just before their return actions. Otherwise, x is in interval of z, which contradicts the
definition of gap-point, and is impossible.
Let l be the sequence of linearization points constructed above. It is obvious that e v l. Since for
each y ∈ Items(e, p), o is after call(put, y, _) and call(rm, x), we can see that rm(x) is after put(y, p)
and rm(y) in l. It is obvious that put(x, p) is before rm(x) in l. Since x does not <pb to y, we can
see that no put(y, p) happens before put(x, p). Then it is easy to see that put(x, p) is after put(y, p)
in l. Since Has-MatchedMaxPriority= (e) holds, all other values in Items(e, p) has matched put and
rm, and it is easy to see that their put and rm (except for that of x) are all before rm(x) in l.
For value z with priority smaller than p, we can see that there are only two possibilities: (1)
put(z, _) and rm(z) are both before rm(x) in l, and (2) put(z, _) and rm(z) (if exists) are after before
rm(x) in l. Therefore, before rm(x) in l, the put and rm of z are matched.
Therefore, it is easy to see that MatchedMaxPriority= -Seq(l, x) holds and e is MatchedMaxPriority= linearizable.
J
J
With Lemma 33, we can prove the following lemma, which states that getting rid of case in
Figure 5 is enough for ensure that MatchedMaxPriority= (e) holds.
Lemma 15: Let e be a data-differentiated execution which contains only one maximal priority p such
that Has-MatchedMaxPriority(e) holds. Then, e is not linearizable w.r.t MatchedMaxPriority= iff
e contains two values x and y of maximal priority p such that y <∗pb x, and the rightmost gap-point
of x is strictly smaller than the index of call(put, y, p) or call(rm, y).
Proof. To prove the if direction, let ex,y be the execution that is obtained from e by erasing all
actions of values that has same priority as x, except for actions of x and y. It is obvious that
Has-MatchedMaxP− riority= (ex,y ) holds. Since y <∗pb x, we can see that x should be chosen as α
in MatchedMaxPriority= .
According to Lemma 13 (Here we temporarily forget the existence of y), the only possible position for locating linearizaton point of rm(x) is at gap-point of x. Otherwise, if the linearizaton point
of rm(x) is chosen at a position that is not a gap-point of x, then there exists unmatched operation
before rm(x) with smaller priority. Since the rightmost gap-point of x is before call(put, y, p) or
call(rm, y), if we locate linearizaton point of rm(x) at gap-point of x, then rm(x) will be before
call(put, y, p) or call(rm, x).
Therefore, for every sequence l = u · put(x, p) · v · rm(x) · w, if ex,y v l, then either u · v
contains some unmatched operations of priority smaller than p, or w contains put(y, p) or rm(y). In
both cases, MatchedMaxPriority= -Seq(l, x) does not hold.
To prove the only if direction, we prove its contrapositive. Assume we already know that for each
x and y has maximal priority in e, if y <∗pb x, then the rightmost gap-point of x is after call(put, y, p)
and call(rm, x). We need to prove that e is MatchedMaxPriority= -linearizable. Recall that we
already assume that each single-priority execution has FIFO property, and value with larger priority
is not covered by values with smaller priority.
Our proof proceed as follows:
- Let ep be the projection of e into operations of priority p. Since each single-priority execution
has FIFO property, there exists sequence lp , such that ep v lp , and when we treat put as enq and
rm as deq, lp belongs to queue.
- Let a1 be the last inserted value of lp .
Step 1: Check whether for each b ∈ Items(e, p), (1) a1 does not <pb to b, and (2) the right-most
gap-point of a is after call(put, b, p) and call(rm, b).

XX:42

Checking Linearizability of Concurrent Priority Queues

It is easy to see that a1 is of priority p, and a1 does not <pb to any b ∈ Items(e, p). If for each
b ∈ Items(e, p), the rightmost gap-point of a1 is after call(put, b, p) and call(rm, b). Then by
Lemma 33, we can obtain that e is MatchedMaxPriority= -linearizable.
- Otherwise, there exists a2 ∈ Items(e, p), such that the rightmost gap-point of a1 is before
call(put, a2 , p) or call(rm, a2 ) in e. We can see that each gap-point of a2 is after the rightmost
gap-point of a1 .By assumption, we know that a2 does not <pb to a1 .
- If for each value b ∈ Items(e, p), a2 does not <pb to b. Then we go to step 1 and treat a2
similarly as a1 .
- Otherwise, there exists a3 with priority p such that a2 <∗pb a3 .
Since lp has FIFO property, it is easy to see that there is no cycle in <pb order. It is safe to
assume that a3 is maximal in the sense of <∗pb . Or we can say, there does not exists a4 , such
that a3 <∗pb a4 .
By assumption,we know that the rightmost gap-point of a3 is after call(put, a2 , p) and call(rm, a2 ).
Therefore, we can see that the rightmost gap-point of a3 is after the rightmost gap-point of
a1 . Then we go to step 1 and treat a3 similarly as a1 .
Let ai be the a1 in the i-th loop of our proof. It is not hard to see that, given i < j, the rightmost
gap-point of aj is after the rightmost gap-point of ai . Therefore, the loop finally stop at some af . af
satisfies the check of Step 1. By Lemma 33, this implies that e is MatchedMaxPriority= -linearizable.
This completes the proof of if direction.
J
J
According to the definition of <∗ob , if a <∗pb b, then there exists a1 , . . . , am , such that a <pb
a1 <pb . . . <pb am <pb b. The following lemma states that, the number of intermediate values ai is
in fact bounded.
Lemma 16: Let e be a data-differentiated execution such that a <pb a1 <pb . . . <pb am <pb b holds
for some set of values a, a1 ,. . .,am , b. Then, one of the following holds:
B
C
- a <A
pb b, a <pb b, or a <pb b,
A
B
B
- a <pb ai <pb b or a <pb ai <A
pb b, for some i.
Proof. Our proof proceed as follows:
A
B
B
C
C
A
A
- (<A
pb · <pb ,<pb · <pb and <pb · <pb ): If c3 <pb c2 <pb c1 , then put(c3 , _) happens before
put(c2 , _), and put(c2 , _) happens before put(c1 , _). Therefore, it is obvious that put(c3 , _) happens before put(c1 , _) and c3 <A
pb c1 .
B
B
Similarly, if c3 <pb c2 <pb c1 , then c3 <B
pb c1 .
C
C
If c3 <C
c
<
c
:
Since
c
<
c
,
ret(rm,
c2 ) is before call(put, c1 , _). Since rm(c2 ) does
2
1
2
1
pb
pb
pb
not happen before put(c2 , _), call(put, c2 , _) is before ret(rm, c2 ). Since c3 <C
pb c2 , ret(rm, c3 ) is
before call(put, c2 , _). Therefore, ret(rm, c3 ) is before call(put, c1 , _), and c3 <C
pb c1 .
A
Therefore, when we meet successive <pb , it is safe to leave only the first and the last elements
C
and ignore intermediate elements. Similar cases hold for <B
pb and <pb .
A
C
- <pb and <pb :
C
A
C
C
- (<A
pb · <pb ): If c3 <pb c2 <pb c1 . Since c2 <pb c1 , ret(rm, c2 ) is before call(put, c1 , _). Since
rm(c2 ) does not happen before put(c2 , _), call(put, c2 , _) is before ret(rm, c2 ). Since c3 <A
pb
c2 , ret(put, c3 , _) is before call(put, c2 , _). Therefore, ret(put, c3 ) is before call(put, c1 , _),
and c3 <A
pb c1 .

Ahmed Bouajjani, Constantin Enea, and Chao Wang

XX:43

A
C
A
A
- (<C
pb · <pb ): If c3 <pb c2 <pb c1 . Since c2 <pb c1 , ret(put, c2 , _) is before call(put, c1 , _). It
is obvious that call(put, c2 , _) is before ret(put, c2 , _). Since c3 <C
pb c2 , ret(rm, c3 ) is before
call(put, c2 , _). Therefore, ret(rm, c3 ) is before call(put, c1 , _), and c3 <C
pb c1 .

C
- <B
pb and <pb :

C
B
C
C
- (<B
pb · <pb ): If c3 <pb c2 <pb c1 . Since c2 <pb c1 , ret(rm, c2 ) is before call(put, c1 , _).
It is obvious that call(rm, c2 ) is before ret(rm, c2 ). Since c3 <B
pb c2 , ret(rm, c3 ) is before
call(rm, c2 ). Therefore, ret(rm, c3 ) is before call(put, c1 , _), and c3 <C
pb c1 .
C
B
C
B
B
- (<pb · <pb ): If c3 <pb c2 <pb c1 . Since c2 <pb c1 , ret(rm, c2 ) is before call(rm, c1 ).
Since rm(c2 ) does not happen before put(c2 , _), call(put, c2 , _) is before ret(rm, c2 ). Since
c3 <C
pb c2 , ret(rm, c3 ) is before call(put, c2 , _). Therefore, ret(rm, c3 ) is before call(rm, c1 ),
and c3 <B
pb c1 .

B
A
A
B
A
- (<A
pb · <pb · <pb ): If c4 <pb c3 <pb c2 <pb c1 :
- If call(rm, c2 ) is before call(put, c1 , _): Since c3 <B
pb c2 , ret(rm, c3 ) is before call(rm, c2 ).
A
C
Then ret(rm, c3 ) is before call(put, c1 , _), and c3 <C
pb c1 . This implies that c4 <pb c3 <pb c1 .
A
C
A
According to the fact for <pb · <pb , we know that c4 <pb c1 .
- If call(rm, c2 ) is after call(put, c1 , _): Since c2 <A
pb c1 , ret(put, c2 , _) is before call(put, c1 , _).
Since c3 <B
c
,
rm(c
)
happens
before
rm(c
),
and then we know that put(c2 , _) can not
2
3
2
pb
happen before put(c3 , _). Since put(c2 , _) does not happen before put(c3 , _), call(put, c3 , _)
is before ret(put, c2 , _). Since c4 <A
pb c3 , ret(put, c4 , _) is before call(put, c3 , _). Therefore,
ret(put, c4 , _) is before call(put, c1 , _), and c4 <A
pb c1 .
B
B
B
A
B
B
- (<pb · <A
·
<
):
If
c
<
c
<
c
<
4
pb
pb
pb 3
pb 2
pb c1 : Since c2 <pb c1 , ret(rm, c2 ) is before
call(rm, c1 ). Since c3 <A
pb c2 , we can see that put(c3 , _) <hb put(c2 , _). Since each singlepriority execution has FIFO property, we know that rm(c2 ) does not happen before rm(c3 ),
and thus, call(rm, c3 ) is before ret(rm, c2 ). Since c4 <B
pb c3 , ret(rm, c4 ) is before call(rm, c3 ).
Therefore, ret(rm, c4 ) is before call(rm, c1 ), and c4 <B
pb c1 .

Based on above results, given a <bpb1 a1 <pb . . . <bpbm am <bpbm+1 b, where each bi is in {A, B, C},
we can merge relations, until we get one of the following facts:
B
C
- a <A
pb b, a <pb b or a <pb b,
B
B
A
- a <A
pb ai <pb b, or a <pb ai <pb b, for some i,

This completes the proof of this lemma.

J

J

There are many enumerations of operations of a, b and a1 that may makes a <∗pb b. The following lemma states that since some of them is not consistent with the requirements of gap-point, the
number of potential enumerations can be further reduced into only five.
I Lemma 34. Given a data-differentiated p-execution e where Has-MatchedMaxPriority= (e)
holds. Let a and b be values with maximal priority p. Assume that a <∗pb b, and the rightmost
gap-point of b is before call(put, a, p) or call(rm, a). Then, there are five possible enumeration of
operations of a, b, a1 (if exists), where a1 is the possible intermediate value for obtain a <∗pb b.
Proof. Let us prove by consider all the possible reasons of a <∗pb b. According to Lemma 16, we
need to consider five reasons: Let o be the right-most gap-point of b.

XX:44

Checking Linearizability of Concurrent Priority Queues

- Reason 1, a <A
pb b:
Since a <A
b,
put(a, p) <hb put(b, p). Since o is after call(put, b, p), and thus, after call(put, a, p),
pb
we can see that o is before call(rm, b).
Since single-priority execution must satisfy the FIFO property, rm(b) 6<hb rm(a), and thus,
call(rm, a) is before ret(rm, b). If call(rm, a) is before call(rm, b), then o is also a gap-point of a
and contradicts our assumption. So we know that call(rm, a) is after call(rm, b). If ret(rm, a) is
before ret(rm, b), since we already assume that there exists gap-point of a, this gap-point is also a
gap-point of b, and is after o, which contradicts that o is the rightmost gap-point of b. Therefore,
ret(rm, a) is after ret(rm, b).
According to above discussion, there are two possible enumeration of operations of a and b, as
shown in Figure 20 and Figure 21. Here we explicitly draw the leftmost gap-point of a as o0 .
Since the position of ret(put, b, _) does not influence the correctness, we can simply ignore it.
- Reason 2, a <B
pb b:
B
Since a <pb b, ret(rm, a) is before call(rm, b). Since o is after call(rm, b), we can see that o is
before call(put, a, p). This implies that ret(rm, a) is before call(put, a, p), and then rm(a) <hb
put(a), which is impossible. Therefore, we can safely ignore this reason.
- Reason 3, a <C
pb b:
Since a <B
b,
ret(rm, a) is before call(put, b, p). Since o is after call(put, b), we can see that o
pb
is before call(put, a, p). This implies that ret(rm, a) is before call(put, a, p), and then rm(a) <hb
put(a), which is impossible. Therefore, we can safely ignore this reason.
B
- Reason 4, a <A
pb a1 <pb b:
Since a1 <B
pb b, rm(a1 ) <hb rm(b), and ret(rm, a1 ) is before call(rm, b). Since rm(a1 ) does
not happen before put(a1 ), call(put, a1 , p) is before ret(rm, a1 ). Since a <A
pb a1 , ret(put, a, p) is
before call(put, a1 , p). Therefore, ret(put, a, p) is before call(rm, b). Since call(rm, b) is before
o, we can see that o is before call(rm, a).
If call(rm, a) is after ret(rm, b), then e|{a,a1 ,b} violates the FIFO property. Therefore, call(rm, a)
is before ret(rm, b). Similarly as the case of reason 1, we can see that ret(rm, b) is before
ret(rm, a).
According to above discussion, there are three possible enumeration of operations of a, a1 and
b, as shown in Figure 22, Figure 23 and Figure 24. Here we explicitly draw the leftmost gappoint of a as o0 . Since the position of ret(put, a1 , p) and call(put, a, p) do not influence the
correctness, we can simply ignore it. We also ignore call(put, b, p) and ret(put, b, _), since the
only requirements of them are (1) rm(b) 6<hb put(b) and (2) call(put, b, p) is before o.
A
- Reason 5, a <B
pb a1 <pb b:
A
Since a1 <pb b, ret(put, a1 ) is before call(put, b, p). Since call(put, b, p) is before o, we can see
that ret(put, a1 , _) is before o.
- If o is before call(rm, a): Then o is obviously before ret(rm, a). Since a <B
pb a1 , ret(rm, a)
is before call(rm, a1 ). Then we can see that, o is before call(rm, a1 ), and remember that
a1 <A
pb b. Then we can goto the case of reason 1 and treat a1 as a. Therefore, we can safely
ignore this.
- If o is before call(put, a, p): Since rm(a) does not happen before put(a, p), we can see that
call(put, a, p) is before ret(rm, a), and then o is before ret(rm, a). Then similarly as above
case, we can see that o is before call(rm, a1 ), and a1 <A
pb b. Then we can goto the case of
reason 1 and treat a1 as a. Therefore, we can safely ignore this.
This completes the proof of this lemma.

J

J

Ahmed Bouajjani, Constantin Enea, and Chao Wang

XX:45

put(b, )
rm(b)
put(a, )

rm(a)

o0

o
Figure 20 The first possible enumeration.

put(b, )
rm(b)
put(a, )

rm(a)

o0

o
Figure 21 The second possible enumeration.

rm(b)
rm(a1 )
put(a1 , )
put(a, )

rm(a)
o0

o

Figure 22 The third possible enumeration.

rm(b)
rm(a1 )
put(a1 , )
put(a, )

rm(a)
o0

o

Figure 23 The forth possible enumeration.

rm(b)
rm(a1 )
put(a1 , )
put(a, )

rm(a)
o

Figure 24 The fifth possible enumeration.

o0

XX:46

Checking Linearizability of Concurrent Priority Queues

Given a data-differentiated execution e with only one maximal priority, two actions act1 , act2 of
maximal priority in e, and assume that act1 is before act2 in e. we say that act1 , act2 is covered by
values d1 , . . . , dm in e, if the priorities of d1 , . . . , dm is smaller than that of act1 and act2 , and
- ret(put, dm , _) is before act1 ,
- For each i < 1 ≤ m,put(di-1 , _) <hb rm(di ),
- act2 is before call(rm, d1 ).
According to Lemma 15, Lemma 16 and Lemma 34, it is not hard to prove that, given a datadifferentiated execution e with only one maximal priority and Has-MatchedMaxPriority= (e) holds.
e is not MatchedMaxPriority-linearizable, if and only if, one of enumerations holds in e (permit
renaming), while call(rm, a) and ret(rm, b) is covered by some d1 , . . . , dm , call(rm, b) is before
ret(put, dm , _), and call(rm, d1 ) is before ret(rm, a). We say that such d1 , . . . , dm constitute the
rightmost gap of b.
Let us begin to represent several register automata that is used to capture the existence of a datadifferentiated execution e, e has a projection e0 , e0 has only one maximal priority, Has-MatchedMax−
Priority(e0 ) holds, there exists values a and b with maximal priority in e0 , a <∗pb b, and the rightmost
gap-point of b is before call(put, a, _) or call(rm, a).
An automaton A1l-eq is given in Figure 25, and it is constructed for the first enumeration in Figure 20. Here we rename the values that cover call(rm, a) and ret(rm, b) into d, and rename the remanning values into >. In this figure, C = {call(put, >, true), ret(put, >, true), call(rm, >), ret(rm, >),
call(rm, empty), ret(rm, empty)}, C1 = C ∪ {call(put, d, < r)}, C2 = C1 ∪ {ret(put, b, = r)},
C3 = C2 ∪ {call(put, d, < r), ret(rm, d)}, C4 = C ∪ {ret(put, b, = r), ret(rm, d)}.
C1
qinit r = ∗

q1

C1
call(put, a, = r)

C2
call(rm, b)

q5

q2

C1
ret(put, a, = r)

C2
ret(put, d, < r)

q6

q3

C2
call(put, b, = r)

C3
call(rm, a)

q7

ret(put, d, < r)

ret(rm, b)

q4

C4

C4

q8

call(rm, d) q
9

C4
ret(rm, a)

q10

call(rm, d)

C3

q11

Figure 25 Automaton A1l-eq

An automaton A2l-eq is given in Figure 26, and it is constructed for the second enumeration in
Figure 21. In Figure 26, C1 , C2 , C3 and C4 is same as that in Figure 25.
For the third enumeration in Figure 22. Since we want to ensure that a and b are putted only once,
we need to explicitly record the positions of call(put, a, p) and call(put, b, p). Since the positions of
call(put, a, p) and call(put, b, p) are not fixed, there are finite possible cases to consider, as shown
below:
- If call(put, b, p) is after call(rm, b) and before call(rm, a): There are two possible positions of
call(put, a, p): (1) before call(rm, a1 ), and (2) after call(rm, a1 ), and before ret(put, a, p).
- If call(put, b, p) is after ret(rm, a1 ) and before call(rm, b): same as above case.

Ahmed Bouajjani, Constantin Enea, and Chao Wang
C1
qinit r = ∗

q1

C1
call(put, a, = r)

q2

ret(put, a, = r)

XX:47

C1

C2

C2

q3

call(rm, b) q
4

call(put, b, = r) q
5
ret(put, d, < r)

c2

C2
ret(put, d, < r)

q6

call(put, b, = r)

q11

C3
cal(rm, a)

q7

ret(put, d, < r)
C3

ret(rm, b)

C4

C4

q8

call(rm, d) q
9

C4
ret(rm, a)

q10

call(rm, d)

q12

Figure 26 Automaton A2l-eq

- If call(put, b, p) is after call(put, a1 , p) and before ret(rm, a1 ): same as above case.
- If call(put, b, p) is after ret(put, a, p) and before call(put, a1 , p): same as above case.
- If call(put, b, p) is after call(rm, a1 ) and before ret(put, a, p): There are three possible positions
of call(put, a, p): (1) after call(put, b, p) and before ret(put, a, p), (2) after call(rm, a1 ) and before call(put, b, p), and (3) before call(rm, a1 ).
- If call(put, b, p) is before call(rm, a1 ): There are three possible positions of call(put, a, p): (1)
after call(rm, a1 ) and before ret(put, a, p), (2) after call(put, b, p) and before call(rm, a1 ), and
(3) before call(put, b, p).
Therefore, there are fourteen possible cases that satisfy the third enumeration in Figure 22. For
each case, we construct an finite automaton. Let A31-eq be the union of register automata that is
constructed for above fourteen cases. For example, for the case ca1 when call(put, a, p) is before
call(rm, a1 ), call(put, b, p) is after ret(rm, a1 ), and call(put, b, p) is before call(rm, b), we construct
a finite automaton A3-1
l-eq in Figure 27. In Figure 27, let C and C1 the same as that in Figure 25.
Let C2 = C1 ∪ {ret(put, a1 , = r)}, C3 = C2 ∪ {ret(put, b, = r)}, C4 = C3 ∪ {call(put, d, <
r), ret(rm, d)}, and C5 = C ∪ {ret(put, b, = r), ret(put, a1 , = r), ret(rm, d)}. Other register automata can be similarly constructed.
Similarly, we construct sets A41-eq and A51-eq of union of register automata for the forth enumeration in Figure 23 and the fifth enumeration in Figure 24, respectively.
Let A1-eq be the union of A1l-eq , A2l-eq , A31-eq , A41-eq and A51-eq . The following lemma states that
A1-eq is MatchedMaxPriority= -complete.
I Lemma 35. A1-eq is MatchedMaxPriority= -complete.
Proof. We need to prove that, given a data-independent implementation I. A1-eq ∩ I =
6 ∅ if and
=
0
0
only if there exists e ∈ I and e ∈ proj(e) such that e is not MatchedMaxPriority -linearizable.
By Lemma 10 and Lemma 15, we need to prove the following fact:
fact1 : Given a data-independent implementation I. A1-eq ∩ I =
6 ∅ if and only if there exists e ∈ I
and e0 ∈ proj(e), Has-MatchedMaxPriority= (e0 ) holds, x is the value with maximal priority in e0 ,
e0 has only one maximal priority, a and b are two values with maximal priority p in e0 , a <∗pb b in e0 ,
and the rightmost gap-point of b is before call(put, a, p) or call(rm, a) in e0 .
The only if direction: Assume that e1 ∈ I is accepted by some register automata in A1-eq . By dataindependence, there exists data-differentiated execution e2 ∈ I and a renaming function r, such that
e1 = r(e2 ). Since e1 is accepted by some register automata in A1-eq , let x, y and z (if exists) be

XX:48

Checking Linearizability of Concurrent Priority Queues

C1
qinit1 r = ∗

q1

C1
call(put, a, = r)

C2
ret(rm, a1 )

q6

q2

C1
call(rm, a1 )

C3
call(put, b, = r)

q7

q3

C1
ret(put, a, = r)

C3
call(rm, b)

q8

q4

C2
call(put, a1 , = r)

C3
ret(put, d)

q9

q5

C4
call(rm, a)

q10

ret(rm, b)

C5

C5

q11

call(rm, d) q
12

ret(rm, a)
ret(put, d, < r)
C4

cal(rm, d)

q14

C5

q13

Figure 27 Automaton A3-1
l-eq

the values that are renamed into b, a and a1 (if exists) by r, respectively, and let d1 , . . . , dm be the
values that are renamed into d by r.
let e00 = e2 |{x,y,z,d1 ,...,dm } . It is obvious that e00 ∈ proj(e2 ), e00 has only one maximal priority,
and Has-MatchedMaxPriority= (e00 ) holds. According to our construction of automata in Auts1-eq , it
is not hard to see that x and y has maximal priority in h2 , y <∗pb x, and the rightmost gap-point of x
is before call(put, y, p) or call(rm, y) in e00 .
The if direction: Assume that there exists e ∈ I6= , e0 ∈ proj(e), such that Has-MatchedMaxPriority= (e0 )
holds e0 has only one maximal priority, a0 and b0 are two values with maximal priority p in e0 ,
a0 <∗pb b0 in e0 , and the rightmost gap-point of b0 is before call(put, a0 , p) or call(rm, a0 ) in e0 . By
data-independence, we can obtain execution e1 as follows: (1) rename a0 and b0 into a and b, respectively, (2) for the values d1 , . . . , dm that constitute the rightmost gap of b0 , we rename them into
0
B
0
d, (3) if a0 <A
pb a1 <pb b, we rename a1 into a1 , and (4) rename the other values into >. It is easy
=
to see that Has-MatchedMaxPriority (e1 ) holds, a and b has maximal priority in e1 , a <∗pb b in e1 ,
and the rightmost gap-point of b is before call(put, a, p) or call(rm, a) in e1 . By Lemma 34, there
are five possible enumeration of operations of a, b, a1 (if exists). Then
- If a <∗pb b because of the first enumeration, it is easy to see that e1 is accepted by A1l-eq .
- If a <∗pb b because of the second enumeration, it is easy to see that e1 is accepted by A2l-eq .
- If a <∗pb b because of the third enumeration, it is easy to see that e1 is accepted by some register
automaton in A31-eq .
- If a <∗pb b because of the forth enumeration, it is easy to see that e1 is accepted by some register
automaton in A41-eq .
- If a <∗pb b because of the fifth enumeration, it is easy to see that e1 is accepted by some register
automaton in A51-eq .
This completes the proof of this lemma.

J

J

Ahmed Bouajjani, Constantin Enea, and Chao Wang

D.5 UnmatchedMaxPriority> (e) Always Holds
I Lemma 36. Given a data-differentiated execution e with only one maximal priority, if Has-Unmat−
chedMaxPriority> (e) holds, then e v l for some l where UnmatchedMaxPriority> -Seq(l, x) holds.
Proof. Since Has-UnmatchedMaxPriority> (e) holds, the actions with maximal priority in e is
some unmatched put. Therefore, no matter how we locate linearization points, we can always obtain
a sequence l of operations that contains unmatched put with maximal priority, and this satisfy the
requirements of UnmatchedMaxPriority> . This completes the proof of this lemma.
J
J

D.6 UnmatchedMaxPriority= (e) Always Holds
I Lemma 37. Given a data-differentiated execution e with only one priority and Has-Unmatched−
MaxPriority= (e) holds. e is not UnmatchedMaxPriority= (e)-linearizable, if and only if there exists
x and y with maximal priority p, x has unmatched put, y has matched put and rm, and put(x, p) <hb
put(y, p).
Proof. The if direction is obvious.
To prove the only if direction, we prove its contrapositive. Assume that for each pair of x and y
with maximal priority in e, if x has unmatched put, y has matched put and rm, then put(x, p) does
not happen before put(y, p). We need to prove that e is UnmatchedMaxPriority= (e)-linearizable.
Let x1 , . . . , xm be the set of values with priority p and has unmatched put in e, let y1 , . . . , yn
be the set of values with priority p and has matched put and rm in e. By assumption, we know that
call(put, yi , p) is before ret(put, xj , p) for each i, j. Then we explicitly construction the linearization
of e by locating the linearization points of e as follows:
- For each xi , locate the linearization point of put(xi , p) just before its return action.
- For each yj , locate the lineariztion point of put(yj , p) jest after its call action.
- For other operations, locate their linearization points at an arbitrary location after its call action
and before its return action.
Let l be the sequence of linearization points. It is easy to see that e v l. Since linearization
points of put(xi , p) is after the linearization point of put(yj , p) for each i, j, it is easy to see that
UnmatchedMaxPriority= -Seq(l, x0 ) holds where x0 = x_ and its return action is after other values
in x1 , . . . , xm . This completes the proof of this lemma.
J
J
Lemma 37 shows how to check non UnmatchedMaxPriority= (e)-linearizable exections. However, the case in Lemma 37 violates our assumption that each single-priority execution is FIFO.
Therefore, we know that UnmatchedMaxPriority= (e) always holds, as states by the following
lemma.
I Lemma 38. Given a data-differentiated execution e with only one maximal priority, if Has-Unmat−
chedMaxPriority= (e) holds, then e v l for some l where UnmatchedMaxPriority= -Seq(l, x) holds.
Proof. According to Lemma 37, if Has-UnmatchedMaxPriority= (e) holds and e is not Unmatched−
MaxPriority= -linearizable, then there exists x and y with maximal priority p, x has unmatched put,
y has matched put, and put(x, p) <hb put(y, p). Let e1 = e|{x,y} . It is obvious that e1 does not
satisfy FIFO property. This contradicts the assumption that every single-priority execution has FIFO
property, and thus, we can safely ignore this case.
J
J

XX:49

XX:50

Checking Linearizability of Concurrent Priority Queues

D.7

Proofs, Definitions and Register Automata for EmptyRemove

In this subsection we construct EmptyRemove-complete register automata. The notion of left-right
constraint of rm(empty) is inspired by left-right constraint of queue [5].
I Definition 39. Given a data-differentiated execution e, and o = rm(empty) of e. The left-right
constraint of o is the graph G where:
-

the nodes are the values of e or o, to which we add a node,
there is an edge from value d1 to o, if put(d1 , _) happens before o,
there is an edge from o to value d1 , if o happens before rm(d1 ) or rm(d1 ) does not exists in h,
there is an edge from value d1 to value d2 , if put(d1 , _) happens before rm(d2 , _).

Given a data-differentiated execution e and o = rm(empty) of e, it is obvious that Has-EmptyRe−
move= (e) holds. Let USet1 (e, o) = {op| op is an operation of some value, and either op <hb o, or
there is op0 with the same value of op, such that op0 <hb o}. For each i ≥ 1, let USeti+1 (e, o) = {op|
op is an operation of some value, op is not in USetk (e, o) for each k ≤ i, and either op happens before some o0 ∈ USeti (e, o), or there is op00 with the same value of o and op00 happens
before some o0 ∈ USeti (e, o)}. We can see that USeti (e, o) ∩ USetj (e, o) = ∅ for any i 6= j. Let
USet(e, o) = USet1 (e, o) ∪ USet2 (e, o) ∪ . . ..
Similarly as UVSet, we can prove the following two lemmas for USet.
I Lemma 40. Given a data-differentiated execution e where Has-EmptyRemove(e) holds. Let o
be a rm(empty) of e. Let G be the graph representing the left-right constraint of o. Assume that G
has no cycle going through o. Then, USet(e, o) contains only matched put and rm.
This Lemma can be similarly proved as Lemma 30.
I Lemma 41. Given a data-differentiated execution e where Has-EmptyRemove(e) holds. Let o
be a rm(empty) of e. Let G be the graph representing the left-right constraint of o. Assume that G
has no cycle going through o. Then, o does not happen before any operation in USet(e, o).
This Lemma can be similarly proved as Lemma 31.
Then we can prove that getting rid of cycle though o in left-right constraint is enough for ensure
linearizable w.r.t MS(SeqPQ3 ), as stated by the following lemma.
I Lemma 42. Given a data-differentiated execution e where Has-EmptyRemove(e) holds. e is
not EmptyRemove-linearizable, if and only if there exists o = rm(empty) in e, G has a cycle going
through o, where G is the graph representing the left-right constraint of o.
Proof. To prove the if direction, assume that there is such a cycle. Assume by contradiction that
e v l = u · o · v and EmptyRemove-Seq(l, o) holds. Let U and V be the set of operations in u and v.
Let the cycle be d1 → d2 → . . . → dm → o → d1 in G. Since dm → o, put(dm , _) happens before
o, and it is easy to see that put(dm , _) is in U . Since U contains matched put and rm, we can see that
operations of dm is in U . Similarly, we can see that operations of dm-1 , . . . , d1 is in U . If rm(d1 )
does not exists, then this contradicts that U contains matched put and rm. Else, if rm(d1 ) exists,
since o happens before rm(d1 ), we can see that rm(d1 ) ∈ V , which contradicts that rm(d1 ) ∈ U .
This completes the proof of the if direction.
To prove the only if direction, we prove its contrapositive. Assume that for each such o and G,
G has no cycle going through o. Let O be the set of operations of e, except for rm(empty). Let
OL = USet(e, o), OR = O \ OL .
0
By Lemma 40, we can see that OL = USet(e, o) contains only matched put and rm. Let OL
be
0
the union of OL and all the rm(empty) that happens before some operations in OL ∪ {o}. Let OR

Ahmed Bouajjani, Constantin Enea, and Chao Wang

XX:51

0
0
be the union of OR and the remanning rm(empty). It remains to prove that for OL
, {o}, OR
, no
elements of the latter set happens before elements of the former set. We prove this by showing that
all the following cases are impossible:
0
- Case 1: If some operation or ∈ OR
happens before o. Then we can see that or ∈ USet(e, o) or
0
0
is a rm(empty) that happens before o, and then or ∈ OL
, which contradicts that or ∈ OR
.
0
0
- Case 2: If some operation or ∈ OR happens before some operation ol ∈ OL . Then we know
that or ∈ USet(e, o) or is a rm(empty) that happens before some operations in OL ∪ {o}, and
0
0
then or ∈ OL
, which contradicts that or ∈ OR
.
0
- Case 3: If o happens before some ol ∈ OL
. If ol ∈ USet(e, o), then by Lemma 41 we know that
this is impossible. Else, ol is a rm(empty) that happens before some operations in OL ∪ {o}, and
o happens before some operations in OL ∪ {o}, which is impossible by Lemma 41.

This completes the proof of the only if direction.
J

J

Let us begin to represent a register automaton that is used for capture the case that, in a subexecution e0 of an execution e, Has-EmptyRemove(e0 ) holds, e0 is not EmptyRemove-linearizable,
and the reason is that there is a cycle going through some rm(empty) o in the left-right constraint of o.
The automaton is A3SeqPQ , which is given in Figure 28. In Figure 28, let C = {call(put, >, true), ret(
put, >, true), call(rm, >), ret(rm, >), call(rm, empty), ret(rm, empty)}, C1 = C∪{call(put, b, true)},
C2 = C1 ∪ {ret(rm, b)}, and C3 = C ∪ {ret(rm, b)}.
C1
qinit ret(put, b, true)

C1

q2

C2
call(rm, empty)

ret(put, b, true)

q3

C2

ret(rm, empty)

C3

C3

q4

call(rm, b) q
5

call(rm, b)

q6

Figure 28 Automaton A3SeqPQ

Given a data-differentiated execution e, we say that o = rm(empty) in e is covered by values
d1 , . . . , dm , if
- put(dm , _) happens before o,
- For each i < 1 ≤ m,put(di-1 , _) happens before rm(di ),
- o happens before rm(d1 ), or rm(d1 ) does not exists in e
According to the definition of left-right constraint for o, in a data-differentiated execution e, there
is a cycle going through o, if and only if there exists values d1 , . . . , dm , such that o is covered by
d1 , . . . , dm .
I Lemma 43. A3SeqPQ is EmptyRemove= -complete.
Proof. We need to prove that, given a data-independent implementation I. A3SeqPQ ∩ I =
6 ∅ if and
only if there exists e ∈ I and e0 ∈ proj(e) such that e0 is not EmptyRemove= -linearizable.
By Lemma 42, we need to prove the following fact:

XX:52

Checking Linearizability of Concurrent Priority Queues

fact1 : Given a data-independent implementation I. A3SeqPQ ∩ I 6= ∅ if and only if ∃e ∈ I6= , e0 ∈
proj(e), Has-EmptyRemove(e0 ) holds, o = rm(empty) is in e0 , and o is covered by some values
d1 , . . . , dm in e0 .
The only if direction: Assume that e1 ∈ I is accepted by A3SeqPQ . By data-independence, there
exists data-differentiated execution e2 ∈ I and a renaming function r, such that e1 = r(e2 ). Let
d1 , . . . , dm be the values in e2 such that r(di ) = b for each 1 ≤ i ≤ m. Let e3 = e2 |{o,d1 ,...,dm } . It is
obvious that e3 ∈ proj(e2 ) and last(e3 ) = SeqPQ3 . It is easy to see that o is covered by d1 , . . . , dm .
The if direction: Assume that there exists such e, e0 , o and d1 , . . . , dm . Then, let e1 be obtained from
e by renaming d1 , . . . , dm into b and renaming other values into >. By data-independence, e1 ∈ I.
It is easy to see that e1 is accepted by A3SeqPQ .
This completes the proof of this lemma.
J
J

D.8

Proofs and Definitions in Section 4.2

In this subsection, we show how to prove that the verification of linearizability of priority queue
to be PSPACE-complete for a fixed number of threads, and EXPSPACE-complete for unbounded
number of processes.
When considering decidability and complexity, we consider only finite variables with finite data
domain. In such case, the priority queue implementations can only model priority queue with
bounded capacity. Then, at some time, the priority queue may become full and then put can not
succeed until some item is removed. However, we assume that each method can always make progress in isolation, which means that put must return some value when the priority queue is full.
Therefore, we introduce a specific value full. A put method returns full indicates that the priority
queue is full now. To fit our results of priority queue in former section, when checking linearizability
of priority queue, we only consider executions without any put(_, _, full). Since does not mean we
consider only executions with bounded number of operations, since an execution can contain unbounded number of pairs of put and remove operations by linearizable w.r.t pairs of put and remove
operations.
Vector Addition Systems with States (VASS): A VASS [4] A = (QA , →A ) contains a finite set
QA of states and a finite set →A of transitions. Each transition is chosen from QA × Zs × QA ,
where s is a positive integer. A vector that has a single non-zero component in {1, −1} is called a
unit vector. We assume, w.l.o.g., that all vectors of transitions are unit vectors.
The operational semantics of a VASS is defined as a LTS. A configuration (q, ~n) of VASS A
contains a state q ∈ QA with a vector ~n ∈ Ns . ~n can be considered as values of several counters.
We use ~n(i) to denote the i-th component of ~n. The transitions between configurations of VASS is
defined as follows: (q1 , ~n1 ) →A (q2 , ~n2 ), if there exists vector ~n, such that (1) (q1 , ~n, q2 ) ∈→A , (2)
if ~n(j) = 1 for some j, then ~n2 is obtain from ~n1 by increasing the i-th component by 1, and (3) if
~n(j) = −1 for some j, then ~n2 is obtain from ~n1 by decreasing the i-th component by 1.
The state-reachability problem of VASS is to determine whether some configuration with state q
is reachable from a given configuration (q0 , ~0). Here ~0 is a specific vector for which all components
are 0 and q0 is the initial state of VASS.
Reducing priority Queue into PSPACE and EXPSPACE problems: We describe a class C of
data-independent implementations for which linearizability w.r.t. SeqPQ is decidable. The implementations in C allow an unbounded number of values but a bounded number of priorities. Each
method manipulates a finite number of local variables which store Boolean values, or data values
from D. Methods communicate through a finite number of shared variables that also store Boolean
values, or data values from D. Data values may be assigned, but never used in program predicates
(e.g., in the conditions of if-then-else and while statements) so as to ensure data independence. This

Ahmed Bouajjani, Constantin Enea, and Chao Wang

class captures typical implementations, or finite-state abstractions thereof, e.g., obtained via predicate abstraction. Since the Γ-complete automata A(Γ) uses a fixed set D = {a, b, a1 , d, e, >} of
values, we have that C ∩ A(Γ) 6= ∅ for some Γ iff CD ∩ A(Γ) 6= ∅ where CD is the subset of C that
uses only values in D.
We model the set CD as the executions of a Vector Addition System with States (VASS) similarly
to Bouajjani et al. [4]. A VASS has a finite set of states, and manipulates a finite set of counters
holding non-negative values. The idea is that the states of the VASS represent the global variables of
CD . This set is finite as we have bounded the data values. Each counter of the VASS then represents
the number of threads which are at a particular control location within a method, with a certain
valuation of the local variables. Here again, as the data values are bounded, there is a finite number
of valuations. When a thread moves from a control location to another, or updates its local variables,
we decrement, resp., increment, the counter corresponding the old, resp., the new, control location
or valuation.
For a fixed set of priorities P , the register automata A(Γ) can be transformed to finite-state
automata since the number of possible valuations of the registers is bounded. In this way, we reduce
checking linearizability of priority queue into the the EXPSPACE-complete problem of checking
state-reachability in a VASS. When we consider only finite number of threads, the value of counters
are bounded and then this problem is PSPACE [10].
Reducing PSPACE and EXPSPACE problems into linearizability of priority queue for bounded
number of threads: We show how to reduce the state-reachability problem of VASS into checking
linearizability of priority queue. Our construction is based on the reduction of state-reachability
problem of counter machine and VASS into linearizability in [4].
There are already several linearizable lock-free implementations of priority queue [21, 17]. It is
not hard to modify them to fit finite variables with finite data domain and it is obvious that they are
still linearizable then. Let Imp-PQlf be one such implementations. It is safe to assume that Imp-PQlf
is given in the form of pseudo-code. We use putlf and rmlf to explicitly denote the pseudo-code of
put and remove method of Imp-PQlf .
A counter machine is a VASS that can additional detect if the value of some counter is 0. In [4],
they construct a library LA that simulate executions of counter machine A. This library use finite
variables with finite data domain. It contains the following six methods:
- M(q,~n,q0 ) , which represents a transition resulting of (q, ~n, q 0 ).
- M(q,i,q0 ) , which represents a transition that from state q to state q 0 while detecting the value of
counter i to be 0.
- Mqf . This method returns if the simulating reaches some state with state qf .
- Minc-i , which simulates increasing counter i with 1.
- Mdec-i , which simulates decreasing counter i with 1.
- Mzero-i , which simulates testing whether the value of counter i to be 0.
The first three methods do their work with the help of the latter three methods. For example, a
M(q,~n,q0 ) method (that increases counter j) will activate a Minc−j method and a Mdec−j method.
Let D0 = {(q, ~n, q 0 )|q, q 0 ∈ QA − {qf }, ~n ∈ Zs } ∪ {qf } ∪ {inc-i, dec-i|1 ≤ i ≤ s}. Let RAs be
the register automata obtained as follows:
- Given Γ ∈ {EmptyRemove, UnmatchedMaxPriority, MatchedMaxPriority}, we modify the
Γ-complete automata while the original value of > is replaced by values > and all values in D0 .
- For register automata that checks FIFO of sub-executions of operations with a same priority,
if the original value under consideration is {b} (the first three automata) or {a, b} (the forth
automaton), then we replace them with {b} ∪ D0 and {a, b} ∪ D0 , respectively.

XX:53

XX:54

Checking Linearizability of Concurrent Priority Queues

Algorithm 2: rm of PQA
Output: A removed value
1 if reachQf = true then
2
return a random value from D0 ;
3 else
4
return rmlf ();

Given a VASS A, we construct a priority queue implementation PQA as follows:
- A new memory location reachQf is introduced. Its initial value is set to false.
- The rm method first check the value of reachQf. If it is true, then it returns a random value.
Otherwise, it works as rmlf . The pseudo-code of rm is shown in Algorithm 2.
- The put method uses items from D0 ∪ {a, b, a1 , d, e, >}. It first uses putlf to do the work of
priority queue, and then choose a role and begin to simulate transitions of A, until qf is reached.
Then, it set the flag reachQf to be true. The pseudo-code of put is shown in Algorithm 3.
In [4], to use a library to simulate counter machine A, their library LA contains the following
variables: (1) variable q that uses value from QA , (2) vector req[] and ack[], the index is chosen from
1 to the number of unit vectors of length s, (3) dec[], where the index is chosen form 1 to s.
Let us explain how put method do to act according to its chosen role. We use the case of
trans(q, ~n, q 0 ) as an example while other cases can be similarly obtained. For the role trans(q, ~n, q 0 ),
it works as M(q,~n,q0 ) in LA . Or we can say, it do the following work:
- atomically do wait(q) and signal(req[~n]),
- atomically do wait(ack[~n]) and signal(q 0 ),
Note that we want to obtain a implementation where each method can always make progress
in isolation. To obtain such an implementation, we need to slightly modify the wait command as
follows:
- If a wait command find itself blocked, then it can still proceed. However, in this case the put
method will return a specific value fail. Moreover, when deciding linearizability, we do not
consider executions with return value fail.
Follows the proof in [4], we can prove that (qf , _) is reachable in A, if and only if PQA is
not linearizable w.r.t SeqPQ. In this way, we reduce the state-reachability problem of VASS into
checking linearizablity of priority queue.
With above discussions, we can now prove the following theorem:
Theorem 17: Verifying whether an implementation in C is linearizable w.r.t. SeqPQ is PSPACEcomplete for a fixed number of threads, and EXPSPACE-complete otherwise.

Ahmed Bouajjani, Constantin Enea, and Chao Wang

Algorithm 3: put of PQA
Input: An item itm and its priority p
Output: full if the priority queue is full
1 x = putlf (itm, p);
2 random select a role from {trans(q, ~
n, q 0 ), reach-qf , inc-i, dec-i};
3 works according to chosen role;
4 if qf is reached then
5
reachQf := true;
6 if x = full then
7
return x;
8 else
9
return;

XX:55

