372
M. Mann and C. Barrett
partial order reductions are sound only for checking state invariants. If the property of interest is temporal, the reduction could disallow input sequences that
trigger the property. This can be avoided by first instantiating a monitor [15]
and, if necessary, converting liveness properties to safety [5].
Partial order reduction is less natural in the synchronous setting, because
synchronous transition systems do not have easily expressible independent actions. Nevertheless, these systems can still benefit from partial order reduction.
Consider our motivating example: despite the huge number of system execution
paths to consider, many of them are redundant. Observe that if both inputs are
zero, then the state does not change. Furthermore, there is a temporal symmetry
in the system execution: from any state where en x is true, driving only inc x
followed by only inc y results in the same state as driving them in the opposite
order. Thus, this system has a large number of redundant interleavings, much
like a multi-threaded program. To address this problem, we introduce a partial order reduction for synchronous hardware. Our goal is to remove redundant
interleavings by adding constraints to the system. To maintain soundness, we
provide a set of conditions which must pass before we can add constraints.
3 Synchronous Partial Order Reduction
In order to be able to apply partial order reduction to a synchronous transition
system, we are interested in identifying pairs of instructions that can be reordered
without affecting the resulting state. More generally, we also want to be able
to find pairs that can only be reordered under certain conditions. To formalize
these notions, we adapt the notation and representation of guarded independence
relations from [37].
1
Definition 2. Given an STS: S, Init, A, En, D, T with instruction set I, let
G := P(S) be the set of predicates over the states. Let i 0 , i 1 , g be a guarded
independence tuple iff for all d 0 , d 1 ∈ D and reachable s ∈ S
3 , the following
condition holds:
en i0 (s 0 )∧g(s 0 )∧T (i 1 , d 1 , i 0 , d 0 , s) =⇒ ∃ s
.T (i 0 , d 0 , i 1 , d 1 , s 0 , s
, s 2 ).
According to this definition, if we can prove that i 0 , i 1 , g is a guarded independence tuple, then we can reorder i 1 , i 0 instruction sequences as long as i) i 0 is
enabled in the first state; ii) g holds in the first state; and iii) we also reorder the
corresponding data inputs. We check only the enabledness of i 0 because i 0 , i 1 is
the representative order, and we only need to be able to reorder to the representative, not from it. The guard allows us to consider partial order reductions that
only hold for a subset of the reachable states. To avoid trivially overconstraining
the system with conflicting reorderings, we will only consider one ordering for
each pair of instructions.
The condition in Definition 2 is difficult to check automatically because of
the existential quantifier. We instead check two slightly weaker conditions that
1 The main differences are our STS formalism and that we consider reachability.
M. Mann and C. Barrett
partial order reductions are sound only for checking state invariants. If the property of interest is temporal, the reduction could disallow input sequences that
trigger the property. This can be avoided by first instantiating a monitor [15]
and, if necessary, converting liveness properties to safety [5].
Partial order reduction is less natural in the synchronous setting, because
synchronous transition systems do not have easily expressible independent actions. Nevertheless, these systems can still benefit from partial order reduction.
Consider our motivating example: despite the huge number of system execution
paths to consider, many of them are redundant. Observe that if both inputs are
zero, then the state does not change. Furthermore, there is a temporal symmetry
in the system execution: from any state where en x is true, driving only inc x
followed by only inc y results in the same state as driving them in the opposite
order. Thus, this system has a large number of redundant interleavings, much
like a multi-threaded program. To address this problem, we introduce a partial order reduction for synchronous hardware. Our goal is to remove redundant
interleavings by adding constraints to the system. To maintain soundness, we
provide a set of conditions which must pass before we can add constraints.
3 Synchronous Partial Order Reduction
In order to be able to apply partial order reduction to a synchronous transition
system, we are interested in identifying pairs of instructions that can be reordered
without affecting the resulting state. More generally, we also want to be able
to find pairs that can only be reordered under certain conditions. To formalize
these notions, we adapt the notation and representation of guarded independence
relations from [37].
1
Definition 2. Given an STS: S, Init, A, En, D, T with instruction set I, let
G := P(S) be the set of predicates over the states. Let i 0 , i 1 , g be a guarded
independence tuple iff for all d 0 , d 1 ∈ D and reachable s ∈ S
3 , the following
condition holds:
en i0 (s 0 )∧g(s 0 )∧T (i 1 , d 1 , i 0 , d 0 , s) =⇒ ∃ s
.T (i 0 , d 0 , i 1 , d 1 , s 0 , s
, s 2 ).
According to this definition, if we can prove that i 0 , i 1 , g is a guarded independence tuple, then we can reorder i 1 , i 0 instruction sequences as long as i) i 0 is
enabled in the first state; ii) g holds in the first state; and iii) we also reorder the
corresponding data inputs. We check only the enabledness of i 0 because i 0 , i 1 is
the representative order, and we only need to be able to reorder to the representative, not from it. The guard allows us to consider partial order reductions that
only hold for a subset of the reachable states. To avoid trivially overconstraining
the system with conflicting reorderings, we will only consider one ordering for
each pair of instructions.
The condition in Definition 2 is difficult to check automatically because of
the existential quantifier. We instead check two slightly weaker conditions that
1 The main differences are our STS formalism and that we consider reachability.