376
M. Mann and C. Barrett
states, thereby reducing the number of pairs of instructions we need to check
while also making it more likely for the checks to succeed. Note that, in isolation,
removing instructions might be problematic, because it could extend the bound
needed to reach a property violation. However, as we will demonstrate in the
experimental section, this disadvantage is more than compensated for when it is
applied in combination with partial order reduction.
Given an STS with instruction set I, we seek a reduced instruction set,
I r ⊆ I, which preserves the reachable states of the system. Let Input r be the
set of inputs which only use instructions from I r . Given an input in ∈ Input,
our goal is to prove the existence of a witness w(in) ∈ Input
n
r (for some n > 0)
that simulates the behavior of in using only reduced instructions. Formally, the
witness function w should satisfy:
∀ s, s
∈ S, in ∈ Input. T (s, in, s
) =⇒
∃ n ∈ N, s ∈ S
n . T (w(in), s : s) ∧ (s n−1 = s
)
(4)
In other words, we need to show that for every instruction in the original instruction set, there exists a sequence of inputs, using only instructions from the
reduced instruction set (RIS), that results in the same final state. Notice that
a witness function that also depended on the state would be more general, but
for our purposes, it is sufficient for the witness function to depend only on the
input.
4.1 Atomic instruction sets
The condition in (4) is quite general and does not provide any intuition on how
to choose w. Here, we focus on a specific case where w is easy to construct: we
choose I r to be an atomic instruction set, defined as an instruction set containing
only atomic instructions. We then must prove that the set of reachable states is
not affected by restricting the instructions to those in I r .
It is sufficient to prove that for each complex instruction, we can remove one
of its actions and perform that action in the next step, with the same result. For
some complex instruction i containing a and some data input d, let w
a (i, d) be
i−{a}, d, {a}, d. We must show that for each input in containing a complex
instruction, there exists some a where w
a (in) has the equivalent effect on the
system as in. Formally, the requirement is:
∀i ∈ I \ I r , d ∈ D, s ∈ S
2 .
T (s 0 , i, d, s 1 ) =⇒ ∃ a ∈ i, s
∈ S
3 . T (w
a (i, d), s
) ∧ s 0 = s
0 ∧ s 1 = s
2
(5)
Condition (5) is still difficult to prove because of the existential quantifier. One
conservative approach is to replace the existential quantifier with a universal
quantifier and attempt to prove that stronger condition. For real systems, this
is unlikely to hold. Instead, we propose a counterexample blocking procedure
which, if it succeeds, guarantees (5). We introduce symbolic values for i, d, and
a and then iteratively add constraints over them until the proof succeeds or
M. Mann and C. Barrett
states, thereby reducing the number of pairs of instructions we need to check
while also making it more likely for the checks to succeed. Note that, in isolation,
removing instructions might be problematic, because it could extend the bound
needed to reach a property violation. However, as we will demonstrate in the
experimental section, this disadvantage is more than compensated for when it is
applied in combination with partial order reduction.
Given an STS with instruction set I, we seek a reduced instruction set,
I r ⊆ I, which preserves the reachable states of the system. Let Input r be the
set of inputs which only use instructions from I r . Given an input in ∈ Input,
our goal is to prove the existence of a witness w(in) ∈ Input
n
r (for some n > 0)
that simulates the behavior of in using only reduced instructions. Formally, the
witness function w should satisfy:
∀ s, s
∈ S, in ∈ Input. T (s, in, s
) =⇒
∃ n ∈ N, s ∈ S
n . T (w(in), s : s) ∧ (s n−1 = s
)
(4)
In other words, we need to show that for every instruction in the original instruction set, there exists a sequence of inputs, using only instructions from the
reduced instruction set (RIS), that results in the same final state. Notice that
a witness function that also depended on the state would be more general, but
for our purposes, it is sufficient for the witness function to depend only on the
input.
4.1 Atomic instruction sets
The condition in (4) is quite general and does not provide any intuition on how
to choose w. Here, we focus on a specific case where w is easy to construct: we
choose I r to be an atomic instruction set, defined as an instruction set containing
only atomic instructions. We then must prove that the set of reachable states is
not affected by restricting the instructions to those in I r .
It is sufficient to prove that for each complex instruction, we can remove one
of its actions and perform that action in the next step, with the same result. For
some complex instruction i containing a and some data input d, let w
a (i, d) be
i−{a}, d, {a}, d. We must show that for each input in containing a complex
instruction, there exists some a where w
a (in) has the equivalent effect on the
system as in. Formally, the requirement is:
∀i ∈ I \ I r , d ∈ D, s ∈ S
2 .
T (s 0 , i, d, s 1 ) =⇒ ∃ a ∈ i, s
∈ S
3 . T (w
a (i, d), s
) ∧ s 0 = s
0 ∧ s 1 = s
2
(5)
Condition (5) is still difficult to prove because of the existential quantifier. One
conservative approach is to replace the existential quantifier with a universal
quantifier and attempt to prove that stronger condition. For real systems, this
is unlikely to hold. Instead, we propose a counterexample blocking procedure
which, if it succeeds, guarantees (5). We introduce symbolic values for i, d, and
a and then iteratively add constraints over them until the proof succeeds or