  In this work, we present a family of operational semantics that gradually
approximates the realistic program behaviors in the C/C++11 memory model. Each
semantics in our framework is built by elaborating and combining two simple
ingredients: viewfronts and operation buffers. Viewfronts allow us to express
the spatial aspect of thread interaction, i.e., which values a thread can read,
while operation buffers enable manipulation with the temporal execution aspect,
i.e., determining the order in which the results of certain operations can be
observed by concurrently running threads.
  Starting from a simple abstract state machine, through a series of gradual
refinements of the abstract state, we capture such language aspects and
synchronization primitives as release/acquire atomics, sequentially-consistent
and non-atomic memory accesses, also providing a semantics for relaxed atomics,
while avoiding the Out-of-Thin-Air problem. To the best of our knowledge, this
is the first formal and executable operational semantics of C11 capable of
expressing all essential concurrent aspects of the standard.
  We illustrate our approach via a number of characteristic examples, relating
the observed behaviors to those of standard litmus test programs from the
literature. We provide an executable implementation of the semantics in PLT
Redex, along with a number of implemented litmus tests and examples, and
showcase our prototype on a large case study: randomized testing and debugging
of a realistic Read-Copy-Update data structure.
