  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.
