Verifying Concurrent Programs via Bounded Context-Switching and Induction

Abstract

This paper presents a new approach to the problem of verifying safety properties of concurrent programs with shared memory and interleaving semantics. The method described leverages recent work on context-bounded analysis (CBA) via "sequentialization". In such work, a concurrent program P is converted to a sequential program whose behavior is equivalent to P for up to K context switches. By itself, CBA is not a sound verification method because it bounds the number of context switches considered, and hence does not explore all of P's behaviors.

We combine CBA with K-induction to create a method that can verify properties for an unbounded number of context switches. In a K-induction argument, two "windows" of K steps are considered: the base case considers a prefix of up to K steps; the inductive case assumes that the property of interest is true for the previous K steps, and attempts to establish the property for one more step.

We argue that CBA has the right characteristics to complement K-induction. In fact, our method uses CBA unchanged to discharge the base case. It also uses CBA as a subroutine when discharging the inductive case. The method works by analyzing two sequential programs, T1 and T2, each of which is a transformed version of P that simulates P's behavior for K context switches. T1 and T2 work slightly differently, and the analyses performed on them start from different sets of initial configurations. If, in both T1 and T2, the analyzer shows that the error state cannot be reached in K context switches, K-induction implies that P cannot reach the error state in any number of context switches.

The account sketched out above over-simplifies. There are actually several impediments to being able to apply K-induction to verify concurrent programs. The paper identifies the elements that make it difficult to push through a K-induction argument in this context, and introduces three techniques that, when used together,side-step the difficulties.