Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
375
Fig. 2: Effect of Partial Order Reduction for Instructions i 0 and i 1 . Initial state
is green.
Proof. It suffices to show that S R can reach all the same states as S. We prove
this by contradiction. Assume there is some in, s such that Init(s 0 )∧T (in, s) and
0 ≤ j ≤ |s|− 1 such that s j is the first state that is unreachable in S R . The value
of j cannot be 0 or 1, because S and S R have the same initial states and T
R only
excludes sequences of length 2. Then, by the definition of T R , in j−2 , in j−1 must
be a sequence excluded by T
R . Conditions (2) and (3) guarantee that permuting
in j−2 and in j−1 results in an enabled sequence that ends in the same state,
s j , which contradicts the assumption. Thus, there cannot be a state which is
reachable in S but not S R .
4 Reduced Instruction Sets
Now that we can apply partial order reduction to synchronous systems, our main
goal is to identify a maximal guarded independence relation, R. Recall that we
defined instructions as sets of atomic actions. We call an instruction containing at most one action atomic (this includes the instruction with no actions).
Non-atomic instructions are complex. Instructions thus reflect the parallelism of
synchronous hardware, and lead to natural candidates for R: pairs of atomic
instructions.
Furthermore, notice that the number of instructions is exponential in the
number of actions. Thus, it could be prohibitively expensive to check every pair
of instructions for guarded independence. In contrast, the number of atomic
instructions is equal to the number of actions (plus one). Furthermore, it is
likely that many complex instruction pairs will not have a guarded independence
relationship because they contain common actions. Our goal in this section is to
disallow as many complex instructions as possible without losing any reachable
375
Fig. 2: Effect of Partial Order Reduction for Instructions i 0 and i 1 . Initial state
is green.
Proof. It suffices to show that S R can reach all the same states as S. We prove
this by contradiction. Assume there is some in, s such that Init(s 0 )∧T (in, s) and
0 ≤ j ≤ |s|− 1 such that s j is the first state that is unreachable in S R . The value
of j cannot be 0 or 1, because S and S R have the same initial states and T
R only
excludes sequences of length 2. Then, by the definition of T R , in j−2 , in j−1 must
be a sequence excluded by T
R . Conditions (2) and (3) guarantee that permuting
in j−2 and in j−1 results in an enabled sequence that ends in the same state,
s j , which contradicts the assumption. Thus, there cannot be a state which is
reachable in S but not S R .
4 Reduced Instruction Sets
Now that we can apply partial order reduction to synchronous systems, our main
goal is to identify a maximal guarded independence relation, R. Recall that we
defined instructions as sets of atomic actions. We call an instruction containing at most one action atomic (this includes the instruction with no actions).
Non-atomic instructions are complex. Instructions thus reflect the parallelism of
synchronous hardware, and lead to natural candidates for R: pairs of atomic
instructions.
Furthermore, notice that the number of instructions is exponential in the
number of actions. Thus, it could be prohibitively expensive to check every pair
of instructions for guarded independence. In contrast, the number of atomic
instructions is equal to the number of actions (plus one). Furthermore, it is
likely that many complex instruction pairs will not have a guarded independence
relationship because they contain common actions. Our goal in this section is to
disallow as many complex instructions as possible without losing any reachable