Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
379
achieved by adding a disjunctive constraint over the possible atomic actions. We
can now state the main results for reduced instruction sets.
Theorem 3. Let S be an STS. If condition (6) holds and ProveRIS(S) returns
true, then (5) holds.
Proof. We maintain the loop invariant at line 8 that for every instruction i
,
there is some action a
such that check sat(|i| = c ∧ i = i
∧ a = a
) is true. It’s
true initially for each c by condition (6). Afterwards, the check on line 14 ensures
that it is maintained. Furthermore, the check on line 9 ensures that when the
while loop is exited, then any satisfying assignment for check sat(|i| = c) is such
that s 1 = s
2 . Together, these conditions guarantee that (5) holds.
Theorem 4. Let S := S, Init, A, En, D, T be an STS such that condition (6)
holds and ProveRIS(S) returns true, and let T r be the transition relation for
the reduced instruction set. Let S r be the reduced STS obtained by replacing T
with T r in S. Then, safety property P ∈ S is an invariant for S r if and only if
it is also an invariant for S.
Proof. It suffices to show that the reachable states of S and S r are identical.
Init does not change, so the initial states cannot be different. Furthermore, T r
is obtained by removing transitions from T , we know that S r cannot add any
reachable states. To show that it also does not remove any reachable states,
consider an arbitrary trace Init(s 0 ) ∧ T (in, s) with |s| = n, we must show
∃ in
, m, s
∈ S
m . Init(s
0 ) ∧ T r (in
, s
) ∧ s n−1 = s
m−1 . We prove this by showing
by induction that it holds whenever in contains instructions of cardinality at
most c.
In the base case, c = 1, so all instructions are of size one or less. All of these
are already atomic and thus we can take in
= in and s
= s by the definition
of T r .
For the inductive step, suppose that it holds for cardinalities up to c − 1, and
assume Init(s 0 ) ∧ T (in, s) with |s| = n. Let in j = i, d be an input containing
an instruction of size at most c. If |i| < c, there is nothing to be done. Thus we
only consider the case where |i| = c. We know that T (s j , in j , s j+1 ) holds. By
Theorem 3 and condition (5), it follows that T (i−{a}, d, {a}, d, s j , s, s j+1 )
holds for some a and s. We can thus replace in j in in by i − {a}, d followed
by {a}, d to obtain an input sequence in c and insert s between s j and s j+1 in
s to obtain s c with final state s n−1 such that Init(s 0 ) ∧ T (in c , s c ). Repeating
this process for each input containing an instruction of size c yields a final in c
such that the maximum cardinality of any instruction is c−1. The property then
holds by the inductive hypothesis.
Note that if there is some instruction i ∈ I which cannot be decomposed
into atomic instructions, we could always keep this instruction in I r and still
benefit from removing other complex instructions. In many cases, we can also
remove the empty instruction, i e = ∅. If applying i e cannot change the state of
the system, regardless of the data input, then it is considered a stutter step [14].
It is straightforward to check whether i e can be removed by comparing the state
before and after applying i e .
379
achieved by adding a disjunctive constraint over the possible atomic actions. We
can now state the main results for reduced instruction sets.
Theorem 3. Let S be an STS. If condition (6) holds and ProveRIS(S) returns
true, then (5) holds.
Proof. We maintain the loop invariant at line 8 that for every instruction i
,
there is some action a
such that check sat(|i| = c ∧ i = i
∧ a = a
) is true. It’s
true initially for each c by condition (6). Afterwards, the check on line 14 ensures
that it is maintained. Furthermore, the check on line 9 ensures that when the
while loop is exited, then any satisfying assignment for check sat(|i| = c) is such
that s 1 = s
2 . Together, these conditions guarantee that (5) holds.
Theorem 4. Let S := S, Init, A, En, D, T be an STS such that condition (6)
holds and ProveRIS(S) returns true, and let T r be the transition relation for
the reduced instruction set. Let S r be the reduced STS obtained by replacing T
with T r in S. Then, safety property P ∈ S is an invariant for S r if and only if
it is also an invariant for S.
Proof. It suffices to show that the reachable states of S and S r are identical.
Init does not change, so the initial states cannot be different. Furthermore, T r
is obtained by removing transitions from T , we know that S r cannot add any
reachable states. To show that it also does not remove any reachable states,
consider an arbitrary trace Init(s 0 ) ∧ T (in, s) with |s| = n, we must show
∃ in
, m, s
∈ S
m . Init(s
0 ) ∧ T r (in
, s
) ∧ s n−1 = s
m−1 . We prove this by showing
by induction that it holds whenever in contains instructions of cardinality at
most c.
In the base case, c = 1, so all instructions are of size one or less. All of these
are already atomic and thus we can take in
= in and s
= s by the definition
of T r .
For the inductive step, suppose that it holds for cardinalities up to c − 1, and
assume Init(s 0 ) ∧ T (in, s) with |s| = n. Let in j = i, d be an input containing
an instruction of size at most c. If |i| < c, there is nothing to be done. Thus we
only consider the case where |i| = c. We know that T (s j , in j , s j+1 ) holds. By
Theorem 3 and condition (5), it follows that T (i−{a}, d, {a}, d, s j , s, s j+1 )
holds for some a and s. We can thus replace in j in in by i − {a}, d followed
by {a}, d to obtain an input sequence in c and insert s between s j and s j+1 in
s to obtain s c with final state s n−1 such that Init(s 0 ) ∧ T (in c , s c ). Repeating
this process for each input containing an instruction of size c yields a final in c
such that the maximum cardinality of any instruction is c−1. The property then
holds by the inductive hypothesis.
Note that if there is some instruction i ∈ I which cannot be decomposed
into atomic instructions, we could always keep this instruction in I r and still
benefit from removing other complex instructions. In many cases, we can also
remove the empty instruction, i e = ∅. If applying i e cannot change the state of
the system, regardless of the data input, then it is considered a stutter step [14].
It is straightforward to check whether i e can be removed by comparing the state
before and after applying i e .