Extending Memory Consistency of Finite Prefixes to Infinite Computations

Infinite computations are widely used to model arbitrarily long computations of infinite-state systems. Certain properties have both a finitary version, applying only to finite prefixes of computations, and an infinitary version. It is tempting to verify these properties for finite computations only, and then conclude that the infinitary version of the property holds too. This generalization is sound for safety properties, but to verify non-safety properties “by prefixes”, one must justify the generalization step. This paper studies how this can be done for sequential consistency of shared memory protocols. In the related literature, this generalization is sometimes done informally, if at all. We define, independently of any specific shared memory algorithm, sufficient conditions so that sequential consistency can be verified by finite prefixes. These conditions are expected to be satisfied by any reasonable shared memory system, regardless of the consistency model.