1 enum Color {white, cyan, blue};
2 int N ; // the number of automata states (equal to |S|)
3 int nthreads; // the total number of participating workers
4 bool[N ][N ] G; // adjacency matrix representation of the input automaton
5 bool[N ] acc; // the encoding of the set of accepting states
6 Color[nthreads][N ] color ; // the colour sets for dfsblue (one for each thread)
7 bool[nthreads][N ] pink ; // the pink colour sets for dfsred (one per thread)
8 bool[N ] red ; // the global set of red colourings
9 bool abort; // global termination flag
10
11 resource resource invariant · · · ; // full definition is deferred to Fig. 4.
12
13 bool Path(int s, int t, seqint P ) // the encoding of (s, t)-paths in G
14
0 ≤ s, t < N ∧ 0 < |P | ∧ P [0] = s ∧ P [|P | − 1] = t ∧
15
(∀i : 0 ≤ i < |P | ⇒ 0 ≤ P [i] < N)∧(∀i : 0 ≤ i < |P |−1 ⇒ G[P [i]][P [i+1]]);
16 bool Path(seqint P ) 0 < |P | ∧ Path(P [0], P [|P | − 1], P );
17 bool ExPath(int s, int t, int n) ∃P : n ≤ |P | ∧ Path(s, t, P );
18 bool SpecialPath(seqint P, int tid) // the encoding of tid-special paths
19
pink [tid ][P [0]] ∧ color [tid ][P [|P | − 1]] = cyan ∧ ∀i : 0 ≤ i < |P | ⇒ ¬red [P [i]];
20 bool ExSpecialPath(int tid ) ∃P : 1 < |P | ∧ Path(P ) ∧ SpecialPath(P, tid );
21
22 /∗ An excerpt of the top-level contract (further discussed in Section 3.3). ∗/
23 ensures \result ⇒ (∃a : 0≤ a < N ∧acc[a]∧ExPath(sI , a, 1)∧ExPath(a, a, 2));
24 ensures (∃a : 0≤ a < N ∧acc[a]∧ExPath(sI , a, 1)∧ExPath(a, a, 2)) ⇒ \result;
25 bool pndfs(int sI );
Fig. 3: The automata representation and an excerpt of pndfs’s top-level contract.
Figure 3 shows the encoding of the input automaton G in VerCors. The
thread-local colour sets are represented as matrices of dimension nthreads×|S|, so
that each thread tid uses color [tid ][·] and pink [tid ][·] to administrate their (local)
status of exploration. The sets of red and accepting states are shared between
threads and thus encoded as |S|-sized Boolean arrays. The succ function can now
be defined such that t ∈ succ(s) whenever G[s][t] is true for every 0 ≤ s, t < N .
This encoding of automata, together with an encoding of the definition of
paths (on lines 13–17) is sufficient to express the main correctness property that
is proven by VerCors. More specifically, line 23 expresses soundness: a positive
return value indicates the existence of an accepting cycle. Line 24 expresses
completeness: if there exists an accepting cycle, then pndfs returns positively.
Atomic operations. The handwritten correctness argument of [25] for Figure 2
assumes that all program lines are executed atomically. This is reflected in the
VerCors encoding: all updates to shared memory are made within atomic operations, which specification-wise all give access to the same shared resources. For
example, the assignment s.pink [tid ] := true on line 15 (Fig. 2) is implemented
as the atomic operation “atomic { pink [tid ][s] := true }”. On the specification
level, the atomic sub-program receives all the missing access rights required for
256
W. Oortwijn et al.
2 int N ; // the number of automata states (equal to |S|)
3 int nthreads; // the total number of participating workers
4 bool[N ][N ] G; // adjacency matrix representation of the input automaton
5 bool[N ] acc; // the encoding of the set of accepting states
6 Color[nthreads][N ] color ; // the colour sets for dfsblue (one for each thread)
7 bool[nthreads][N ] pink ; // the pink colour sets for dfsred (one per thread)
8 bool[N ] red ; // the global set of red colourings
9 bool abort; // global termination flag
10
11 resource resource invariant · · · ; // full definition is deferred to Fig. 4.
12
13 bool Path(int s, int t, seqint P ) // the encoding of (s, t)-paths in G
14
0 ≤ s, t < N ∧ 0 < |P | ∧ P [0] = s ∧ P [|P | − 1] = t ∧
15
(∀i : 0 ≤ i < |P | ⇒ 0 ≤ P [i] < N)∧(∀i : 0 ≤ i < |P |−1 ⇒ G[P [i]][P [i+1]]);
16 bool Path(seqint P ) 0 < |P | ∧ Path(P [0], P [|P | − 1], P );
17 bool ExPath(int s, int t, int n) ∃P : n ≤ |P | ∧ Path(s, t, P );
18 bool SpecialPath(seqint P, int tid) // the encoding of tid-special paths
19
pink [tid ][P [0]] ∧ color [tid ][P [|P | − 1]] = cyan ∧ ∀i : 0 ≤ i < |P | ⇒ ¬red [P [i]];
20 bool ExSpecialPath(int tid ) ∃P : 1 < |P | ∧ Path(P ) ∧ SpecialPath(P, tid );
21
22 /∗ An excerpt of the top-level contract (further discussed in Section 3.3). ∗/
23 ensures \result ⇒ (∃a : 0≤ a < N ∧acc[a]∧ExPath(sI , a, 1)∧ExPath(a, a, 2));
24 ensures (∃a : 0≤ a < N ∧acc[a]∧ExPath(sI , a, 1)∧ExPath(a, a, 2)) ⇒ \result;
25 bool pndfs(int sI );
Fig. 3: The automata representation and an excerpt of pndfs’s top-level contract.
Figure 3 shows the encoding of the input automaton G in VerCors. The
thread-local colour sets are represented as matrices of dimension nthreads×|S|, so
that each thread tid uses color [tid ][·] and pink [tid ][·] to administrate their (local)
status of exploration. The sets of red and accepting states are shared between
threads and thus encoded as |S|-sized Boolean arrays. The succ function can now
be defined such that t ∈ succ(s) whenever G[s][t] is true for every 0 ≤ s, t < N .
This encoding of automata, together with an encoding of the definition of
paths (on lines 13–17) is sufficient to express the main correctness property that
is proven by VerCors. More specifically, line 23 expresses soundness: a positive
return value indicates the existence of an accepting cycle. Line 24 expresses
completeness: if there exists an accepting cycle, then pndfs returns positively.
Atomic operations. The handwritten correctness argument of [25] for Figure 2
assumes that all program lines are executed atomically. This is reflected in the
VerCors encoding: all updates to shared memory are made within atomic operations, which specification-wise all give access to the same shared resources. For
example, the assignment s.pink [tid ] := true on line 15 (Fig. 2) is implemented
as the atomic operation “atomic { pink [tid ][s] := true }”. On the specification
level, the atomic sub-program receives all the missing access rights required for
256
W. Oortwijn et al.