Weak memory models have been studied extensively in the contexts of software,
hardware, and mappings between the two.  However, considerably less attention
has been paid to verifying how any specific hardware implementation correctly
enforces the memory model rules required by its architectural specification. 
This leaves a gap in correctness that has proven troublesome over the years;
there have been numerous instances (e.g., ARM load-load reordering, GPU fences,
Intel TSX, etc.) in which commercially-available hardware has been shown to
contain ordering bugs.  It also makes it more difficult to analyze, e.g.,
accelerators or low-level GPU ISAs which may not have a pre-existing or
well-defined hardware memory model specification.

To address this problem, I will begin by presenting PipeCheck, a tool and
methodology for specifying and verifying memory reordering behavior at the
microarchitecture level.  PipeCheck defines a multi-event axiomatic model of the
memory consistency behavior of one particular microarchitecture based on a
pipeline-specific set of microarchitectural axioms.  It uses this model to 1)
verify the behaviors of the given implementation against its hardware memory
model specification, and 2) identify cases in which the microarchitecture may be
stricter than necessary (e.g., an SC implementation of TSO) or weaker than
necessary (i.e., due to an implementation bug).  PipeCheck was nominated for the
Best Paper award at MICRO '14 and was chosen as an IEEE Micro Top Pick of 2014.
I will then discuss ongoing work to verify weak memory behavior in
microarchitecturally-relevant contexts such as partially incoherent caches,
virtual-to-physical address translation, and/or cache coherence protocols which
violate common formal notions of "coherence" and "from-reads".  I will conclude
with a broader analysis of the challenges of bridging the gap between formal
analysis and practical implementation.