Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
371
Model Checking. Given an STS S, let a safety property P ⊆ S be a set containing acceptable states. The model checking problem is to determine whether
the system stays within this acceptable set for all possible execution traces.
Formally, we want to check whether the following holds:
∀ n ≥ 0, in ∈ Input
n , s ∈ S
n+1 . (Init(s 0 ) ∧ T (in, s)) =⇒ s n ∈ P
(1)
When equation (1) holds, we say that P is an invariant of S. A number of
techniques exist for solving this problem, including Binary Decision Diagram
(BDD)-based [12] approaches, Interpolant-based [27] approaches, and IC3/PDR
(property directed reachability) techniques [10,16]. We refer the interested reader
to [15] for a more complete survey of model checking algorithms.
In this paper, we will focus on bounded model checking (BMC). In BMC,
instead of proving (1) for all n, we prove it for all n less than some finite bound
k. Though it typically cannot be used to prove properties, BMC can be quite
effective at finding bugs [6] and is especially useful when full model checking is
infeasible.
Symmetry. Early on in the development of model checking, researchers recognized the importance of symmetry reduction to combat the state explosion
problem [13]. Existing approaches in the hardware domain perform data symmetry reduction and data type reduction through the use of bit-width reduction
preprocessing passes or syntactic restrictions such as scalarsets [8,20,28]. There
have also been abstraction-refinement loop algorithms proposed to handle memory symmetries [9]. All of these approaches are focused on symmetries present
in the transition system description, such as the presence of large data types.
We refer to these types of symmetries as data symmetries. Most of these techniques are intended to speed up proofs of true properties rather than accelerate
bug-finding.
Model checking of asynchronous systems such as concurrent programs faces
an orthogonal issue due to the many possible redundant interleavings of independent processes. Throughout this paper, we refer to this as path symmetry.
Path symmetry is a temporal symmetry: it relates to executions of a system
rather than just its size. Path symmetries occur when there are many distinct
ways of reaching the same state in a system execution. Exploring all such paths
can result in exponential case splitting.
This paper provides evidence that path symmetry can also severely hurt
model checking performance in synchronous systems. One of the first techniques
proposed to handle path symmetry was partial order reduction.
Partial Order Reduction. Partial order reduction was first developed in the
explicit-state model checking context but was later extended to symbolic model
checking [37]. The approach is named “partial order reduction” for historical reasons, but Clarke noted in [14] that “model checking using representatives” [30,31]
may have been a more appropriate name. In particular, partial order reduction
attempts to develop equivalence classes of behaviors so that only one representative from each class needs to be considered during model checking. Note that
371
Model Checking. Given an STS S, let a safety property P ⊆ S be a set containing acceptable states. The model checking problem is to determine whether
the system stays within this acceptable set for all possible execution traces.
Formally, we want to check whether the following holds:
∀ n ≥ 0, in ∈ Input
n , s ∈ S
n+1 . (Init(s 0 ) ∧ T (in, s)) =⇒ s n ∈ P
(1)
When equation (1) holds, we say that P is an invariant of S. A number of
techniques exist for solving this problem, including Binary Decision Diagram
(BDD)-based [12] approaches, Interpolant-based [27] approaches, and IC3/PDR
(property directed reachability) techniques [10,16]. We refer the interested reader
to [15] for a more complete survey of model checking algorithms.
In this paper, we will focus on bounded model checking (BMC). In BMC,
instead of proving (1) for all n, we prove it for all n less than some finite bound
k. Though it typically cannot be used to prove properties, BMC can be quite
effective at finding bugs [6] and is especially useful when full model checking is
infeasible.
Symmetry. Early on in the development of model checking, researchers recognized the importance of symmetry reduction to combat the state explosion
problem [13]. Existing approaches in the hardware domain perform data symmetry reduction and data type reduction through the use of bit-width reduction
preprocessing passes or syntactic restrictions such as scalarsets [8,20,28]. There
have also been abstraction-refinement loop algorithms proposed to handle memory symmetries [9]. All of these approaches are focused on symmetries present
in the transition system description, such as the presence of large data types.
We refer to these types of symmetries as data symmetries. Most of these techniques are intended to speed up proofs of true properties rather than accelerate
bug-finding.
Model checking of asynchronous systems such as concurrent programs faces
an orthogonal issue due to the many possible redundant interleavings of independent processes. Throughout this paper, we refer to this as path symmetry.
Path symmetry is a temporal symmetry: it relates to executions of a system
rather than just its size. Path symmetries occur when there are many distinct
ways of reaching the same state in a system execution. Exploring all such paths
can result in exponential case splitting.
This paper provides evidence that path symmetry can also severely hurt
model checking performance in synchronous systems. One of the first techniques
proposed to handle path symmetry was partial order reduction.
Partial Order Reduction. Partial order reduction was first developed in the
explicit-state model checking context but was later extended to symbolic model
checking [37]. The approach is named “partial order reduction” for historical reasons, but Clarke noted in [14] that “model checking using representatives” [30,31]
may have been a more appropriate name. In particular, partial order reduction
attempts to develop equivalence classes of behaviors so that only one representative from each class needs to be considered during model checking. Note that