Summary.
The contribution of the paper is two-fold. We give a set of properties expressible as temporal logic formulas such that any system satisfying them is a sequentially consistent memory, and which is sufficiently precise such that every reasonable concrete system that implements a sequentially consistent memory satisfies these properties. Then, we verify these properties on a distributed cache memory system by means of a verification method, based on the use of abstract interpretation which has been presented in previous papers and so far applied to finite state systems. The motivation for this paper was to show that it can also be successfully applied to systems with an infinite state space. This is a revised and extended version of [GrA94].
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Graf, S. Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. Distrib Comput 12, 75–90 (1999). https://doi.org/10.1007/s004460050059
Issue Date:
DOI: https://doi.org/10.1007/s004460050059