Toward A Decidable Notion of Sequential Consistency

Jesse D. Bingham, Anne Condon, Alan J. Hu

15th Annual ACM Symposium on Parallelism in Algorithms and Architectures,
pp. 304-314, 2003.

A memory model specifies a correctness requirement for a distributed
shared memory protocol.  Sequential consistency (SC) is the most widely
researched model; previous work~\cite{alur1996} has shown that, in
general, the SC verification problem is undecidable.  We identify two
aspects of the formulation found in~\cite{alur1996} that we consider to
be highly unnatural; we call these non-prefix-closedness and prophetic
inheritance.  We conjecture that preclusion of such behavior yields a
decidable version of SC, which we call decisive sequential consistency
(DSC).  We also introduce a structure called a \emph{view window} (VW),
which retains information about a protocol's history, and we define the
notion of a \emph{VW-bound}, which essentially bounds the size of the
VWs needed to maintain DSC.  We prove that the class of DSC protocols
with VW-bound $k$ is decidable; left conjectured is the hypothesis that
all DSC protocols have such a bound, and further that the bound is
computable from the protocol description.  This hypothesis is true for
all real protocols known to us; we verify its truth for the Lazy
Caching protocol~\cite{afek1993}.