374
M. Mann and C. Barrett
If both conditions pass, then we can choose a representative order and disallow the opposite ordering for that pair of instructions. If the proof of condition (3) fails, it provides a counterexample which should either convince the
user that partial order reduction does not apply for that pair of instructions
(a real counterexample), or serve as a guide for the user to write guards that
would remove the spurious counterexample. Other invariants of the system, either obtained automatically or manually guessed by the user, could also remove
spurious counterexamples. We can now state the first theorem of synchronous
partial order reduction: that these conditions guarantee guarded independence
over all reachable states.
Theorem 1. Given an STS S := S, Init, A, En, D, T , with instruction set I :=
P(A): if conditions (2) and (3) hold for instructions i o , i 1 ∈ I, and guard g ∈
P(S), then i 0 , i 1 , g is a guarded independence tuple.
Proof. Assume conditions (2) and (3) and that for some d 0 , d 1 ∈ D and reachable
s ∈ S
3 , we have:
en i0 (s 0 ) ∧ g(s 0 ) ∧ T (i 1 , d 1 , i 0 , d 0 , s)
Because en i0 (s 0 ), we have ∃s
, d
. T (s 0 , i 0 , d
, s
) because of our enabledness
assumption. Furthermore, by the data-input independence property of transition
relations, it follows that for some s
1 , T (s 0 , i 0 , d 0 , s
1 ) Now, because one of our
assumptions is a transition from s 0 using i 1 , en i1 (s 0 ) must be true. Condition
(2) implies that en i1 (s
1 ), thus ∃ s
, d
. T (i 0 , d 0 , i 1 , d
, s 0 , s
1 , s
). As before,
this implies that for some s
2 , we also have that T (i 0 , d 0 , i 1 , d 1 , s 0 , s
1 , s
2 ).
It then follows from (3) that s
2 = s 2 , and thus, i 0 , i 1 , g satisfies the condition
from Definition 2.
Let a guarded independence relation, R ⊆ I × I × G, be a set of guarded
independence tuples. We now describe how to apply partial order reductions,
given some R. For each i 0 , i 1 , g ∈ R, and for every s ∈ S
2 , d ∈ D, whenever
T (s 0 , i 1 , d 1 , s 1 )∧en i0 (s 0 )∧g(s 0 ) holds, we remove from T every transition of the
form s 1 , i 0 , d, s (for any d and s). Let T
R be the result. To apply this reduction
in practice, we add a constraint to the BMC encoding: (g(s 0 )∧en i0 (s 0 )∧i 1 ) =⇒
¬next(i 0 ).
This makes it impossible for the STS system to ever execute an instruction
i 0 after an instruction i 1 when starting from a state where i 0 is enabled and g
holds. This effectively gives preference to i 0 as long as it is enabled. The effect
of partial order reduction on a pair of instructions in a synchronous system is
depicted in Fig. 2. Red X’s show removed transitions, and for simplicity, we
assume a trivial guard of true. Notice that all states are still reachable via some
path from the initial state in the bottom left corner.
Theorem 2. Given S := S, Init, A, En, D, T , let R be a guarded independence
relation and let S R be the reduced STS obtained by replacing T with T
R in S.
Then, if a property P is an invariant for S R , it is also an invariant for S.
M. Mann and C. Barrett
If both conditions pass, then we can choose a representative order and disallow the opposite ordering for that pair of instructions. If the proof of condition (3) fails, it provides a counterexample which should either convince the
user that partial order reduction does not apply for that pair of instructions
(a real counterexample), or serve as a guide for the user to write guards that
would remove the spurious counterexample. Other invariants of the system, either obtained automatically or manually guessed by the user, could also remove
spurious counterexamples. We can now state the first theorem of synchronous
partial order reduction: that these conditions guarantee guarded independence
over all reachable states.
Theorem 1. Given an STS S := S, Init, A, En, D, T , with instruction set I :=
P(A): if conditions (2) and (3) hold for instructions i o , i 1 ∈ I, and guard g ∈
P(S), then i 0 , i 1 , g is a guarded independence tuple.
Proof. Assume conditions (2) and (3) and that for some d 0 , d 1 ∈ D and reachable
s ∈ S
3 , we have:
en i0 (s 0 ) ∧ g(s 0 ) ∧ T (i 1 , d 1 , i 0 , d 0 , s)
Because en i0 (s 0 ), we have ∃s
, d
. T (s 0 , i 0 , d
, s
) because of our enabledness
assumption. Furthermore, by the data-input independence property of transition
relations, it follows that for some s
1 , T (s 0 , i 0 , d 0 , s
1 ) Now, because one of our
assumptions is a transition from s 0 using i 1 , en i1 (s 0 ) must be true. Condition
(2) implies that en i1 (s
1 ), thus ∃ s
, d
. T (i 0 , d 0 , i 1 , d
, s 0 , s
1 , s
). As before,
this implies that for some s
2 , we also have that T (i 0 , d 0 , i 1 , d 1 , s 0 , s
1 , s
2 ).
It then follows from (3) that s
2 = s 2 , and thus, i 0 , i 1 , g satisfies the condition
from Definition 2.
Let a guarded independence relation, R ⊆ I × I × G, be a set of guarded
independence tuples. We now describe how to apply partial order reductions,
given some R. For each i 0 , i 1 , g ∈ R, and for every s ∈ S
2 , d ∈ D, whenever
T (s 0 , i 1 , d 1 , s 1 )∧en i0 (s 0 )∧g(s 0 ) holds, we remove from T every transition of the
form s 1 , i 0 , d, s (for any d and s). Let T
R be the result. To apply this reduction
in practice, we add a constraint to the BMC encoding: (g(s 0 )∧en i0 (s 0 )∧i 1 ) =⇒
¬next(i 0 ).
This makes it impossible for the STS system to ever execute an instruction
i 0 after an instruction i 1 when starting from a state where i 0 is enabled and g
holds. This effectively gives preference to i 0 as long as it is enabled. The effect
of partial order reduction on a pair of instructions in a synchronous system is
depicted in Fig. 2. Red X’s show removed transitions, and for simplicity, we
assume a trivial guard of true. Notice that all states are still reachable via some
path from the initial state in the bottom left corner.
Theorem 2. Given S := S, Init, A, En, D, T , let R be a guarded independence
relation and let S R be the reduced STS obtained by replacing T with T
R in S.
Then, if a property P is an invariant for S R , it is also an invariant for S.