Toward a decidable notion of sequential consistency
Jesse D. Bingham, Anne Condon, Alan J. Hu · 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 citealur1996 has shown that, in general, the SC verification problem is undecidable. We identify two aspects of the formulation found in citealur1996 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 phview window (VW), which retains information about a protocol's history, and we define the notion of a phVW-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 citeafek1993.