Verifying Concurrent Programs via Bounded ContextSwitching and Induction
Prathmesh Prabhu, Akash Lal, NIcholas Kidd, Thomas Reps
2011
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 contextbounded 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 Kinduction to create a method that can verify properties for an unbounded number of context switches. In a Kinduction 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 Kinduction. 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, Kinduction implies that P cannot reach the error state in any number of context switches. The account sketched out above oversimplifies. There are actually several impediments to being able to apply Kinduction to verify concurrent programs. The paper identifies the elements that make it difficult to push through a Kinduction argument in this context, and introduces three techniques that, when used together,sidestep the difficulties.
Download this report (PDF)
Return to tech report index
