Context-Bounded Model Checking for POWER

TL;DR

This paper introduces a new context-bounded analysis method for POWER memory models, reducing the problem to sequential consistency and enabling bug detection with existing tools like CBMC.

Contribution

It generalizes context-bounding to POWER, providing a polynomial reduction to SC reachability, and implements a prototype tool for practical analysis.

Findings

Polynomial reduction from POWER to SC reachability.

Feasibility demonstrated on benchmark programs.

Prototype tool successfully applied to real-world examples.

Abstract

We propose an under-approximate reachability analysis algorithm for programs running under the POWER memory model, in the spirit of the work on context-bounded analysis intitiated by Qadeer et al. in 2005 for detecting bugs in concurrent programs (supposed to be running under the classical SC model). To that end, we first introduce a new notion of context-bounding that is suitable for reasoning about computations under POWER, which generalizes the one defined by Atig et al. in 2011 for the TSO memory model. Then, we provide a polynomial size reduction of the context-bounded state reachability problem under POWER to the same problem under SC: Given an input concurrent program P, our method produces a concurrent program P' such that, for a fixed number of context switches, running P' under SC yields the same set of reachable states as running P under POWER. The generated program P' contains the same number of processes as P, and operates on the same data domain. By leveraging the standard model checker CBMC, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our approach.