1 resource resource invariant
2
Perm(N ) ∗∗ Perm(nthreads) ∗∗ Perm(G) ∗∗ Perm(acc) ∗∗
3
(∀tid , s : Perm(color [tid ][s],
1
2
) ∗∗ Perm(pink [tid ][s],
1
2
)) ∗∗
4
(∀s : Perm(red [s], 1)) ∗∗
5
termination() ∗∗ colourings() ∗∗ dfsred status() ∗∗ keyinvariant();
6
7 resource termination() // Resources for termination handling.
8
Perm(abort,
1
2
) ∗∗ abort ⇒ ∃s : acc[s] ∧ ExPath(sI , s, 1) ∧ ExPath(s, s, 2);
9
10 resource colourings() // The low-level colouring invariant encodings.
11
∀tid , s : (color [tid ][s] = blue ∨ pink [tid ][s]) ⇒ ∀s
∈ succ(s) :
12
color [tid ][s
] = blue ∨ color [tid ][s
] = cyan ∨ red [s
] ∗∗ // Inv. 1.1
13
∀s : red [s] ⇒ ∀s
∈ succ(s) :
14
red [s
] ∨ ∃tid : pink [tid ][s
] ∧ color [tid ][s
] = cyan ∗∗ // Inv. 1.2
15
∀tid , s : (acc[s] ∧ color [tid ][s] = blue) ⇒ red [s] ∗∗ // Inv. 1.3
16
∀tid , s : (acc[s] ∧ pink [tid ][s]) ⇒ color [tid ][s] = cyan ∗∗ // Inv. 1.4
17
∀tid , s : pink [tid ][s] ⇒ (color [tid ][s] = cyan ∨ color [tid ][s] = blue); // 1.5
18
19 /∗ Auxiliary ghost state for proving Lemma 3 and preserving Inv. 4. ∗/
20 resource dfsred status() ∀tid : (
21
Perm(exploringred [tid ],
1
2
) ∗∗ Perm(redroot [tid ],
1
2
) ∗∗ Perm(waiting[tid ],
1
2
) ∗∗
22
∀s : pink [tid ][s] ⇒ (exploringred [tid ] ∧ (acc[s] ⇒ s = redroot[tid ])) ∗∗ // 1.6
23
exploringred [tid ] ⇒ acc[redroot [tid ]] ∧
24
(∀s : pink [tid ][s] ⇒ ExPath(redroot [tid ], s, 1)) ∧
25
(∀s : color [tid ][s] = cyan ⇒ ExPath(s, redroot [tid ], 1)) ∧
26
(¬waiting[tid ] ⇒ ¬red [redroot [tid ]]) ∧
27
(waiting[tid ] ⇒ ∀s : pink [tid ][s] ⇔ s = redroot[tid ])
28
29 /∗ The encoding of Lemma 4, from which completeness of pndfs follows. ∗/
30 resource keyinvariant()
31
(∀s : acc[s] ∧ ExPath(sI , s, 1) ∧ ExPath(s, s, 2) ⇒ ¬red [s]) ∨
32
(∃tid : ExSpecialPath(tid ));
Fig. 4: The full definition of the resource invariant. Several bound checks have
been omitted for presentational clarity.
Observe that the resource invariant holds a lot of quantified information. As a
result, we experienced that proving the reestablishment of resource invariant
after finishing atomics is expensive performance-wise. To make verification more
efficient, we extracted all atomic operations (e.g., colour updates) into separate
methods and prove their contracts in a function-modular way. This improves
performance, as it cuts the problem of verifying dfsred and dfsblue into smaller
sub-problems that are individually more manageable for the SMT solver.
Finally, Figure 5 presents an excerpt of the contract of dfsblue, which shows
the ownership pattern of all threads. Notably, every thread tid receives the remaining ownership of color [tid ] and pink [tid ] on line 4. Thus threads can always
read from their thread-local colour fields, and may write to them while doing so
258
W. Oortwijn et al.
2
Perm(N ) ∗∗ Perm(nthreads) ∗∗ Perm(G) ∗∗ Perm(acc) ∗∗
3
(∀tid , s : Perm(color [tid ][s],
1
2
) ∗∗ Perm(pink [tid ][s],
1
2
)) ∗∗
4
(∀s : Perm(red [s], 1)) ∗∗
5
termination() ∗∗ colourings() ∗∗ dfsred status() ∗∗ keyinvariant();
6
7 resource termination() // Resources for termination handling.
8
Perm(abort,
1
2
) ∗∗ abort ⇒ ∃s : acc[s] ∧ ExPath(sI , s, 1) ∧ ExPath(s, s, 2);
9
10 resource colourings() // The low-level colouring invariant encodings.
11
∀tid , s : (color [tid ][s] = blue ∨ pink [tid ][s]) ⇒ ∀s
∈ succ(s) :
12
color [tid ][s
] = blue ∨ color [tid ][s
] = cyan ∨ red [s
] ∗∗ // Inv. 1.1
13
∀s : red [s] ⇒ ∀s
∈ succ(s) :
14
red [s
] ∨ ∃tid : pink [tid ][s
] ∧ color [tid ][s
] = cyan ∗∗ // Inv. 1.2
15
∀tid , s : (acc[s] ∧ color [tid ][s] = blue) ⇒ red [s] ∗∗ // Inv. 1.3
16
∀tid , s : (acc[s] ∧ pink [tid ][s]) ⇒ color [tid ][s] = cyan ∗∗ // Inv. 1.4
17
∀tid , s : pink [tid ][s] ⇒ (color [tid ][s] = cyan ∨ color [tid ][s] = blue); // 1.5
18
19 /∗ Auxiliary ghost state for proving Lemma 3 and preserving Inv. 4. ∗/
20 resource dfsred status() ∀tid : (
21
Perm(exploringred [tid ],
1
2
) ∗∗ Perm(redroot [tid ],
1
2
) ∗∗ Perm(waiting[tid ],
1
2
) ∗∗
22
∀s : pink [tid ][s] ⇒ (exploringred [tid ] ∧ (acc[s] ⇒ s = redroot[tid ])) ∗∗ // 1.6
23
exploringred [tid ] ⇒ acc[redroot [tid ]] ∧
24
(∀s : pink [tid ][s] ⇒ ExPath(redroot [tid ], s, 1)) ∧
25
(∀s : color [tid ][s] = cyan ⇒ ExPath(s, redroot [tid ], 1)) ∧
26
(¬waiting[tid ] ⇒ ¬red [redroot [tid ]]) ∧
27
(waiting[tid ] ⇒ ∀s : pink [tid ][s] ⇔ s = redroot[tid ])
28
29 /∗ The encoding of Lemma 4, from which completeness of pndfs follows. ∗/
30 resource keyinvariant()
31
(∀s : acc[s] ∧ ExPath(sI , s, 1) ∧ ExPath(s, s, 2) ⇒ ¬red [s]) ∨
32
(∃tid : ExSpecialPath(tid ));
Fig. 4: The full definition of the resource invariant. Several bound checks have
been omitted for presentational clarity.
Observe that the resource invariant holds a lot of quantified information. As a
result, we experienced that proving the reestablishment of resource invariant
after finishing atomics is expensive performance-wise. To make verification more
efficient, we extracted all atomic operations (e.g., colour updates) into separate
methods and prove their contracts in a function-modular way. This improves
performance, as it cuts the problem of verifying dfsred and dfsblue into smaller
sub-problems that are individually more manageable for the SMT solver.
Finally, Figure 5 presents an excerpt of the contract of dfsblue, which shows
the ownership pattern of all threads. Notably, every thread tid receives the remaining ownership of color [tid ] and pink [tid ] on line 4. Thus threads can always
read from their thread-local colour fields, and may write to them while doing so
258
W. Oortwijn et al.