  We introduce a denotational semantic framework for shared-memory concurrent
programs in a C11-style memory model. This denotational approach is an
alternative to techniques based on "execution graphs" and axiomatizations, and
it allows for compositional reasoning. Our semantics generalizes from traces
(sequences of actions) to pomsets (partial orders of actions): instead of
traces and interleaving, we embrace "true" concurrency. We build on techniques
from our prior work that gives a denotational semantics to SPARC TSO. We add
support for C11's wider range of memory orderings, e.g., acquire-release and
relaxed, and support for local variables and various synchronization
primitives, while eliminating significant amounts of technical bookkeeping. Our
approach features two main components. We first give programs a syntax-directed
denotation in terms of sets of pomsets of memory actions. We then give a
race-detecting executional interpretation of pomsets using footprints and a
local view of state.
