Stateless Model Checking for POWER

TL;DR

This paper introduces a novel framework for stateless model checking tailored to the POWER relaxed memory model, enabling systematic and efficient exploration of program behaviors with proven soundness and optimality.

Contribution

It develops a scheme to derive operational models from axiomatic ones and introduces RSMC, an efficient, sound, and optimal stateless model checking technique for POWER.

Findings

RSMC systematically explores all program behaviors exactly once.

The framework is applicable to C/pthreads programs.

The approach is proven to be sound and optimal.

Abstract

We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines several contributions. The first contribution is that we develop a scheme for systematically deriving operational execution models from existing axiomatic ones. The scheme is such that the derived execution models are well suited for efficient SMC. We apply our scheme to an axiomatic model of POWER. Our main contribution is a technique for efficient SMC, called Relaxed Stateless Model Checking (RSMC), which systematically explores the possible inequivalent executions of a program. RSMC is suitable for execution models obtained using our scheme. We prove that RSMC is sound and optimal for the POWER memory model, in the sense that each complete program behavior is explored exactly once. We show the feasibility of our technique by providing an implementation for programs written in C/pthreads.