1

arXiv:1708.08323v2 [] 3 Apr 2018

Scheduling Constraint Based Abstraction Refinement for
Multi-Threaded Program Verification
LIANGZE YIN, School of Computer, National University of Defense Technology, China
WEI DONG, School of Computer, National University of Defense Technology, China
WANWEI LIU, School of Computer, National University of Defense Technology, China
JI WANG, School of Computer, National University of Defense Technology, China
Bounded model checking is among the most efficient techniques for the automatic verification of concurrent
programs. However, encoding all possible interleavings often requires a huge and complex formula, which
significantly limits the salability. This paper proposes a novel and efficient abstraction refinement method
for multi-threaded program verification. Observing that the huge formula is usually dominated by the exact
encoding of the scheduling constraint, this paper proposes a scheduling constraint based abstraction refinement
method, which avoids the huge and complex encoding of BMC. In addition, to obtain an effective refinement,
we have devised two graph-based algorithms over event order graph for counterexample validation and
refinement generation, which can always obtain a small yet effective refinement constraint. Enhanced by
two constraint-based algorithms for counterexample validation and refinement generation, we have proved
that our method is sound and complete w.r.t. the given loop unwinding depth. Experimental results on
SV-COMP 2017 benchmarks indicate that our method is promising and significantly outperforms the existing
state-of-the-art tools.
CCS Concepts: •Software and its engineering → Software verification and validation;
Additional Key Words and Phrases: Multi-Threaded Program, Bounded Model Checking, Scheduling Constraint,
Event Order Graph
ACM Reference format:
Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang. 2016. Scheduling Constraint Based Abstraction Refinement
for Multi-Threaded Program Verification. 1, 1, Article 1 (January 2016), 26 pages.
DOI: 10.1145/nnnnnnn.nnnnnnn

1

INTRODUCTION

Facilitated by the popularization of multi-core architectures, concurrent programs are becoming
popular to take full advantage of the available computing resources. However, due to the nondeterministic thread interleavings, traditional approaches such as testing and simulation are hard
to guarantee the correctness of such programs. Automatic program verification has become an
important complementary to traditional approaches. Given that most of the errors can be detected
with small loop unwinding depths, bounded model checking (BMC) has been proven to be one
of the most efficient techniques for the automatic verification of concurrent programs [6, 33].
However, due to the complex inter-thread communication, a huge encoding is usually required to
offer an exact description of the concurrent behavior, which greatly limits the scalability of BMC
for concurrent programs.
This paper focuses on multi-threaded programs based on shared variables and sequential consistency (SC) [2]. For these programs, we have observed that the scheduling constraint, which defines
This work has been submitted to the IEEE for possible publication. Copyright may be transferred without notice, after
which this version may no longer be accessible.
2016. XXXX-XXXX/2016/1-ART1 $15.00
DOI: 10.1145/nnnnnnn.nnnnnnn

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:2

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang

that “for any pair hw, r i s.t. r reads the value of a variable v written by w, there should be no other
write of v between them,” significantly contributes to the complexity of the behavior encoding. In
the existing work of BMC, to encode the scheduling constraint, each access of a shared variable is
associated with a “clock variable”. The scheduling constraint is then encoded into a complicated
logic formula over the state and clock variables, the size of which is cubic in the number of shared
memory accesses [3].
Inspired by this observation, this paper proposes a novel method for multi-threaded program
verification which performs abstraction refinement by weakening and strengthening the scheduling
constraint. It initially ignores the scheduling constraint and then obtains an over-approximation
abstraction of the original program (w.r.t. the given loop unwinding depth). If the property is
safe on the abstraction, then it also holds on the original program. Otherwise, a counterexample
is obtained and the abstraction is refined if the counterexample is infeasible. N. Sinha and C.
Wang also performed abstraction refinement to deal with the overhead of an exact encoding of
the concurrent behavior [35]. However, their abstraction model was performed by restricting the
sets of read events and read-write links, while we consider all read events and read-write links but
ignore the scheduling constraint.
The efficiency of our method depends on the number of iterations required to verify the property
and the sizes of the constraints added during the refinement process. Another innovation of this
paper is that, to verify the property with a small number of small problems, we have devised
two graph-based algorithms over event order graph (EOG) for counterexample validation and
refinement generation, s.t. an effective refinement constraint can be obtained in each refinement
iteration. Whenever an abstraction counterexample is determined to be infeasible, we can always
obtain a set of “core kernel reasons” of the infeasibility, which can usually be encoded into simple
constraints and reduce a large amount of space. In our experiments, most of the programs can be
verified within dozens of refinement iterations. Meanwhile, the increased size of the abstraction
during the refinement process can usually be ignored compared with that of the initial abstraction.
Our graph-based EOG validation method is effective in practice. Given an infeasible EOG, it can
usually identify the infeasibility with rare exceptions. If it is not sure whether an EOG is feasible or
not, we explore a constraint-based EOG validation process to further validate its feasibility. If an
infeasibility is returned, we explore a constraint-based refinement generation process to refine the
abstraction. Enhanced by these two constraint-based processes, we have proved that our method is
sound and complete w.r.t the given loop unwinding depth.
We have implemented the proposed method on top of CBMC and applied it to the benchmarks
in the concurrency track of SV-COMP 2017 [36]. The experimental results demonstrate that our
method drastically improves the verification performance. Without the scheduling constraint, the
formula size reduces to 1/8 on average, whereas the number of CNF clauses increased during the
refinement process can usually be ignored compared with that of the abstraction. Moreover, our
tool has successfully verified all these examples within 1550 seconds and 43 GB of memory. By
contrast, Lazy-CSeq-Abs — a leading tool for concurrent program verification — spended 9820
seconds and 104 GB memory to achieve the same score. Our tool has won the gold medal in the
concurrency track of SV-COMP 2017 [36] (Warning: It will violate our anonymity).
The contributions of this paper are listed as follows.

(1) This paper presents a scheduling constraint based abstraction refinement method for multithreaded program verification, which avoids the huge and complex constraint to encode
the concurrent behavior.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification1:3
(2) This paper presents two graph-based algorithms over event order graph for counterexample validation and refinement generation, which can always obtain a small yet effective
refinement constraint in practice.
(3) To ensure the soundness, we have enhanced our method by two constraint-based algorithms
for counterexample validation and refinement generation. In this manner, a both efficient
and sound method for multi-threaded program verification is obtained.
(4) We have implemented our method on top of CBMC. The evaluation on the SV-COMP
2017 benchmarks indicates that our method is promising and significantly outperforms the
existing state-of-the-art tools.
The rest of this paper is organized as follows. Section 2 introduces the preliminaries. Section 3
outlines and illustrates our proposed method by presenting a running example. Sections 4 and 5
present our EOG-based counterexample validation and refinement generation algorithms, respectively. Section 6 discusses the soundness and efficiency of our method. Section 7 provides the
experimental results. Section 8 reviews the related work, and Section 9 concludes the paper.
2

PRELIMINARIES

2.1

Multi-Threaded Program

A multi-threaded program P consists of N ≥ 1 concurrent threads Pi (1 ≤ i ≤ N ). It contains a
set of variables which are partitioned into shared variables and local variables. Each thread Pi can
read/write both the shared variables and its local variables. We focus on programs based on PThreads,
one of the most popular libraries for multi-threaded programming. It uses pthread create(&t,
&attrib, &f, &args) to create a new thread t, and pthread join(t, & return) to suspend
the current thread until thread t terminates 1 .
In this paper, we assume each variable access is atomic. We also assume that each statement t of a
multi-threaded program is either 1) a global statement that contains only one shared variable access
(it may further contain multiple local variable accesses) or 2) a local statement that only operates
on local variables. A statement with multiple shared variable accesses can always be translated to a
sequence of global statements. By defining the expressions suitably and using source-to-source
transformations, we can model all statements using global and local statements.
We also assume that all functions are inlined and all loops are unwound by a limited depth (it is
a basic proviso in BMC). We also omit the discussion on modeling the sophisticated C language
data elements, such as pointers, structures, arrays, and heaps, etc., because they are irrelative with
the concurrency and we deal with them in the same way as CBMC does. The discussion on PThread
primitives, such as pthread mutex lock and pthread mutex unlock, etc., are also omitted in this
paper. In CBMC, they are implemented by shared variables and we deal with them in the same
way as CBMC does.
Given a multi-threaded program, we write V for the set of shared variables. An event e is a
read/write access to a shared variable. We use E to denote all of them. Each global statement
corresponds to an event, i.e., the event contained in the global statement. Each e ∈ E is associated
with an element var(e) ∈ V, a type type(e), and a literal guard(e), which represent the accessed
variable, the type of access, and the guard condition literal, respectively. type(e) can be either rr
(i.e., “read”) or ww (i.e., “write”). Any event e with var(e) = v and type(e) = rr (resp. type(e) = ww)
is called a read (resp. a write) of v. To express the execution orders of different events, we also
associate each event with an unique natural number clk(e). clk(e 1 ) < clk(e 2 ) represents that e 1
executes before e 2 .
1 More

information about PThreads can be found at https://computing.llnl.gov/tutorials/pthreads/

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:4

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang

The program P determines a partial order ≺P0 ⊂ E × E. Intuitively, e 1 ≺P0 e 2 (or we write
(e 1 , e 2 ) ∈≺P0 ) indicates that “e 1 should happen before e 2 according to the program order of P”.
According to the program order, e 1 ≺P0 e 2 holds in the following three cases.
• For any two events e 1 and e 2 of the same thread, if e 1 must happen before e 2 according to
the sequential semantics, then we have e 1 ≺P0 e 2 .
• If pthread create() is used to create a new thread t at some point p of the current thread,
then for any event e 1 of the current thread before p and e 2 of the thread t, we have e 1 ≺P0 e 2 .
• If pthread join(t) is used to suspend the current thread at some point p, then for any
event e 1 of the thread t and e 2 of the current thread after p, we have e 1 ≺P0 e 2 .
A read-write link (e 1 , e 2 ) represents that “e 2 reads the value written by e 1 ”. Therefore, type(e 1 ) =
ww, type(e 2 ) = rr, var(e 1 ) = var(e 2 ), and the value of e 2 is equal to that of e 1 . In addition, there
should be no other “write” of var(e 1 ) happening between them. Given a read-write link λ := (e 1 , e 2 ),
we denote by sel(λ) the read-write link literal (a boolean variable) that represents the link.
2.2

