1 context Perm(N ) ∗∗ Perm(nthreads) ∗∗ Perm(G) ∗∗ Perm(acc) ∗∗ Perm(abort,
1
2
);
2 context ∀tid , s : Perm(color [tid ][s],
1
2
) ∗∗ Perm(pink [tid ][s],
1
2
);
3 context ∀tid : Perm(exploringred [tid ],
1
2
) ∗∗ Perm(redroot[tid ],
1
2
);
4 context ∀tid : Perm(waiting[tid ],
1
2
);
5 context 0 ≤ sI < N;
6 requires ∀tid , s : ¬exploringred [tid ] ∧ color [tid ][s] = white ∧ ¬pink [tid ][s];
7 ensures \result ⇒ (∃a : acc[a] ∧ ExPath(sI , a, 1) ∧ ExPath(a, a, 2));
8 ensures (∃a : acc[a] ∧ ExPath(sI , a, 1) ∧ ExPath(a, a, 2)) ⇒ \result;
9 bool pndfs(sI )
10
par tid = 0 to nthreads
11
context Perm(N ) ∗∗ Perm(nthreads) ∗∗ Perm(G) ∗∗ Perm(acc);
12
context ∀s : Perm(color [tid ][s],
1
2
) ∗∗ Perm(pink [tid ][s],
1
2
);
13
context Perm(term[tid ],
1
2
) ∗∗ Perm(exploringred [tid ],
1
2
);
14
context Perm(redroot[tid ],
1
2
) ∗∗ Perm(waiting[tid ],
1
2
);
15
requires ¬exploringred [tid ] ∧ ∀s : color [tid ][s] = white ∧ ¬pink [tid ][s];
16
ensures ¬abort ⇒ ∀s : color [tid ][s] = cyan ∧ ¬pink [tid ][s];
17
ensures ¬abort ⇒ color [tid ][sI ] = blue;
18
do
19
bool found := dfsblue(sI , tid );
20
if found then
21
atomic { abort := true; } // initiate global termination.
22
atomic { if ¬abort then theorem one() }; // apply Thm. 1’s encoding.
23
return abort;
Fig. 6: The annotated version of pndfs, extending the excerpt given in Figure 3.
Correctness of pndfs. Figure 6 gives the annotated version of pndfs
6 that
extends the excerpt given earlier, in lines 23–25 of Figure 3. The main thread
requires partial ownership of all thread-local colour fields on line 2 and distributes
these over the appropriate threads on line 12. The contract associated to the
parallel block (lines 11–17) is called an iteration contract and assigns pre- and
postconditions to every parallel instance. For more details on iteration contracts
we refer to [5]. Most importantly, the iteration contract of each thread holds
enough resources to satisfy all the preconditions of dfsblue, on line 19.
Soundness of pndfs (line 7) is proven as follows. Suppose that all threads have
terminated and abort has been set to true. In that case, the resource invariant
states that an accepting cycle has been found. This information can be retrieved
by briefly obtaining the resource invariant in ghost code on line 22, which directly
allows to deduce soundness. Note that this information is not lost upon releasing
the resource invariant, as it is a Boolean property and thus duplicable.
To prove completeness, suppose that abort is still false when all workers have
terminated. This implies that Pink tid = ∅ and Cyan tid = ∅ for every worker tid
(line 16), as well as s I ∈ Blue tid (line 17), since all threads started their blue
6 Observe that every thread reads abort in their contract on lines 16–17, even though
they do not have the required access rights to do so. This is resolved by adding some
auxiliary ghost state, but this is omitted for presentational clarity.
260
W. Oortwijn et al.
1
2
);
2 context ∀tid , s : Perm(color [tid ][s],
1
2
) ∗∗ Perm(pink [tid ][s],
1
2
);
3 context ∀tid : Perm(exploringred [tid ],
1
2
) ∗∗ Perm(redroot[tid ],
1
2
);
4 context ∀tid : Perm(waiting[tid ],
1
2
);
5 context 0 ≤ sI < N;
6 requires ∀tid , s : ¬exploringred [tid ] ∧ color [tid ][s] = white ∧ ¬pink [tid ][s];
7 ensures \result ⇒ (∃a : acc[a] ∧ ExPath(sI , a, 1) ∧ ExPath(a, a, 2));
8 ensures (∃a : acc[a] ∧ ExPath(sI , a, 1) ∧ ExPath(a, a, 2)) ⇒ \result;
9 bool pndfs(sI )
10
par tid = 0 to nthreads
11
context Perm(N ) ∗∗ Perm(nthreads) ∗∗ Perm(G) ∗∗ Perm(acc);
12
context ∀s : Perm(color [tid ][s],
1
2
) ∗∗ Perm(pink [tid ][s],
1
2
);
13
context Perm(term[tid ],
1
2
) ∗∗ Perm(exploringred [tid ],
1
2
);
14
context Perm(redroot[tid ],
1
2
) ∗∗ Perm(waiting[tid ],
1
2
);
15
requires ¬exploringred [tid ] ∧ ∀s : color [tid ][s] = white ∧ ¬pink [tid ][s];
16
ensures ¬abort ⇒ ∀s : color [tid ][s] = cyan ∧ ¬pink [tid ][s];
17
ensures ¬abort ⇒ color [tid ][sI ] = blue;
18
do
19
bool found := dfsblue(sI , tid );
20
if found then
21
atomic { abort := true; } // initiate global termination.
22
atomic { if ¬abort then theorem one() }; // apply Thm. 1’s encoding.
23
return abort;
Fig. 6: The annotated version of pndfs, extending the excerpt given in Figure 3.
Correctness of pndfs. Figure 6 gives the annotated version of pndfs
6 that
extends the excerpt given earlier, in lines 23–25 of Figure 3. The main thread
requires partial ownership of all thread-local colour fields on line 2 and distributes
these over the appropriate threads on line 12. The contract associated to the
parallel block (lines 11–17) is called an iteration contract and assigns pre- and
postconditions to every parallel instance. For more details on iteration contracts
we refer to [5]. Most importantly, the iteration contract of each thread holds
enough resources to satisfy all the preconditions of dfsblue, on line 19.
Soundness of pndfs (line 7) is proven as follows. Suppose that all threads have
terminated and abort has been set to true. In that case, the resource invariant
states that an accepting cycle has been found. This information can be retrieved
by briefly obtaining the resource invariant in ghost code on line 22, which directly
allows to deduce soundness. Note that this information is not lost upon releasing
the resource invariant, as it is a Boolean property and thus duplicable.
To prove completeness, suppose that abort is still false when all workers have
terminated. This implies that Pink tid = ∅ and Cyan tid = ∅ for every worker tid
(line 16), as well as s I ∈ Blue tid (line 17), since all threads started their blue
6 Observe that every thread reads abort in their contract on lines 16–17, even though
they do not have the required access rights to do so. This is resolved by adding some
auxiliary ghost state, but this is omitted for presentational clarity.
260
W. Oortwijn et al.