Sequential consistency is a multiprocessor memory model of both
practical and theoretical importance. The general problem of
deciding whether a finite-state protocol implements sequential
consistency is undecidable. In this paper, however, we show that
for the protocols that arise in practice, proving sequential
consistency can be done automatically in theory and can be
reduced to regular language inclusion via a small amount of
manual effort. In particular, we introduce two ways to
construct finite-state "observers" that guarantee that a
protocol is sequentially consistent. From a theoretical
perspective, we are characterizing two classes of protocols
for which sequential consistency can be efficiently decided.
From a practical perspective, we are giving a methodology
for designing memory protocols such that sequential consistency
may be proven automatically via model-checking.