Scaling Verification by Leveraging Parametrization

Abstract

Modern hardware and software systems have become increasingly concurrent for increased performance. This performance, however, comes at a cost--these systems are highly error prone and hard to verify. Consequently, important techniques such as testing which have had considerable success in verifying sequential systems, have only witnessed limited success in verifying concurrent systems. These techniques can easily end up missing out important system bugs. In response, model checking has emerged as an important technique for exhaustively verifying such systems. Model checking verifies a model of the system by exhaustively exploring all the possible states the system can reach. However, this exhaustiveness comes at the cost of scalability: the system state which model checking has to explore grows exponentially with the system size. This is referred to as the state space explosion problem.

In this dissertation, I propose techniques for scaling model checking to large concurrent systems. In particular, I focus on systems which use simple replicated components operating concurrently in order to achieve high performance. Examples of such systems include multi-threaded software, multi-processors and data centers. In order to scale verification to a large number of components, I leverage special mathematical representations of these systems, referred to as parameterized systems.

Verification techniques for these systems, i.e., parameterized verification techniques, verify them for an unbounded number of components operating concurrently. These techniques typically work by constructing small-sized, over-approximate models of the system. This is accomplished by iteratively using abstraction and refinement techniques, where the abstraction technique typically reduces the size of the model under verification by discarding information and the refinement technique typically adds back any information required, which got discarded by the abstraction technique.

The parametric verification techniques developed in this dissertation either (1) rewrite the property under verification in order to enable efficient existing abstractions, (2) construct novel abstractions, or (3) construct novel refinement mechanisms. Using these techniques, I have verified systems from three important application domains: cache coherence protocols, emerging computer networks (software defined networks), and concurrent data structures.