Characterization of a sequentially consistent memory and verification of acache memory by abstraction

The contribution of the paper is two-fold. We give a set of properties expr essible as temporal logic formulas such that any system satisfying them is a sequentially consistent memory, and which is sufficiently precise such th at every reasonable concrete system that implements a sequentially consiste nt memory satisfies these properties. Then, we verify these properties on a distributed cache memory system by me ans of a verification method, based on the use of abstract interpretation w hich has been presented in previous papers and so far applied to finite sta te systems. The motivation for this paper was to show that it can also be s uccessfully applied to systems with an infinite state space. This is a revised and extended version of [Gra94].