Bounded Model Checking

Bounded model checking [7] is one of the most applicable techniques to alleviate the state space
explosion problem in concurrent program verification. Given that most of the errors can be
detected with small loop unwinding depths, the unwinding depth for those loops and recursions is
limited [33]. Instead of explicitly enumerating all thread interleavings, BMC employs a symbolic
representation to encode the verification problem, which is then solved by a SAT/SMT solver. If a
positive answer is given, then a satisfying assignment corresponding to a feasible counterexample
is acquired. Otherwise, the program is proven safe w.r.t. the given loop unwinding depth.
In BMC, the monolithic encoding of a multi-threaded program is usually represented as α :=
ϕ init ∧ ρ ∧ζ ∧ξ , where ϕ init is the initial states, ρ encodes each thread in isolation, ζ formulates that
“each read of a variable v may read the result of any write of v”, and ξ formulates the scheduling
constraint, which defines that “for any pair hw, r i s.t. r reads the value of a variable v written by w,
there should be no other write of v between them” [3].
3
3.1

METHOD OVERVIEW AND ILLUSTRATION
Method Overview

The performance of BMC is usually decided by that of the constraint solving, the performance
of which depends significantly on the size of the constraint problem. Hence, an important way
to improve the performance of BMC is to reduce the size of the constraint problem. In BMC of
multi-threaded programs, we have observed that the monolithic encoding α is usually dominated
by the scheduling constraint ξ . To reduce the constraint problem size, we propose to ignore the
scheduling constraint in the constraint solving process. An abstraction of the monolithic encoding
is then obtained, which is defined as follows.
Definition 3.1. Given a multi-threaded program, the abstraction ignoring the scheduling constraint can be formulated as φ 0 := ϕ init ∧ ρ ∧ ζ , where ϕ init is the initial states, ρ encodes each
thread in isolation, and ζ formulates that “each read of a variable v may read the result of any write
of v”.
The scheduling constraint ξ defines a set of order requirements among the events. All of them
should be satisfied for any concrete execution of a multi-threaded program. Hence, whenever
a counterexample π of the abstraction is obtained, further validation is required to determine
whether π satisfies all the order requirements defined in ξ . If that is true, π is feasible. Otherwise,
π is infeasible. In other words, it may not correspond to a concrete execution. In this case, we
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification1:5
Refinement Constraint

i

Graph-based
Refinement
Abstraction 0
Error states err

Multi-Threaded
C Program

Constraint-based
Refinement

[Infeasible]
Abstraction
Model

[SAT]

Graph-based
EOG Validation

[Not Sure]

[UNSAT]

[Infeasible]
Constraint-based
EOG Validation
[Feasible]

True
Counterexample

Proof

Fig. 1. An overview of our method

continually search the rest of the abstraction space for another new counterexample, until a feasible
counterexample is found or all counterexamples of the abstraction have been determined to be
infeasible.
Fig. 1 presents an overview of our method. Given a multi-threaded C program, we first add the
abstraction φ 0 and the error states ϕ er r to the abstraction model. If it is unsatisfiable, then the
property is proven safe w.r.t. the given loop unwinding depth. Otherwise, a counterexample of
the abstraction is provided. Given that the scheduling constraint is ignored in the abstraction, this
counterexample may be infeasible and further validation is required. In our method, the feasibility
of an abstraction counterexample is determined via validating the feasibility of its corresponding
event order graph (EOG). An intuitive method for EOG validation is constraint solving. If the EOG is
infeasible, then the abstraction is refined by exploring the unsatisfiable core. However, this method
is not effective for refinement generation (cf. Section 5). To obtain an effective refinement, we
have devised two graph-based algorithms over EOG for EOG validation and refinement generation,
in which a small yet effective refinement can always be obtained if the EOG is determined to
be infeasible. However, this method is not complete. It can only give an infeasible answer (cf.
Section 4). To make our method both efficient and sound, we first adopt the graph-based EOG
validation method. If the EOG is determined to be infeasible, the graph-based refinement process is
performed to obtain an effective refinement constraint. Otherwise, we employ the constraint-based
validation process to further validate the EOG. Our experiments demonstrate that our graph-based
EOG validation method is effective in practice. It can always identify the infeasibility of an infeasible
EOG with rare exceptions. Actually, the constraint-based refinement generation process (the dashed
part of Fig. 1) has never been invoked on SV-COMP 2017 benchmarks.
3.2

Method Illustration

We provide a running example to illustrate our method. The program involves three threads,
namely, main, thr1, and thr2, as shown in Fig. 2(a). In this example, the set of shared variables
V := {x, y, m, n}, which are initialized to {1, 1, 0, 0}, respectively. The main thread creates threads
thr1 and thr2, and then waits until these two threads terminate. We attempt to verify that it is
impossible for both m and n to be 1 after the exit of thr1 and thr2. This program offers a modular
proof to this property.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:6

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang
int x = 1, y = 1, m = 0, n = 0;
void* thr1(void * arg) {
x = y + 1;
m = y;
x = 0;
}
void* thr2(void * arg) {
y = x + 1;
n = x;
y = 0;
}
void main() {
pthread_t t1, t2;
pthread_create(&t1, 0, thr1, 0);
pthread_create(&t2, 0, thr2, 0);
pthread_join(t1, 0);
pthread_join(t2, 0);
assert (!(m == 1 && n == 1));
}

int x1 = 1, y1 = 1, m1 = 0, n1 = 0;
void* thr1(void * arg) {
x2 = y2 + 1;
m2 = y3;
x3 = 0;
}
void* thr2(void * arg) {
y4 = x4 + 1;
n2 = x5;
y5 = 0;
}
void main() {
pthread_t t1, t2;
pthread_create(&t1, 0, thr1, 0);
pthread_create(&t2, 0, thr2, 0);
pthread_join(t1, 0);
pthread_join(t2, 0);
assert (!(m3 == 1 && n3 == 1));
}

(a) The original program

(b) The SSA statements of the program

Fig. 2. A three-thread program

Initial abstraction. We use ϕ init and ϕ er r to denote the initial and error states, respectively, while
ρmain , ρ t hr 1 , and ρ t hr 2 denote the transition relationships of these three threads, respectively, and
ρ is the conjunction of those transition relationships of all threads.
To encode the program, as shown in Fig. 2(b), we convert the original program into a set of static
single assignment (SSA) statements, in which the program variables are renamed s.t. each variable
is assigned only once. Particularly, each “read” of any shared variable also has a unique name.
Then ϕ init , ϕ er r , and ρ are defined as follows. Note that the transition relationship of each thread
(such as ρmain , ρ t hr 1 , and ρ t hr 2 ) encodes that thread in isolation, i.e., it doesn’t consider the thread
communications.
ϕ init
ϕ er r
ρ t hr 1
ρ t hr 2
ρmain
ρ

:= (x 1 = 1) ∧ (y1 = 1) ∧ (m 1 = 0) ∧ (n 1 = 0)
:= (m 3 = 1) ∧ (n 3 = 1)
:= (x 2 = y2 + 1) ∧ (m 2 = y3 ) ∧ (x 3 = 0)
:= (y4 = x 4 + 1) ∧ (n 2 = x 5 ) ∧ (y5 = 0)
:= true
:= ρ t hr 1 ∧ ρ t hr 2 ∧ ρmain

To encode ζ , we must identify the behavior of every “read” event. Consider the shared variable
x for example. There are five read/write accesses to the variable x. For each access, as shown in
Fig. 2(b), we rename x to a unique name in the SSA statements, i.e., x 1 , x 2 , · · · , x 5 . We denote by e x i
(1 ≤ i ≤ 5) the event corresponding to x i . Then {e x 1 , e x 2 , e x 3 } and {e x 4 , e x 5 } are the sets of “writes”
and “reads” of x, respectively. We use a read-write link literal sv,i, j to indicate that ev j reads the
value written by evi (v ∈ V). The encoding ψ x i (i = 4, 5), defined below, indicates that the value
of x i can take any value of x 1 , x 2 , and x 3 . Given that the variable x i can not take several different
values simultaneously, the formula s x,4,1 ∨ s x,4,2 ∨ s x,4,3 represents that, among these three literals,
there is one and only one true literal. We denote by ζ x the conjunction of ψ x 4 and ψ x 5 . It formulates
the possible behaviors of all “reads” of x.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification1:7

ψ x 4 := (s x,4,1 ⇒ (x 4 = x 1 ))∧
(s x,4,2 ⇒ (x 4 = x 2 ))∧
(s x,4,3 ⇒ (x 4 = x 3 ))∧
(s x,4,1 ∨ s x,4,2 ∨ s x,4,3 )
ψ x 5 := (s x,5,1 ⇒ (x 5 = x 1 ))∧
(s x,5,2 ⇒ (x 5 = x 2 ))∧
(s x,5,3 ⇒ (x 5 = x 3 ))∧
(s x,5,1 ∨ s x,5,2 ∨ s x,5,3 )
ζ x := ψ x 4 ∧ ψ x 5
Similarly, we obtain the corresponding formulas of ζy , ζm , and ζn . Let ζ := ζ x ∧ ζy ∧ ζm ∧ ζn .
The initial abstraction can then be formulated as follows.
φ 0 := ϕ init ∧ ρ ∧ ζ

(1)

