378
M. Mann and C. Barrett
Formally:
∀ i ∈I \I r , d∈ D, s ∈ S
2 , a∈ i. en i (s 0 ) ∧ T (s 0 , i−{a}, d, s 1 ) =⇒ en a (s 1 ) (6)
Note that this is only a slight generalization of the property that atomic instructions do not disable each other, a condition that we will need anyway in order to
apply partial order reduction to the atomic instruction set (see condition (2)).
The algorithm first creates an identical copy of the STS in line 1. Lines 2-4 set
up symbolic variables for the instructions, data, and states of each system. Line
5 adds constraints to the solver enforcing that both systems start in the same
state, use the same data, and that i
is i but with symbolic action a dropped.
Line 6 adds the transition relation constraint for each STS. The initial symbolic
set up is depicted in Fig. 3.
The outer loop at line 7 iterates over all possible complex instruction cardinalities. The inner loop starting at line 8 attempts to show that for each cardinality
c, instructions of that cardinality can be decomposed by delaying one action
(symbolically represented by a). If all instructions of cardinality c have been
decomposed, then the while loop condition is false and the outer loop continues.
Otherwise, it gets variable assignments from the constraint solver in lines 9-11
and learns a constraint at line 13 that prevents this particular action, a μ , from
being chosen for decomposition again. To ensure that we have not blocked all
possible actions, there is an additional check at line 13, which returns false in
the case that no action can be delayed for the current instruction.
Importantly, the algorithm assumes that if the delay of action a μ does not
create a valid witness sequence for a given complex instruction i μ , then the
same is true whenever the instruction i includes i μ . We call this a monotonicity
assumption, and it typically holds when actions are somewhat independent. The
monotonicity assumption motivated the current structure of the algorithm and
can significantly reduce the number of iterations in the algorithm. We can remove
this assumption by changing i μ ⊆ i to i μ = i in the antecedent in line 13.
Note that the monotonicity assumption does not make the algorithm unsound:
if it returns true, then (as we prove below) condition (5) holds. However, if the
algorithm returns false, then it may be that the version without the assumption
would return true. For each of our experiments, we were able to get a true result
with the monotonicity assumption.
Because the algorithm does not consider state reachability and looks for a
witness function that only depends on inputs, it can still return false when an
equivalent sequence might exist for reachable states. In such cases, users can
examine the constraint solver models and attempt to remove some of them by
proving other invariants.
3
If algorithm 1 returns true, we replace T with T r , where T r is the result of
removing from T all transitions s, i, d, s
where |i| > 1. Practically, this is
3 This was rarely necessary in our experiments. Our implementation also extended
the algorithm to support predicate abstraction, which could also rule out spurious
counterexamples, but this feature was never needed in our experiments.
M. Mann and C. Barrett
Formally:
∀ i ∈I \I r , d∈ D, s ∈ S
2 , a∈ i. en i (s 0 ) ∧ T (s 0 , i−{a}, d, s 1 ) =⇒ en a (s 1 ) (6)
Note that this is only a slight generalization of the property that atomic instructions do not disable each other, a condition that we will need anyway in order to
apply partial order reduction to the atomic instruction set (see condition (2)).
The algorithm first creates an identical copy of the STS in line 1. Lines 2-4 set
up symbolic variables for the instructions, data, and states of each system. Line
5 adds constraints to the solver enforcing that both systems start in the same
state, use the same data, and that i
is i but with symbolic action a dropped.
Line 6 adds the transition relation constraint for each STS. The initial symbolic
set up is depicted in Fig. 3.
The outer loop at line 7 iterates over all possible complex instruction cardinalities. The inner loop starting at line 8 attempts to show that for each cardinality
c, instructions of that cardinality can be decomposed by delaying one action
(symbolically represented by a). If all instructions of cardinality c have been
decomposed, then the while loop condition is false and the outer loop continues.
Otherwise, it gets variable assignments from the constraint solver in lines 9-11
and learns a constraint at line 13 that prevents this particular action, a μ , from
being chosen for decomposition again. To ensure that we have not blocked all
possible actions, there is an additional check at line 13, which returns false in
the case that no action can be delayed for the current instruction.
Importantly, the algorithm assumes that if the delay of action a μ does not
create a valid witness sequence for a given complex instruction i μ , then the
same is true whenever the instruction i includes i μ . We call this a monotonicity
assumption, and it typically holds when actions are somewhat independent. The
monotonicity assumption motivated the current structure of the algorithm and
can significantly reduce the number of iterations in the algorithm. We can remove
this assumption by changing i μ ⊆ i to i μ = i in the antecedent in line 13.
Note that the monotonicity assumption does not make the algorithm unsound:
if it returns true, then (as we prove below) condition (5) holds. However, if the
algorithm returns false, then it may be that the version without the assumption
would return true. For each of our experiments, we were able to get a true result
with the monotonicity assumption.
Because the algorithm does not consider state reachability and looks for a
witness function that only depends on inputs, it can still return false when an
equivalent sequence might exist for reachable states. In such cases, users can
examine the constraint solver models and attempt to remove some of them by
proving other invariants.
3
If algorithm 1 returns true, we replace T with T r , where T r is the result of
removing from T all transitions s, i, d, s
where |i| > 1. Practically, this is
3 This was rarely necessary in our experiments. Our implementation also extended
the algorithm to support predicate abstraction, which could also rule out spurious
counterexamples, but this feature was never needed in our experiments.