Dynamic Verification of Sequential Consistency

In the past decade, online businesses have created an increasing demand for
reliable, multiprocessor machines that can perform millions of transactions
without failure. The memory system is a key component in these machines. This
work describes a fault tolerant design for dynamically detecting memory system
errors on an end-to-end basis.

Correctness of a multiprocessor memory system is defined by a memory
consistency model, which specifies valid behavior for any given sequence of
memory requests. Previous work on error detection focused on verification of
individual components of the memory system such as caches, DRAMs and
interconnects under the assumption that the system works correctly as long as
all parts work correctly.  is a viable approach, it is difficult for
the designer to cover all possible error cases because many will appear at the
interfaces of different components. The design proposed in this work employs
direct verification of the observed execution sequence against the specified
consistency model. This end-to-end approach allows the detection of all
possible errors.

This talk presents two implementations of this approach along with experimental
results and evaluation using the Sequential Consistency (SC) model, which is
the oldest and simplest consistency model. The talk will conclude with a
discussion of current work toward extending the described design to more
relaxed consistency models.