Constraint solving of the first round. Using φ 0 ∧ ϕ er r as input to a constraint solver will return
SAT and yield a counterexample π0 , which is a set of assignments to the variables in φ 0 ∧ ϕ er r .
Counterexample validation of the first round. Given that the scheduling constraint is excluded
from the abstraction, such a counterexample may be infeasible. In our method, a counterexample
π is validated via validating its corresponding EOG (cf. Section 4), which captures all the order
requirements among the events of π . We first employ the graph-based EOG validation method to
determine its feasibility.
Fig. 3 shows the EOG corresponding to π0 . In figures that describe EOGs, the white and gray
nodes denote “writes” and “reads” occurring in the corresponding counterexample, respectively. A
solid arrow with a triangular head from e 1 to e 2 represents a program order, which requires that
e 1 should happen before e 2 . A dashed arrow from e 1 to e 2 represents a read-write link (e 1 , e 2 ). It
requires that 1) e 1 should happen before e 2 , and 2) no “write” of var(e 1 ) can happen between them.
A solid arrow with a hollow head from e 1 to e 2 represents a derived order, which is derived from
existing order requirements. It also requires that e 1 should happen before e 2 . For brevity, in these
figures, we use the subscripts of an event as labels, that is, we use vi to represent the event evi . Now
the question is: Is there any total order of all these nodes that satisfies all these order requirements?
This is not a trivial problem. However, if there exists some cycle in the graph, then the answer
must be “no”, and the counterexample is infeasible.
Given a counterexample π and two events e 1 and e 2 , we use e 1 ≺π e 2 to represent that e 1 should
happen before e 2 in π . By applying our graph-based EOG validation algorithm (cf. Section 4),
we can deduce two derived orders ey3 ≺π0 ey4 and e x 5 ≺π0 e x 2 , which are denoted by h 1 and h 2
respectively 2 . Fig. 3 shows two cycles, including C 1 : e x 2 ≺π0 ey3 ≺π0 ey4 ≺π0 e x 5 ≺π0 e x 2 and
C 2 : e x 2 ≺π0 e x 4 ≺π0 ey4 ≺π0 e x 5 ≺π0 e x 2 . Therefore, π0 is infeasible.
Refinement of the first time. To prune more search space rather than just one counterexample,
we should find the “kernel reasons” that make the counterexample infeasible. According to our
graph-based kernel reason analysis algorithm (cf. Section 5), the derived orders h 1 and h 2 are caused
by r 1 and r 3 , respectively (according to Rule 3). h 1 is derived as follows. According to the order
requirements of r 1 , we have that y1 ≺π0 y3 , and no “write” of y can be executed between y1 and y3 .
According to the program orders, we have y1 ≺π0 y4 . Hence, we can deduce that y3 ≺π0 y4 . Given
that the guard conditions for all these events are true, as long as r 1 holds in the counterexample,
we may obtain the derived order h 1 . Hence, the reason of h 1 is r 1 . Similarly, we can obtain that the
2 We

can deduce more orders from the EOG, but we only list h 1 and h 2 , because they will be used later.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:8

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang

x1

x1

y1

y1

m1
n1

x4

n1

y2

y4

x2

x5

y3

n3

m2

y5

x3

r3

m1

r2

r1

r4

h1

x4

h2

y4
x5

n2
r5

r6

m2

m3

n2

n3

y5

Fig. 3. EOG of counterexample π 0 .

x1

y1

m1

n1

m3

n3

reason of h 2 is r 3 . Given that the guard conditions for xall
these events are true, the reason for any
1
program order is TRUE. And according to Section 5, the reason for any read-write link is itself.
y1
A kernel reason of a cycle C is a conjunction of those kernel
reasons for those orders constructing
r
h1 r 4 . Given that r 1 , r 3 , and
4
C. We can
obtain that C 1 is causedrby r 1 ∧ r 3 , and C 2m1is caused
r2 by r 3 ∧
1
r 4 are represented by read-write link literals sy,3,1 , s x,5,1 , and s x,4,2 , respectively, we obtain that
n1
the kernel reason of C 1 is {sy,3,1 , s x,5,1 }, and the
y2 kernel reason ofx4C 2 is {s x,5,1 , s x,4,2 }. We hence use
x4 κ 0 := ¬(sy,3,1 ∧ s x,5,1 ) ∧ ¬(s x,5,1 ∧ s x,4,2
x2 ) as
r3 the refinement constraint,y4which contains only two
y
simple 4CNF clauses.
x

y3

x5

5
Second
constraint solving. Let φ 1 := φ 0 ∧ κ 0 . When using φ 1 r∧4 ϕ er r as input, the constraint solver
m2 counterexample π 1 .
n2
returns
n2 SAT again, and produces a new
r
r6
5
r6
x3 applying
y5 validation algorithm, the
Second
our graph-based
EOG
y5 counterexample validation. By
EOG corresponding to π1 has two cycles. Hence, π1 ismalso
infeasible.
3

Refinement, the second time. Again, we apply our graph-based
kernel reason analysis algorithm.
n3
The refinement constraint is formulated as κ 1 := ¬(s x,4,3 ∧s x,5,1 ) ∧ ¬(sy,2,4 ∧s x,4,3 ) ∧ ¬(sy,4,3 ∧s x,4,3 ),
which contains three simple CNF clauses. Here, one of these two cycles has two different kernel
reasons.
Third constraint solving. Same as before, let φ 2 := φ 1 ∧ κ 1 . When using φ 2 ∧ ϕ er r as input to a
constraint solver, we get another counterexample π2 .
Third counterexample validation. By applying our graph-based EOG validation algorithm, the
EOG corresponding to π2 also has two cycles. Hence, π2 is also infeasible.
Refinement, the third time. By applying our graph-based kernel reason analysis algorithm, we
obtain a new refinement constraint κ 2 := ¬(sy,3,1 ∧ sy,2,5 ) ∧ ¬(s x,5,2 ∧ sy,2,5 ), which contains two
simple CNF clauses.
Constraint solving, the fourth time. Let φ 3 := φ 2 ∧κ 2 . When using φ 3 ∧ϕ er r as input, the constraint
solver returns UNSAT this time, which indicates that the property is safe.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification1:9
Given that the serial of constraint solving queries are incremental, they can be solved in an
incremental manner. From this example, we can observe that:
(1) Without the scheduling constraint, the size of the abstraction is much smaller than that
of the monolithic encoding. In this example, excluding the 3049 CNF clauses encoding
the pthread create and pthread join function calls, the monolithic encoding contains
10214 CNF clauses, while the abstraction φ 0 contains only 1018 CNF clauses.
(2) With our graph-based refinement generation method, the verification problem can usually be solved with a small number of refinement iterations. In this example, only three
refinements are required to verify the property.
(3) With our graph-based refinement generation method, the number of clauses increased
during the refinement process can usually be ignored compared with that of the abstraction.
In this example, only 7 simple CNF clauses are added during the refinement process, while
the initial abstraction contains 4067 CNF clauses.
(4) Our graph-based EOG validation method is effective to identify the infeasibility in practice.
In this example, all the four abstractions are infeasible. All of them can be detected by our
graph-based EOG validation process. The constraint-based EOG validation and refinement
processes have never been invoked.
4
4.1

EOG-BASED COUNTEREXAMPLE VALIDATION
Counterexample and Event Order Graph

Definition 4.1. A counterexample π of an abstraction φ i , or a counterexample π for short, is a set
of assignments to the variables in φ i ∧ ϕ er r , where ϕ er r is the error states.
A counterexample π is an execution of the abstraction that falsifies the property. It defines a
trace for each thread and the read-write relationship among the “reads” and “writes” occurring in
π . Given that the scheduling constraint is ignored in the abstraction, the counterexample may not
be feasible, i.e., it may not correspond to any concrete execution. Note that the execution order of
those statements from different threads is not defined. If the counterexample is feasible, it may
correspond to multiple concrete executions.
Given a counterexample π , we use Eπ ⊆ E to denote the set of events occurring in π . We define
a partial order ≺π ⊆ Eπ × Eπ . Intuitively, e 1 ≺π e 2 represents that “e 1 should happen before e 2 in π ”,
i.e., clk(e 1 ) < clk(e 2 ). We also use ≺π0 to denote the restriction of ≺P0 on π . In this case, ≺π0 ⊆≺P0 , and
we have ≺π0 ⊆≺π . We also focus on the partial order π , which is called the read-from relationship
of π . e 1 π e 2 (or we write (e 1 , e 2 ) ∈ π ) represents that “(e 1 , e 2 ) is a read-write link in π ”. According
to this definition, we obtain π ⊆≺π . An element in ≺π0 (resp. in π ) is called a program order
(resp. read-from order) of π .
A counterexample π defines a quadruple hs 0, π , Tπ , Eπ , π i, where s 0, π is the initial states, Tπ is
the set of statements contained in π , Eπ is the set of events occurring in π , and π ⊆ Eπ × Eπ is
the read-from relationship that links each “read” r ∈ Eπ to a “write” w ∈ Eπ s.t. r reads the value
written by w. Note that ≺π0 is the restriction of ≺P0 to Eπ . Table 1 lists the set of notations we use
for a counterexample π .
Definition 4.2. A counterexample π is feasible if a concrete execution τ of the original program
can be constructed from π .
To validate a counterexample π , we define a concrete execution of a multi-threaded program as
follows.

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:10

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang
Table 1. Notations for a counterexample π

Notation
s 0, π
Tπ
Eπ
e 1 ≺π e 2
e 1 ≺π0 e 2
e 1 π e 2

Meaning
The initial states of π .
The set of statements contained in π
The set of events occurring in π .
e 1 should happen before e 2 in π .
e 1 ≺π e 2 according to the program order.
e 2 reads the value written by e 1 .
t

Definition 4.3. Let s 0 be an initial state of P, Λ := t 0 · · · tn be a statement sequence, and s → s 0
indicate that s 0 is the successor of s by t. The tuple (s 0 , Λ) defines a concrete execution of P iff there
ti

