Zing: Exploiting program structure for model checking concurrent software

Model checking is a technique for finding bugs in systems by systematically exploring their state spaces. We wish to extract sound models from concurrent programs automatically and check the behaviors of these models systematically. The Zing project is an effort to build a flexible infrastructure to represent and model check abstractions of large concurrent software.

To support automatic extraction of models from programs written in common programming languages, Zing’s modeling language supports three facilities present in modern programming languages: (1) procedure calls with a call-stack, (2) objects with dynamic allocation, and (3) processes with dynamic creation, using both shared memory and message passing for communication. We believe that these three facilities capture the essence of model checking modern concurrent software.

Building a scalable model-checker for such an expressive modeling language is a huge challenge. Zing’s modular architecture provides a clear separation between the expressive semantics of the modeling language, and a simple view of Zing programs as labeled transition systems. This separation has allowed us to decouple the design of efficient model checking algorithms from the complexity of supporting rich constructs in the modeling language.

Zing’s model checking algorithms have been designed to exploit existing structural abstractions in concurrent programs such as processes and procedure calls. We present two such novel techniques in the paper: (1) compositional checking of Zing models for message-passing programs using a conformance theory inspired by work in the process algebra community, and (2) a new summarization algorithm, which enables Zing to reuse work at procedure boundaries by extending interprocedural data-flow analysis algorithms from the compiler community to analyze concurrent programs.