  We present a framework for the efficient application of stateless model
checking (SMC) to concurrent programs running under the Release-Acquire (RA)
fragment of the C/C++11 memory model. Our approach is based on exploring the
possible program orders, which define the order in which instructions of a
thread are executed, and read-from relations, which specify how reads obtain
their values from writes. This is in contrast to previous approaches, which
also explore the possible coherence orders, i.e., orderings between conflicting
writes. Since unexpected test results such as program crashes or assertion
violations depend only on the read-from relation, we avoid a potentially
significant source of redundancy. Our framework is based on a novel technique
for determining whether a particular read-from relation is feasible under the
RA semantics. We define an SMC algorithm which is provably optimal in the sense
that it explores each program order and read-from relation exactly once. This
optimality result is strictly stronger than previous analogous optimality
results, which also take coherence order into account. We have implemented our
framework in the tool Tracer. Experiments show that Tracer can be significantly
faster than state-of-the-art tools that can handle the RA semantics.
