  We present a technique for efficient stateless model checking of programs
that execute under the relaxed memory models TSO and PSO. The basis for our
technique is a novel representation of executions under TSO and PSO, called
chronological traces. Chronological traces induce a partial order relation on
relaxed memory executions, capturing dependencies that are needed to represent
the interaction via shared variables. They are optimal in the sense that they
only distinguish computations that are inequivalent under the widely-used
representation by Shasha and Snir. This allows an optimal dynamic partial order
reduction algorithm to explore a minimal number of executions while still
guaranteeing full coverage. We apply our techniques to check, under the TSO and
PSO memory models, LLVM assembly produced for C/pthreads programs. Our
experiments show that our technique reduces the verification effort for relaxed
memory models to be almost that for the standard model of sequential
consistency. In many cases, our implementation significantly outperforms other
comparable tools.