exists a state sequence s 0 · · · sn+1 s.t. si → si+1 for all 0 ≤ i ≤ n.
According to Definition 4.3, to validate a counterexample π , one should find a statement sequence
of Tπ that defines a concrete execution. Note that for a concrete execution τ , the events occurring
in τ must satisfy the following order requirements: 1) for each program order (e 1 , e 2 ), we have e 1
happens before e 2 ; and 2) for each read-write link (e 1 , e 2 ), we have e 1 happens before e 2 , and no
write of var(e 1 ) happens between e 1 and e 2 . Given that those local statements do not affect other
threads, the crucial issue to construct a concrete execution is to find a total order < π over Eπ s.t.
< π obeys all the above order requirements. To address this problem, we introduce the event order
graph (EOG) notion to capture all order requirements of a counterexample.
Definition 4.4. Given a counterexample π , the event order graph (EOG) G π is a triple hEπ , ≺π0 , π i,
where the nodes are the events in Eπ , and the edges are the orders defined in ≺π0 and π . Each
node corresponds to either a “read” or a “write” of π , and each edge corresponds to either a program
order or a read-from order of π . For each edge corresponding to a program order (e 1 , e 2 ) ∈ ≺π0 , it
requires that clk(e 1 ) < clk(e 2 ); and for each edge corresponding to a read-from order (e 1 , e 2 ) ∈ π ,
it requires that clk(e 1 ) < clk(e 2 ) and ∀e 3 ∈ Eπ , ((var(e 3 ) = var(e 1 )) ∧ (type(e 3 ) = ww)) ⇒ (clk(e 3 ) <
clk(e 1 ) ∨ clk(e 2 ) < clk(e 3 )).
Definition 4.5. An EOG G π is feasible iff there exists a total order < π over Eπ s.t. < π obeys all
the order requirements defined in G π .
Theorem 4.6. A counterexample π is feasible iff the corresponding EOG G π is feasible.
Proof. Sufficiency. If π is feasible, then we can construct a concrete execution τ from π .
Suppose that the statement sequence of τ is Λ. We order all the events in Eπ as the execution
order of those corresponding global statements in Λ, and obtain a total order < π over Eπ , which is
consistent with ≺π0 and π . Therefore, G π is feasible.
Necessity. We try to construct a concrete execution τ from π . If G π is feasible, then there must
exist a total order < π over Eπ that is consistent with ≺π0 and π . To obtain a statement sequence
Λ of Tπ , we first order all the global statements in Tπ as the order of those corresponding events in
< π , and obtain a total order <д of all the global statements. Then we “place” the local statements in
Tπ into <д . Specifically, we first give a total order t 0 · · · tn of all local statements according to the
program order. Afterward, we insert the local statements into <д according to this order and obtain
a statement sequence Λ. For each local statement ti , suppose that among all its predecessors of
д
global statements (according to the program order), ti is lastly scheduled in <д , then ti is scheduled
д
д
д
after both ti−1 and ti . For instance, if ti−1 is scheduled before ti , then ti is scheduled after ti .
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification
1:11

(b)
(b)

(a)
(a)

(c)
(c)

Fig. 4. Three EOG examples

(a)
(a)

(b)
(b)

(c)
(c)

Fig. 5. Derived orders deduced by applying Rule 2 to the three EOGs shown in Fig. 4.

Otherwise, ti is scheduled after ti−1 . Given that < π is both consistent with ≺π0 and π , the tuple
(s 0, π , Λ) is a concrete execution. Therefore, π is feasible.

Now we ask, how can we validate the feasibility of an EOG? An intuitive way is to exactly encode
all the order requirements defined in Definition 4.4 into a constraint. The EOG is feasible iff the
constraint is satisfiable. However, as we will justify later (cf. Section 5 and 7), constraint solving is
not effective enough for refinement generation.
4.2

Graph-Based EOG Validation

According to Definition 4.5, any edge (e 1 , e 2 ) of an EOG G π requires that e 1 ≺π e 2 . Hence, an
EOG must be infeasible if it contains some cycles. Note that a read-from order (e 1 , e 2 ) ∈ π
further requires that no other write of var(e 1 ) could happen between e 1 and e 2 . Some implicit order
requirements deducible from the EOG must exist. We call them derived orders of the EOG. For each
derived order (e 1 , e 2 ), it also requires that clk(e 1 ) < clk(e 2 ), i.e., e 1 ≺π e 2 .
Consider the EOG shown in Fig. 4(a), where {e x 0 , e x 2 } and {e x 1 } are the “writes” and “reads” of x,
respectively. e x 0 ≺π0 e x 1 , and e x 2 π e x 1 . We deduce that e x 0 ≺π e x 2 because e x 0 ≺π0 e x 1 and e x 2 π e x 1 ,
of which the latter implies that no “write” of x can happen between e x 2 and e x 1 .
Based on this observation, we can deduce as many derived orders as possible first, and add them
to ≺π . If some cycle exists in ≺π , then the EOG must be infeasible. To this end, we propose the
following three rules to produce derived orders. We initially obtain ≺π := ≺π0 ∪ π .
Rule 1.

e 1 ≺π e 2 , e 2 ≺π e 3
.
e 1 ≺π e 3

Rule 1 only reflects the transitivity of ≺π .
Rule 2.

e 1 π e 2 , e 3 ≺π e 2 , type(e 3 ) = ww, var(e 3 ) = var(e 1 )
.
e 3 ≺π e 1

Given that e 1 π e 2 , type(e 3 ) = ww, and var(e 3 ) = var(e 2 ), then either clk(e 3 ) < clk(e 1 ) or clk(e 2 ) <
clk(e 3 ). Given that e 3 ≺π e 2 holds, then clk(e 3 ) < clk(e 2 ) can be obtained. Therefore, we have
clk(e 3 ) < clk(e 1 ), which implies e 3 ≺π e 1 .
Similarly, we propose the following deductive rule:
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:12

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang
P0

P1

w1

w2

m1

n1

x1

P2
x2

P3
y2

w3

w4

y3

x3

n2

m2

P5

P4
n3

y1

w5

m3

w6

Fig. 6. The “butterfly” example

Rule 3.

e 1 π e 2 , e 1 ≺π e 3 , type(e 3 ) = ww, var(e 3 ) = var(e 1 )
.
e 2 ≺π e 3

According to these three rules, for the three EOGs presented in Fig. 4, we can deduce e x 0 ≺π e x 2 ,
e x 0 ≺π e x 3 , and e x 0 ≺π e x 2 , respectively. We add these terms to the corresponding EOGs as shown
in Fig. 5.
When a derived order (e 1 , e 2 ) is added to ≺π , some new orders may be propagated via Rules 1 to
3. We repeat this process until we reach a fixpoint, i.e., no derived order can be deduced any more.
If some cycle exists in ≺π , then the EOG is infeasible.
Now a conjecture is that, an EOG is feasible if it contains no cycle. Such a conjecture holds for
almost all examples in our experiments. However, this conjecture may still be false for some special
examples. Consider the “butterfly” example in Fig. 6 that involves six threads {P 0 , P 1 , · · · , P 5 } and
five shared variables {m, n, x, y, w }. No derived order can be deduced, and no cycle exists in the
EOG. However, no total order of Eπ can satisfy all the order requirements defined in the EOG, and
the EOG is infeasible.
Our graph-based EOG validation method is shown in Algorithm 1. It repeatedly applies Rules 1
to 3 to deduce new derived orders, until a fixpoint is reached. If there exists some conflict event e
s.t. e ≺π e, then the EOG must be infeasible. Otherwise, it is not sure whether the EOG is feasible
or not.
We now prove the correctness of this algorithm.
Theorem 4.7. If Algorithm 1 concludes that G π is infeasible, then G π must be infeasible.
Proof. If Algorithm 1 concludes that G π is infeasible, then there must exist some conflict event
e s.t. e ≺π e. Suppose that G π is feasible. Then according to Definition 4.5, there must exist a total
order < π s.t. < π obeys all order requirements defined in G π . According to Rules 1 to 3, we have
< π also obeys all the derived orders deduced in Algorithm 1. Hence, clk(e) < clk(e) in < π , which
is impossible for a total order.
Therefore, the theorem is proved.

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification
1:13
Input: An EOG G π = hEπ , ≺π0 , π i
Output: Infeasible: G π is infeasible; Not-Sure: not sure whether G π is feasible or not
repeat
if there exist (e 1 , e 2 ), (e 2 , e 3 ) ∈≺π and (e 1 , e 3 ) <≺π then
≺π =≺π ∪(e 1 , e 3 );
end
if there exists (e 1 , e 2 ) ∈ π exists (e 3 , e 2 ) ∈≺π and (e 3 , e 1 ) <≺π then
if type(e 3 ) = ww and var(e 3 ) = var(e 1 ) then
≺π :=≺π ∪(e 3 , e 1 );
end
end
if there exists (e 1 , e 2 ) ∈ π exists (e 1 , e 3 ) ∈≺π and (e 2 , e 3 ) <≺π then
if type(e 3 ) = ww and var(e 3 ) = var(e 1 ) then
≺π :=≺π ∪(e 2 , e 3 );
end
end
until ≺π reaches a fixpoint;
if e ≺π e for some e then
return Infeasible;
end
return Not-Sure;
Algorithm 1: Graph-based EOG validation
4.3

Constraint-Based EOG Validation

If the graph-based EOG validation method is not sure whether an EOG is feasible or not, we employ
a constraint solver to further determine feasibility of the EOG. The method is that, we exactly
encode all the order requirements defined in Definition 4.4 into a constraint. The EOG is feasible iff
the constraint is satisfiable. If a SAT is returned, then it generates a total order of all the events
which satisfies all the order requirements of the EOG as a byproduct. Otherwise, both the EOG and
the counterexample are infeasible and an unsatisfiable core is generated as a byproduct.
5

KERNEL REASON BASED REFINEMENT GENERATION

If a counterexample is determined to be infeasible, one should add some constraints to the abstraction
to prevent this counterexample from appearing again in the future search. The most intuitive way
to address this problem is to add the negation of this counterexample to the abstraction. However,
such a manner excludes only one counterexample in each refinement. To prune more search space,
a better idea is to analyze the kernel reasons that make the counterexample infeasible, and then
adds the negation of these kernel reasons to the next abstraction. Given that a counterexample is
validated via validating its corresponding EOG, we analyze the kernel reasons that make an EOG
infeasible, s.t. a large amount of space can be pruned in each refinement iteration.
5.1

