  We investigate the problem of runtime analysis of C11 programs under
Multi-Copy-Atomic semantics (MCA). Under MCA, one can analyze program outcomes
solely through interleaving and reordering of thread events. As a result,
obtaining intuitive explanations of program outcomes becomes straightforward.
Newer versions of ARM (ARMv8 and later), Alpha, and Intel's x-86 support MCA.
Our tests reveal that state-of-the-art dynamic verification techniques that
analyze program executions under the C11 memory model generate safety property
violations that can be interpreted as false alarms under MCA semantics. Sorting
the true from false violations puts an undesirable burden on the user. In this
work, we provide a dynamic verification technique (MoCA) to analyze C11 program
executions which are permitted under the MCA model. We design a happens-before
relation and introduce coherence rules to capture precisely those C11 program
executions which are allowed under the MCA model. MoCA's exploration of the
state-space is based on the state-of-the-art dynamic verification algorithm,
source-DPOR. Our experiments validate that MoCA captures all coherent C11
program executions, and is precise for the MCA model.
