1 void dfsblue(s, tid )
2
s.color [tid ] := cyan;
3
for t ∈ succ(s) do
4
if t.color [tid ] = white ∧ ¬t.red then
5
dfsblue(t, tid );
6
if s.acc ∧ ¬s.red then
7
s.count := s.count + 1;
8
dfsred(s, tid );
9
s.color [tid ] := blue;
10 void pndfs(s, nthreads)
11
par tid = 0 to nthreads do
12
dfsblue(s, tid );
13
report no cycle;
14 void dfsred(s, tid )
15
s.pink [tid ] := true;
16
for t ∈ succ(s) do
17
if t.color [tid ] = cyan then
18
report cycle; exit all;
19
if ¬t.pink [tid ] ∧ ¬t.red then
20
dfsred(t, tid );
21
if s.acc then
22
s.count := s.count − 1;
23
await s.count = 0;
24
s.pink [tid ] := false, s.red := true;
Fig. 2: An implementation of parallel NDFS, where the red colours are shared.
cycles. Moreover, if multiple workers initiated dfsred from the same accepting
state s, they must now finish their red search simultaneously for the algorithm
to be correct. The await synchroniser on line 23 ensures this, by blocking thread
execution until s.count—the number of workers in dfsred(s, ·)—reaches 0.
The original correctness argument of Laarman et al. relies on a complicated
inductive invariant stating that not all accepting cycles can be missed due to
pruning. However, this invariant is unsuitable for use in a (semi-)automated
verifier. Section 3 discusses the verification of pndfs and provides a new invariant
on the red colours that allows its correctness to be proven mechanically. It also
discusses how our verification handles concurrency and thread synchronisation.
2.3 Concurrency Verification with VerCors
Before discussing the actual verification, let us first briefly introduce VerCors, an
automated program verifier for parallel programs. VerCors uses concurrent separation logic with permissions as its logical foundation. Its annotation language
contains fractional permission predicates of the form Perm(s, π), in the style of
Boyland [7], that capture the notion of ownership enforced by separation logic,
where s is a shared memory location (e.g., a class field) and π ∈ (0, 1] Q a fractional value. The fractional permissions denote access rights: if π = 1 it denotes
write access to s, whereas π < 1 denotes a read access to s. Sometimes Perm(s)
is written as shorthand for ∃π : Perm(s, π), to indicate some ownership of s.
Soundness of the underlying logic ensures that the total sum of permissions for
any shared memory location does not exceed 1, which implies data race freedom.
In addition to ownership predicates, the annotation language supports the ∗∗
connective, which is the separating conjunction of separation logic. The assertion
P ∗∗ Q expresses that the ownerships captured by P and Q are disjoint, e.g., it is
disallowed that both express write access to the same shared location. Ownership
252
W. Oortwijn et al.
2
s.color [tid ] := cyan;
3
for t ∈ succ(s) do
4
if t.color [tid ] = white ∧ ¬t.red then
5
dfsblue(t, tid );
6
if s.acc ∧ ¬s.red then
7
s.count := s.count + 1;
8
dfsred(s, tid );
9
s.color [tid ] := blue;
10 void pndfs(s, nthreads)
11
par tid = 0 to nthreads do
12
dfsblue(s, tid );
13
report no cycle;
14 void dfsred(s, tid )
15
s.pink [tid ] := true;
16
for t ∈ succ(s) do
17
if t.color [tid ] = cyan then
18
report cycle; exit all;
19
if ¬t.pink [tid ] ∧ ¬t.red then
20
dfsred(t, tid );
21
if s.acc then
22
s.count := s.count − 1;
23
await s.count = 0;
24
s.pink [tid ] := false, s.red := true;
Fig. 2: An implementation of parallel NDFS, where the red colours are shared.
cycles. Moreover, if multiple workers initiated dfsred from the same accepting
state s, they must now finish their red search simultaneously for the algorithm
to be correct. The await synchroniser on line 23 ensures this, by blocking thread
execution until s.count—the number of workers in dfsred(s, ·)—reaches 0.
The original correctness argument of Laarman et al. relies on a complicated
inductive invariant stating that not all accepting cycles can be missed due to
pruning. However, this invariant is unsuitable for use in a (semi-)automated
verifier. Section 3 discusses the verification of pndfs and provides a new invariant
on the red colours that allows its correctness to be proven mechanically. It also
discusses how our verification handles concurrency and thread synchronisation.
2.3 Concurrency Verification with VerCors
Before discussing the actual verification, let us first briefly introduce VerCors, an
automated program verifier for parallel programs. VerCors uses concurrent separation logic with permissions as its logical foundation. Its annotation language
contains fractional permission predicates of the form Perm(s, π), in the style of
Boyland [7], that capture the notion of ownership enforced by separation logic,
where s is a shared memory location (e.g., a class field) and π ∈ (0, 1] Q a fractional value. The fractional permissions denote access rights: if π = 1 it denotes
write access to s, whereas π < 1 denotes a read access to s. Sometimes Perm(s)
is written as shorthand for ∃π : Perm(s, π), to indicate some ownership of s.
Soundness of the underlying logic ensures that the total sum of permissions for
any shared memory location does not exceed 1, which implies data race freedom.
In addition to ownership predicates, the annotation language supports the ∗∗
connective, which is the separating conjunction of separation logic. The assertion
P ∗∗ Q expresses that the ownerships captured by P and Q are disjoint, e.g., it is
disallowed that both express write access to the same shared location. Ownership
252
W. Oortwijn et al.