Model checking concurrent programs

Concurrent programs are in widespread use for harnessing the computing power of multi-core hardware. However, it is very challenging to develop correct concurrent programs. In practice, concurrency-related bugs such as data races, deadlocks, and atomicity violations are very common. In this chapter, we describe efforts based on model-checking for automatic verification and debugging of concurrent programs. The emphasis is on core ideas for reasoning about synchronizations and communication between threads and processes, while considering all possible behaviors due to their interactions. We start by considering model-checking based on interacting pushdown system (PDS) models. In these models, each component (thread or process) is modeled as a pushdown automaton, where the stack is used to model recursion. Model checking based on pushdown automata has a close correspondence with dataflow analysis of programs, and this has been successfully used for verification of sequential programs. However, applying these methods to a system of interacting pushdown automata is not straightforward. Even the basic problem of reachability is undecidable in the general case. We describe some techniques that have been proposed to get around this barrier, by restricting the patterns of synchronization and communication among components. Although PDSs provide a natural model for concurrent programs, it is difficult to apply PDS-based model-checking techniques directly to concurrent programs in practice. In addition to the formidable decidability barrier, this is also due to the huge gap between low-level PDS models and the feature-rich high-level programming languages in which concurrent programs are written. Fortunately, the successes of model-checking on finite state systems and sequential programs have provided a wealth of useful abstractions and techniques to bridge this gap. In the last part of the chapter, we will describe verification techniques for concurrent programs that are inspired by these models. They often abstract the effects of synchronization and focus on handling the complexity of reasoning about all possible behaviors. However, they can, and should, exploit insights and results of PDS-based modelchecking.