Representation of Kernel Reasons

Given a counterexample π , the corresponding EOG G π := hEπ , ≺π0 , π i is determined by the values
of the following two kinds of literals: 1) The values of those guard condition literals for the events
in E. They determine both Eπ and ≺π0 . Eπ is the set of events appeared in π . ≺π0 is the restriction of
≺P0 to Eπ . 2) The values of those read-write link literals which define the read-from relationship π .
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:14

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang

Let Gπ and Sπ denote the sets of true guard condition literals and true read-write link literals in
π , respectively. If G π is infeasible, then the infeasibility could be deduced by the conjunction of
all literals in Gπ ∪ Sπ . The infeasibility can often be deduced by a subset of Gπ ∪ Sπ . Therefore,
the kernel reasons that make a counterexample π infeasible could be represented by the minimal
subsets of Gπ ∪ Sπ that could deduce the infeasibility. Finding the minimal subsets not only reduces
the constraint size but also prunes more search space.
5.2

Constraint-Based Kernel Reason Analysis

If the infeasibility is identified by the constraint-based EOG validation process, the constraint solver
can return an unsatisfiable core as a byproduct. Modern constraint solvers, such as MiniSat2, allow
their users to take a set of literals as assumptions. When an UNSAT is returned, the constraint
solver generates a subset of the assumption literals as an unsatisfiable core. Based on this idea,
we take all literals in Gπ ∪ Sπ as assumption literals. Whenever the EOG is determined to be
infeasible, the constraint solver generates a subset of Gπ ∪ Sπ that can still deduce the infeasibility.
Suppose that it is {`1 , `2 , · · · , `n }. Let ϖ := `1 ∧ `2 ∧ · · · ∧ `n . The refinement constraint can then
be formulated as follows.
κ := ¬ϖ

(2)

If the constraint that exactly encodes all order requirements of an EOG is unsatisfiable, it may
have a large number of unsatisfiable cores. To prune as much search space as possible, one should
obtain all of them. However, generating all unsatisfiable cores is usually time consuming. Most
constraint solvers generate only one unsatisfiable core each time, and it may not be the shortest one,
which significantly limits the pruned search space in each refinement. Hence, constraint solving is
not a good choice for our refinement generation.
5.3

Graph-Based Kernel Reason Analysis

This section presents our graph-based kernel reason analysis method. Compared with the constraintbased method, it usually obtains a much more effective refinement. It can efficiently obtain all
kernel reasons that make an EOG infeasible. In addition, the obtained “core kernel reasons” are
always the shortest ones. Hence, it can usually prune much more search space in each iteration.
In Algorithm 1, if an infeasibility is determined, then there must exist some conflict event e s.t.
e ≺π e. A conflict event can usually be attributed to several kernel reasons, and there are usually
many conflict events. To prune more search space, one should find all kernel reasons of all conflict
events.
We define “a kernel reason of an order λ ∈≺π ” to be “the minimal subset of Gπ ∪ Sπ that
can deduce λ”. When a derived order λ is deduced, if the kernel reasons of all existing orders
(including existing derived orders) are given, then we can obtain a set of kernel reasons of λ upon
its production. Note that a derived order λ may be deduced for multiple times. Whenever it is
deduced, we can obtain new kernel reasons of λ. Based on this observation, we initialize the kernel
reasons of every order λ to ∅. The kernel reasons of an order λ are then updated once λ is added
(we add the orders in ≺π0 and π into the graph one by one) or deduced. In this manner, we obtain
the kernel reasons of each order λ ∈≺π when Algorithm 1 terminates.
We then discuss how to update the kernel reasons of an order λ ∈≺π when λ is added or deduced.
We hypothesize that the kernel reasons of all existing orders are given. We denote by o(λ) and O(λ)
a kernel reason and the set of kernel reasons of λ, respectively.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification
1:15
• If λ := (e 1 , e 2 ) is added because λ ∈ ≺π0 , then e 1 ≺π e 2 iff both e 1 , e 2 ∈ Eπ , i.e., the guard condition literals for both e 1 and e 2 are true. Therefore, O(λ) := O(λ)∪ {{guard(e 1 ), guard(e 2 )}},
where guard(e) is the guard condition literal of e.
• If λ := (e 1 , e 2 ) is added because λ ∈ π , λ holds iff e 2 reads the value written by e 1 ,
which already indicates that both guard(e 1 ) and guard(e 2 ) are true. Therefore, O(λ) :=
O(λ) ∪ {{sel(λ)}}, where sel(λ) is the read-write link literal of λ.
• If λ is a derived order deduced from λ 1 and λ 2 , then λ ∈≺π iff both λ 1 and λ 2 belong to ≺π .
Therefore, O(λ) := O(λ) ∪ {o 1 ∪ o 2 | oi ∈ O(λi )}. Note that λ may be deduced for multiple
times. We incrementally update O(λ) whenever λ is deduced.
A kernel reason o ∈ O(λ) is considered redundant if some kernel reason o 0 ∈ O(λ) exists s.t.
⊆ o. Such kernel reasons are immediately eliminated from O(λ), and the remaining reasons are
called core kernel reasons of λ. Using this strategy, we maintain only the set of core kernel reasons
in our algorithm. This set is dynamically updated during the running of the algorithm.
In this manner, we obtain the set of core kernel reasons of any order λ ∈≺π when Algorithm 1
terminates. Let A denote the set of conflict events. The kernel reasons that make π infeasible
(denoted by O(π )) can be expressed as follows.

o0

Ø

O(π ) :=

O(e ≺π e)

(3)

e ∈A

Again, we eliminate those redundant kernel reasons from O(π ), and maintain only those core
kernel reasons. In our experiments, hundreds or even thousands of kernel reasons may be observed,
but only several or dozens of them are considered core ones.
Suppose that o := {`1 , `2 , · · · , `m } where each `i is a literal, we define the following:
ϖ o := `1 ∧ `2 ∧ · · · ∧ `m

(4)

Suppose that O(π ) := {o 1 , o 2 , · · · , on }, then the refinement constraint is formulated as follows.
κ :=

n
Û

¬ϖ oi

(5)

i=1

Algorithm 2 demonstrates our graph-based refinement generation method. We first add all the
program orders into ≺π , and update their kernel reasons according to the kernel reason updating
method we have discussed. Adding a read-from order or a derived order to ≺π may propagate a
large number of new orders. Whenever a read-from order λ ∈ π is added to ≺π , we denote by D
the set of orders that will be added to ≺π before another read-from order is added. Adding each
order λ 0 ∈ D to ≺π may propagate a set of derived orders, which are denoted by B. Whenever an
order λ 00 ∈ B is deduced, we update its kernel reasons and add it to D if it is not contained in ≺π .
In this manner, once all read-from orders have been added to ≺π , we obtain all derived orders and
the kernel reasons of all orders in ≺π . We then compute the refinement constraint according to
equation (3), (4) and (5).
From the above discussion, the graph-based refinement generation method has the following
advantages:
(1) It can detect all kernel reasons that make π infeasible, leading to a large amount of search
space pruned in each iteration.
(2) It maintains a minimal subset of core kernel reasons, thereby making the refinement
constraint small and manageable.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:16

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang

Input: An EOG G π := hEπ , ≺π0 , π i.
Output: A refinement constraint κ.
≺π := ≺π0 , and update O(λ) for each λ ∈ ≺π0 ;
foreach λ ∈ π do
Update O(λ), and let D := {λ};
foreach λ 0 ∈ D do
≺π :=≺π ∪{λ 0 };
Let B be the set of propagated orders due to λ 0;
foreach λ 00 ∈ B do
Update O(λ 00);
if λ 00 <≺π then
D := D ∪ {λ 00 };
end
end
end
end
Compute κ according to equation (3), (4) and (5);
return κ;
Algorithm 2: Graph-based refinement generation.

5.4

Correctness of the Graph-Based Kernel Reason Analysis

We prove the correctness of our graph-based refinement generation method, that is, the refinement
constraint obtained in equation (5) should be true in any feasible counterexample, i.e., it will not
eliminate any feasible counterexample from the abstraction.
Theorem 5.1. Given a counterexample π and a kernel reason o(λ) obtained according to our graphbased kernel reason analysis method, we have o(λ) |= λ. That is, for any other counterexample π 0, we
also have λ ∈≺π 0 if π 0 |= ϖ o(λ) .
Proof. We prove this theorem by induction.
Inductive Base: If o(λ) is obtained because λ ∈ ≺π0 or λ ∈ π , then the conclusion can be
immediately inferred from the definition.
Inductive Step: If o(λ) is obtained via Rule 1, 2, or 3, then two orders λ 1 and λ 2 must exist, such
that o(λ) = o(λ 1 ) ∪ o(λ 2 ). Given that ϖ o(λ) holds w.r.t. π 0, ϖ o(λ1 ) and ϖ o(λ2 ) are also true w.r.t. π 0. By
applying the induction hypothesis, we obtain λ 1 , λ 2 ∈≺π 0 . According to the same rule, we deduce
that λ ∈≺π 0 .

Theorem 5.2. Given a kernel reason o ∈ O(π ) of an infeasible counterexample π , for any feasible
counterexample π 0, we have π 0 |= ¬ϖ o .
Proof. Given that o is a kernel reason that makes π infeasible, according to equation (3), there
must exist a corresponding order λ := (e, e) ∈≺π . Suppose that π 0 |= ϖ o . Then according to
Theorem 5.1, we have λ := (e, e) ∈≺π 0 . It indicates that π 0 is infeasible, which is contradict with
that π 0 is feasible. Hence, we must have π 0 |= ¬ϖ o .

Theorem 5.3. Given a refinement constraint κ obtained in some iteration, for any feasible counterexample π 0, we have π 0 |= κ.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification
1:17
Ó
Proof. Suppose that κ := ni=1 ¬ϖ oi , and the corresponding counterexample is π . According to
Theorem 5.2, for any i (1 ≤ i ≤ n), we have π 0 |= ¬ϖ oi . Hence, π 0 |= κ.

6

SOUNDNESS AND EFFICIENCY

6.1

Soundness and Completeness

We prove the soundness and completeness of our method (shown in Fig. 1) via three theorems.
Theorem 6.1. If our method concludes that the property is safe, then it must be safe w.r.t. the given
loop unwinding depth.
Proof. To prove this theorem, we prove that α ∧ ϕ er r |= φ 0 ∧ ∧ni=0κi ∧ ϕ er r , where α is the
monolithic encoding, φ 0 is the initial abstraction, κi is the i-th refinement constraint, and ϕ er r
is the error states. According to the definition of α and φ 0 (cf. Definition 3.1), we can obtain
α ∧ ϕ er r |= φ 0 ∧ ϕ er r . We prove that α ∧ ϕ er r |= κi as follows.
If κi is obtained from the graph-based refinement process, we prove that for each element
¬ϖ ∈ κi , α ∧ ϕ er r |= ¬ϖ. Suppose that α ∧ ϕ er r 2 ¬ϖ. Then there must exist an assignment π of
α ∧ ϕ er r s.t. ϖ holds. Given that π is a feasible counterexample, according to Theorem 5.2, π |= ¬ϖ,
which is contradict with that ϖ holds in π . Hence, we must have α ∧ ϕ er r |= ¬ϖ and α ∧ ϕ er r |= κi .
If κi is obtained from the constraint-based refinement process, then κi = ¬ϖ where ϖ is an
unsatisfiable core of the formula which encodes all order requirements of an EOG. Suppose that
α ∧ ϕ er r 2 ¬ϖ. Then there must exist an assignment π of α ∧ ϕ er r s.t. ϖ holds, which is contradict
with that ϖ is an unsatisfiable core. Hence, we must have α ∧ ϕ er r |= κi .

Theorem 6.2. If our method concludes that the property is unsafe, then a true counterexample of
the property must exist.
Proof. In our method, the property is concluded unsafe only if the constraint-based EOG
validation process returns SAT. Given that the formula in the constraint-based EOG validation
process encodes all order requirements of the EOG exactly, according to Definition 4.4 and 4.5, the
EOG is feasible iff the formula is satisfiable. Hence, the EOG is feasible. According to Theorem 4.6,
the corresponding counterexample must be feasible. Therefore, a true counterexample of the
property must exist.

Theorem 6.3. Our method will terminate for any program with finite state space.
Proof. For a multi-threaded program with finite state space, the number of counterexamples of
the initial abstraction must be finite. Suppose that the counterexample obtained in the i-th iteration
is πi . According to Section 5, each kernel reason of the counterexample or the unsatisfiable core
obtained in the constraint-based refinement process is just a subset of Gπi ∪ Sπi . According to
equation (5) and (2), we have πi must be absent in the next abstraction. Hence, our method reduces
at least one counterexample in each iteration. It terminates when all counterexamples have been
reduced or a true counterexample is found.

6.2

Efficiency

A both efficient and sound way for counterexample validation and refinement generation will be
elegant. However, such procedure is usually difficult to devise. As an alternative, we integrate the
graph-analysis and constraint solving approaches together to obtain a both efficient and sound
method.
We have proved that enhanced by the constraint-based counterexample validation and refinement
generation processes, our method is sound and complete. We now analyze the effectiveness of the
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:18

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang

graph-based EOG validation method. If the EOG is infeasible, the infeasibility may be determined
by either the graph-based EOG validation process or the constraint-based EOG validation process.
Although both of these processes can rapidly determine such infeasibility, a much more effective
refinement can be obtained if the infeasibility is determined from the graph-based EOG validation
process. Fortunately, cases similar to the “butterfly” example rarely occur in practice. In other
words, the graph-based EOG validation process can always identify the infeasibility with rare
exceptions.
Suppose that the verification problem is solved via n iterations. If the property is determined
to be unsafe, then all EOGs generated during the first n − 1 rounds must be infeasible, which can
generally be identified by the graph-based EOG validation process. The constraint-based EOG
validation process is only invoked in the last iteration during which the property is violated. If the
property is proved safe w.r.t. the given loop unwinding depth, then the infeasibility of all the n
infeasible EOGs can generally be identified by the graph-based EOG validation process, and the
constraint-based EOG validation process will not be invoked.
In sum, advantages of our method include: 1) Without the scheduling constraint, the initial
abstraction φ 0 is usually much smaller than the monolithic encoding. 2) The graph-based refinement
process can usually obtain a small yet effective refinement, which reduces a large amount of space in
each iteration whereas the size of all those refinement constraints can usually be ignored compared
with that of the abstraction. 3) Though the graph-based validation process is not complete, it is
effective to identify the infeasibility in practice.
7

EXPERIMENTAL RESULTS

We have implemented our method on top of CBMC-4.9 3 and employed MiniSat2 as the back-end
constraint solver. Our tool is named Yogar-CBMC, and it is available at [36]. We use the 1047
multi-threaded programs of SV-COMP 2017 [36] as our benchmarks. In the experiments, our tool
supports nearly all features of C language and PThreads.
7.1

Benchmark of SV-COMP 2017

The open-source, representative, and reproducible benchmarks of Competition on Software Verification (SV-COMP) have been widely accepted for program verification. Given that these benchmarks
are devised for comparison of those state-of-the-art techniques and tools, a significant number of
studies on concurrent program verification have performed their experiments on them.
The concurrency benchmarks of SV-COMP 2017 include 1047 examples and cover most of the
publicly available concurrent C programs that are used for verification. Though many of these
examples are small in size in previous years, dozens of complex examples have been added to
these benchmarks in recent years. For instance, the examples in the pthread-complex directory (collected by the CSeq team) are taken from the papers on PLDI15 [28], POPL15 [8], and
PPOPP14 [37], which are used for concurrent program debugging and testing; the examples in the
pthread-driver-races directory (collected by the SMACK+CORRAL team) are used for symbolic
analysis of the drivers from the Linux 4.0 kernel [13]; and the examples in the pthread-C-DAC
directory (collected by C-DAC) are from the industrial problems of Centre for Development of Advanced Computing, Pune, India. These programs contain hundreds of lines, 4 to 8 threads, complex
structure variables with 2D pointers, and hundreds or even a thousand read/write accesses 4 . Given

3 Downloaded

from https://github.com/diffblue/cbmc/releases on Nov 20, 2015
read/write access of a complex structure variable may contain hundreds of read/write accesses of boolean variables.
Here a read/write access of a complex structure variable is considered just one read/write access.

4A

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification
1:19
these complex features, these programs are challenging for existing state-of-the-art concurrency
verification techniques and tools.
7.2

Experimental Setup

We conduct all of our experiments using a computer with Intel(R) Core(TM) i5-4210M CPU 2.60
GHz and 12 GB memory. A 900-second time limit is observed.
We select and compare two classes of the state-of-the-art tools with our method. The first class
is those top winners in recent competitions, including MU-CSeq5 [39] and Lazy-CSeq-Abs5 [30].
MU-CSeq is the gold medal winner of SV-COMP 2016, and Lazy-CSeq-Abs is the silver medal
winner of SV-COMP 2017. The second class comprises those tools which methods are closely related
to ours, including CBMC [3] and Threader6 [31]. CBMC is a highly popular verifier for program
verification. Different from our method, it provides an exact encoding of the scheduling constraint
for multi-threaded program verification. For Threader, to the best of our knowledge, it is the
best CEGAR-based verifier for multi-threaded C programs. It has received the gold medal of the
concurrency track of SV-COMP 2013.
Given that different tools employ different techniques, each of which has its own features, it
is difficult to make the comparison absolutely fair. For example, Threader performs unbounded
verification, while all the other tools perform BMC; and given a loop unwinding depth, both MUCSeq and Lazy-CSeq-Abs are incomplete whereas all the other tools are complete. To make the
comparison as fair as possible, we select the latest available version of them, and set the parameters
of them to be that of the competition. We believe that these tools should perform best under
these parameters. For the loop unwinding depth, we set that of CBMC and Yogar-CBMC the
same as that of MU-CSeq. Specifically, it is dynamically determined through syntax analysis. The
bound is set to 2 for programs with arrays, and n if some of the program’s for-loops are upper
bounded by a constant n [39]. Given that our method is implemented on top of CBMC. The only
difference between CBMC and Yogar-CBMC is that CBMC employs the monolithic encoding while
we perform our abstraction refinement on the scheduling constraint.
7.3

Effectiveness and Efficiency

Yogar-CBMC solved7 all the 1047 concurrent programs and has received the highest score of 1293
points. It has won the gold medal in the concurrency track of SV-COMP 2017 [36] (Warning: It will
violate our anonymity).
Overall comparison with state-of-the-art tools. Fig. 7 compares our tool with the state-of-the-art
tools, including MU-CSeq, Lazy-CSeq-Abs, and CBMC. Similar to SV-COMP 2017, we perform our
experiments on BenchExec 8 to achieve a reliable and repeatable benchmarking.
The experimental results for Lazy-CSeq-Abs and MU-CSeq are consistent with those in SVCOMP 2017. However, the results in our experiments for CBMC is better than those in SV-COMP
2017. The reason is that we have improved CBMC in several aspects, and we have also realized
some concurrency-related improvements in CBMC-5.5 9 .
Fig. 7(a) compares the overall performance of Lazy-CSeq-Abs, MU-CSeq, CBMC, and YogarCBMC based on the SV-COMP rules. The x-axis represents the accumulated score, while the y-axis
5 Downloaded

from http://sv-comp.sosy-lab.org/2017/systems.php on January 24, 2017
from http://sv-comp.sosy-lab.org/2014/participants.php on January 24, 2017
7 Solve means that the verifier gives a correct answer (true/false) within the time limit. Refer to [36] for the rules of the
competition.
8 https://github.com/sosy-lab/benchexec
9 Released on August 20, 2016 in https://github.com/diffblue/cbmc/releases
6 Downloaded

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:20

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang
sec.

MB

1000
Lazy‐CSeq‐Abs

Lazy‐CSeq‐Abs
1000

MU‐CSeq

MU‐CSeq

CBMC

CBMC

Our tool

Our tool

Memory in MB

Time in second

100

10

100

1

0.1

10

0

200

400

600

800

1000

1200

Accumulated score

(a) Time comparison

0

200

400

600

800

1000

Accumulated solved examples

(b) Memory comparison

Fig. 7. Compare with state-of-the-art tools

represents the time needed to achieve a certain score 10 . Both our tool and Lazy-CSeq-Abs have
successfully solved all examples and obtained 1293 points, while MU-CSeq and CBMC obtained
1243 and 1258 points, respectively. Lazy-CSeq-Abs, MU-CSeq, and CBMC spent 9820, 2540, and
12300 s to finish all examples, respectively, while our tool completed all examples within 1550 s.
Fig. 7(b) shows the overall memory consumption of the aforementioned tools. Lazy-CSeq-Abs,
MU-CSeq, CBMC, and Yogar-CBMC require 104, 103, 84 and 43 GB to solve all 1047 examples,
respectively. Given that the scheduling constraint is ignored in the abstraction, our tool always
solves small problems and consumes much less memory than the three other tools.
We further compare our tool with Lazy-CSeq-Abs, MU-CSeq, CBMC, and Threader to evaluate
its performance.
Yogar-CBMC versus Lazy-CSeq-Abs. Compared with Lazy-CSeq-Abs, our tool runs 6.34 times
faster on average, and consumes only 41% of the memory over all 1047 examples. As shown
in Fig. 8(a), Lazy-CSeq-Abs outperforms our tool in only 12 of the 1047 examples. With its
abstract interpretation technique, Lazy-CSeq-Abs outperforms our tool in those examples where
the numerical analysis dominates the complexity.
Yogar-CBMC versus MU-CSeq. MU-CSeq fails to solve 30 of the 1047 examples. Compared with
this tool, our tool runs 2.43 times faster on average and consumes only 36% of the memory for the
remaining 1017 examples. As shown in Fig. 8(b), MU-CSeq outperforms our tool in only 33 of the
1047 examples. By applying the memory unwinding technique to limit the number of writes, the
encoding size of MU-CSeq is insensitive to the scale of the data structures, thereby outperforming
our tool for some special examples.
Yogar-CBMC versus CBMC. Fig. 9(a) compares CBMC with our tool. CBMC fails to solve 23 of
the 1047 examples. Both CBMC and our tool can easily solve 92% of these examples. For these trivial
examples, the monolithic encoding may sometimes run faster. However, our tool outperforms
CBMC by 35.8 times on average in the 56 complex cases in which CBMC needs more than two
seconds to solve them.
10 The

rules to assign the score can be found in http://sv-comp.sosy-lab.org/2017/rules.php

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification
1:21
sec.

sec.

100

100

MU‐CSeq

1000

Lazy‐CSeq‐Abs

1000

10

10

1

1

sec.

0.1
0.1

1

10

100

sec.

0.1

1000

0.1

Our tool

(a) Our tool versus Lazy-CSeq-Abs

1

10

Our tool

100

1000

(b) Our tool versus MU-CSeq

Fig. 8. Compare with Lazy-CSeq-Abs and MU-CSeq

sec.

100

100

Threader

1000

CBMC

1000

10

10

1

1

sec.

0.1
0.1

1

10

Our tool

100

(a) Our tool versus CBMC

1000

0.1
0.1

1

10

100

1000

Our tool

(b) Our tool versus Threader

Fig. 9. Compare with CBMC and Threader

Yogar-CBMC versus Threader. Threader only participated in SV-COMP 2013 and 2014. Given
that this tool cannot solve many of the examples in SV-COMP 2017, we compare it with our tool on
the benchmarks of SV-COMP 2014, which contain only 78 examples. Fig. 9(b) presents the results.
Our tool has completed all 78 examples within the time limit, while Threader completed only
59 examples. Moreover, our tool and Threader require 140 s and 6865 s to solve these examples
respectively, thereby showing that our tool is 49 times faster than Threader on average. However,
as we have declared before, Threader performs unbounded verification, while we perform BMC.
7.4

Essence Analysis

The performance of our tool is mainly affected by the number of refinements, size of constraints
and cost of constraint solving, etc. We also justify the benefits from the graph-based refinement
generation method.
Number of refinements. Fig. 10(a) presents the number of refinements of our tool in the experiments. The point (50, 644) indicates that 644 examples can be solved in less than 50 refinements.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:22

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang
1000

800

100

SAT‐CEGAR

Number of examples

1000

600
400

10

1

200

0.1

0

0

50

100

150

200

Number of refinements

(a) Number of refinements

250

0.1

1

10

100

1000

Our tool

(b) Our tool versus SAT-CEGAR

Fig. 10. Number of refinements and benefits from EOG

Fig. 10(a) shows that most of the examples can be solved in less than 80 refinements. In our method,
we successfully decomposed the complex verification problem into dozens of small problems.
Size of refinements. Our experimental results reveal that without the scheduling constraint, the
formula size reduces to 1/8 on average and to 1/1200 in the extreme case, thereby allowing for the
abstractions to be solved quickly. However, the number of clauses increased during the refinement
process can usually be ignored. Most of the examples in our experiments show hundreds or even
thousands of increase in the number of CNF clauses during the refinements. However, the CNF
clause number of the abstraction may reach millions.
Cost of constraint solving. Without the scheduling constraint, the abstractions can usually be
solved instantly. Meanwhile, the graph-based EOG validation and refinement generation processes
are not trivial. We have observed that in our experiments, our tool has spent most of its time
on graph analysis for those examples where the scheduling constraint dominates the encoding.
Meanwhile, for those examples where the complexity mainly stems from the complex data structures
and numerical calculation, our tool has spent most of its time on constraint solving.
Efficiency benefit from the graph-based refinement generation. The efficiency of our method mainly
benefits from the graph-based refinement generation. We have implemented another scheduling
constraint based abstraction refinement method, SAT-CEGAR, which employs only constraint
solving for EOG validation and refinement generation. SAT-CEGAR has solved only 265 of the 1047
examples in the experiments. Fig. 10(b) compares the performance of our tool with SAT-CEGAR in
solving these examples. Our tool outperforms SAT-CEGAR for most examples, and runs 58 times
faster on average. On average, our tool finds 9.3 core kernel reasons in each refinement, with each
kernel reason having an average clause length of 3.06. Meanwhile, SAT-CEGAR only finds one
kernel reason in each refinement, with each reason having an average clause length of 7.5.
Exceptions where the graph-based EOG validation method fails. In our method, if the constraint
solving based refinement process is invoked and returns UNSAT, then we cannot achieve an
effective refinement. How often does this case occur in the experiments? Fortunately, we have not
observed cases similar to the “butterfly” example in our experiments, and the constraint solving
based refinement process has never been invoked.
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification
1:23
7.5

Threats to Validity

One threat to the validity is the limited benchmarks we have used. For those examples where the
scheduling constraint is not a major part of the encoding, our method may still need dozens of
refinements. Given that those abstractions may have similar size with the monolithic encoding,
our method may perform worse than the monolithic method.
Another threat to the validity is the tools we have used. Given that different technologies have
different advantages, it is difficult to give an absolute fair comparison. In some other scenarios, one
may prefer Threader and other tools.
The third threat to the validity is the parameters we have used for each tool. Most tools have
some parameters related with their techniques, such as the loop unwinding depth. Given that
different tools may have different parameters, it is difficult to compare all the tools under the same
parameters.
8

RELATED WORK

Addressing the control state explosion resulting from concurrency poses a significant challenge to
concurrent program verification. Several techniques have recently been studied to overcome this
problem, including stateless model checking [1, 4, 9, 24], compositional reasoning [14, 22, 29, 32],
bounded model checking [3, 10, 20, 25, 38, 43], and abstraction refinement [11, 12, 21, 29, 35], etc.
The general idea of stateless model checking is to employ partial order reduction (POR) or
dynamic partial order reduction (DPOR) [1, 4, 9, 41] to explore only non-redundant interleavings.
There are also some work which reduces the search space by restricting the schedules of the
program [5, 40]. In compositional reasoning, rather than considering all possible interleavings
of a program, the property is decomposed into different components. Each component is then
considered in isolation, without any knowledge of the precise concurrent context. Recent work on
compositional reasoning includes assume-guarantee reasoning [15, 16], rely-guarantee reasoning
[19, 22, 27], thread-modular reasoning [29], and compositional reasoning [14, 32], etc.
Our scheduling constraint based abstraction refinement method explores both bounded model
checking and abstraction refinement. Afterward, we compare our study with the recent work on
these two methods.
On Bounded Model Checking. Bounded model checking has been considered an efficient technique
to address the interleaving problem. In SV-COMP 2017, 16 out of the 18 participants in the
concurrency track have adopted this technique [6]. However, pure BMC is still not efficient enough.
Many existing tools combine this method with other techniques. ESBMC combines symbolic model
checking with explicit state space exploration [10]. VVT employs a CTIGAR method, an SMT-based
IC3 algorithm that incorporates CEGAR [20]. The interleaving problem can also be addressed by
translating the concurrent programs into sequential programs. Tools implementing this technique
include MU-CSeq [38], Lazy-CSeq-Abs [25], and SMACK[34], etc.
However, all of these work gives an exact encoding of the scheduling constraint, while we ignore
this constraint and employ a scheduling constraint based abstraction refinement method to obtain
a small yet effective abstraction w.r.t. the property.
On Abstraction Refinement. Abstraction refinement has been widely studied in concurrent program verification. Most of these work employs predicate abstraction to address the data space
explosion problem [11, 12, 21–23, 42]. In predicate abstraction, it uses a finite number of predicates
to abstract the program. If an abstraction counterexample is spurious, it finds predicates that add
more details of the program to refine the abstraction, s.t. the spurious counterexample is absent in
the latter abstraction models. To find the right set of predicates in less iterations, many heuristics
, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:24

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang

have been proposed. For example, Ashutosh Gupta and Thomas A. Henzinger et al. accelerated the
search for the right predicates by exploring the bad abstraction traces [21]. By contrast, we employ
abstraction refinement to address the control space explosion problem resulting from the thread
interleavings. Our abstraction and refinement methods are both different with that of predicate
abstraction.
The work most related to ours focuses on interference abstraction (IA) [35]. N. Sinha and C.
Wang also performed abstraction refinement to deal with the overhead of the exact encoding of
the concurrent behavior. However, they abstracted the behavior by restricting the sets of read
events and read-write links, while we consider all read events and read-write links but relax the
scheduling constraint. Accordingly, their abstraction was refined by introducing new read events
and read-write links, while we perform the refinement by exploring a graph-based method to
analyze core kernel reasons that make an counterexample infeasible. Moreover, they employ
a mixed framework of over- and under-approximations, while our method produces only overapproximation abstractions. Given that their implementation was for Java program slices, an
empirical comparision between their and our method is difficult.
Another work closely related to ours is [26]. In this work, M. Kusano and C. Wang also presented
a set of deduction rules to help determine the infeasibility of an interference combination. However,
our task is to determine the feasibility of a counterexample which contains a large number of
read-write links, and our main innovation is to devise a graph-based refinement generation method
to obtain an effective refinement constraint. In addition, our deduction rules are much simpler yet
stronger than theirs.
To deal with the interleaving problem, A. Farzan and Z. Kincaid also divided the verification
into data and control modules, and incorporated them into an abstraction refinement framework
[17, 18]. The difference is that in their work, the verification is reasoned by data-flow analysis, while
we represent the program by SSA statements and employ graph and constraint based EOG analysis
approaches to do the refinement. In addition, their work focuses on parameterized programs, while
we concentrate on multi-threaded programs based on PThreads.
9

CONCLUSIONS

This paper proposed a scheduling constraint based abstraction refinement method for multi-threaded
program verification. To obtain an effective refinement, we also devised two graph-based algorithms
for counterexample validation and refinement generation. Our experiment results on benchmarks
of SV-COMP 2017 show that our method is promising and significantly outperforms the existing
state-of-the-art tools. We plan to extend this technique to weak memory models, such as TSO, PSO,
POWER, in the future.
REFERENCES
[1] Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos F. Sagonas. 2014. Optimal dynamic partial
order reduction. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. 373–384.
[2] Sarita V. Adve and Kourosh Gharachorloo. 1996. Shared Memory Consistency Models: A Tutorial. IEEE Computer 29,
12 (1996), 66–76.
[3] Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial Orders for Efficient Bounded Model Checking of
Concurrent Software. In International Conference on Computer Aided Verification, CAV. 141–157.
[4] Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlı́cek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimı́r Still, and Jirı́
Weiser. 2013. DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. In International
Conference on Computer Aided Verification, CAV. 863–868.
[5] Tom Bergan, Luis Ceze, and Dan Grossman. 2013. Input-covering schedules for multithreaded programs. In ACM
SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA.
677–692.

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification
1:25
[6] Dirk Beyer. 2017. Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP
2017). In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS.
[7] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic Model Checking without
BDDs. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS. 193–207.
[8] Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. 2015. Tractable Refinement Checking for
Concurrent Objects. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. 651–662.
[9] Katherine E. Coons, Madan Musuvathi, and Kathryn S. McKinley. 2013. Bounded partial-order reduction. In ACM
SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA.
833–848.
[10] Lucas C. Cordeiro, Jeremy Morse, Denis Nicole, and Bernd Fischer. 2012. Context-Bounded Model Checking with
ESBMC 1.17 - (Competition Contribution). In International Conference on Tools and Algorithms for Construction and
Analysis of Systems, TACAS. 534–537.
[11] Andrei Marian Dan, Yuri Meshman, Martin T. Vechev, and Eran Yahav. 2013. Predicate Abstraction for Relaxed
Memory Models. In International Static Analysis Symposium, SAS. 84–104.
[12] Andrei Marian Dan, Yuri Meshman, Martin T. Vechev, and Eran Yahav. 2015. Effective Abstractions for Verification
under Relaxed Memory Models. In International Conference on Verification, Model Checking and Abstract Interpretation,
VMCAI. 449–466.
[13] Pantazis Deligiannis, Alastair F. Donaldson, and Zvonimir Rakamaric. 2015. Fast and Precise Symbolic Analysis of
Concurrency Bugs in Device Drivers (T). In 30th IEEE/ACM International Conference on Automated Software Engineering,
ASE 2015, Lincoln, NE, USA. 166–177.
[14] Thomas Dinsdale-Young, Lars Birkedal, Philippa Gardner, Matthew J. Parkinson, and Hongseok Yang. 2013. Views:
compositional reasoning for concurrent programs. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL. 287–300.
[15] Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, and Sharon Shoham. 2015. Automated Circular AssumeGuarantee Reasoning. In International Symposium on Formal Methods, FM. 23–39.
[16] Karam Abd Elkader, Orna Grumberg, Corina S. Pasareanu, and Sharon Shoham. 2016. Automated Circular AssumeGuarantee Reasoning with N-way Decomposition and Alphabet Refinement. In International Conference on Computer
Aided Verification, CAV. 329–351.
[17] Azadeh Farzan and Zachary Kincaid. 2012. Verification of parameterized concurrent programs by modular reasoning
about data and control. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. 297–308.
[18] Azadeh Farzan and Zachary Kincaid. 2013. Duet: Static Analysis for Unbounded Parallelism. In International Conference
on Computer Aided Verification, CAV. 191–196.
[19] Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis. 2015. Rely/Guarantee Reasoning for
Asynchronous Programs. In International Conference on Concurrency Theory, CONCUR. 483–496.
[20] Henning Günther, Alfons Laarman, and Georg Weissenbacher. 2016. Vienna Verification Tool: IC3 for Parallel Software
- (Competition Contribution). In International Conference on Tools and Algorithms for Construction and Analysis of
Systems, TACAS. 954–957.
[21] Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta, and Thorsten Tarrach. 2015. Succinct
Representation of Concurrent Trace Sets. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL. 433–444.
[22] Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. 2011. Predicate abstraction and refinement for verifying
multi-threaded programs. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL.
331–344.
[23] Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. 2011. Threader: A Constraint-Based Verifier for Multithreaded Programs. In International Conference on Computer Aided Verification, CAV. 412–417.
[24] Jeff Huang. 2015. Stateless model checking concurrent programs with maximal causality reduction. In ACM SIGPLAN
Conference on Programming Language Design and Implementation, PLDI. 165–174.
[25] Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2014. Bounded Model
Checking of Multi-threaded C Programs via Lazy Sequentialization. In International Conference on Computer Aided
Verification, CAV. 585–602.
[26] Markus Kusano and Chao Wang. 2016. Flow-sensitive composition of thread-modular abstract interpretation. In
Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle,
WA, USA, November 13-18. 799–809.
[27] Ori Lahav and Viktor Vafeiadis. 2015. Owicki-Gries Reasoning for Weak Memory Models. In International Colloquium
on Automata, Languages and Programming, ICALP. 311–323.
[28] Nuno Machado, Brandon Lucia, and Luı́s E. T. Rodrigues. 2015. Concurrency debugging with differential schedule
projections. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. 586–595.

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

1:26

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang

[29] Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. 2010. Thread-Modular Counterexample-Guided
Abstraction Refinement. In International Static Analysis Symposium, SAS. 356–372.
[30] Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2017. Lazy-CSeq 2.0: Combining
lazy sequentialization with abstract interpretation - (Competition Contribution). In International Conference on Tools
and Algorithms for Construction and Analysis of Systems, TACAS.
[31] Corneliu Popeea and Andrey Rybalchenko. 2013. Threader: A Verifier for Multi-threaded Programs - (Competition
Contribution). In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS.
633–636.
[32] Corneliu Popeea, Andrey Rybalchenko, and Andreas Wilhelm. 2014. Reduction for compositional verification of
multi-threaded programs. In Formal Methods in Computer-Aided Design, FMCAD. 187–194.
[33] Shaz Qadeer and Jakob Rehof. 2005. Context-Bounded Model Checking of Concurrent Software. In International
Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS. 93–107.
[34] Zvonimir Rakamaric and Michael Emmi. 2014. SMACK: Decoupling Source Language Details from Verifier Implementations. In Proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, Vienna, Austria,
July 18-22. 106–113.
[35] Nishant Sinha and Chao Wang. 2011. On interference abstractions. In ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, POPL. 423–434.
[36] SV-COMP. 2017. 2017 software verification competition. (Warning: It will violate our anonymity). http://sv-comp.
sosy-lab.org/2017/. (2017).
[37] Paul Thomson, Alastair F. Donaldson, and Adam Betts. 2014. Concurrency testing using schedule bounding: an
empirical study. In ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP. 15–28.
[38] Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2015. Verifying
Concurrent Programs by Memory Unwinding. In International Conference on Tools and Algorithms for Construction
and Analysis of Systems, TACAS. 551–565.
[39] Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2016.
MU-CSeq 0.4: Individual Memory Location Unwindings - (Competition Contribution). In International Conference on
Tools and Algorithms for Construction and Analysis of Systems, TACAS. 938–941.
[40] Jingyue Wu, Yang Tang, Gang Hu, Heming Cui, and Junfeng Yang. 2012. Sound and precise analysis of parallel programs
through schedule specialization. In ACM SIGPLAN Conference on Programming Language Design and Implementation,
PLDI. 205–216.
[41] Naling Zhang, Markus Kusano, and Chao Wang. 2015. Dynamic partial order reduction for relaxed memory models.
In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. 250–259.
[42] Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang. 2014. On abstraction refinement for program
analyses in Datalog. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. 27.
[43] Manchun Zheng, Michael S. Rogers, Ziqing Luo, Matthew B. Dwyer, and Stephen F. Siegel. 2015. CIVL: Formal
Verification of Parallel Programs. In International Conference on Automated Software Engineering, ASE. 830–835.

, Vol. 1, No. 1, Article 1. Publication date: January 2016.

