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

摘要

The contribution of the paper is two-fold. W give a set of properties expressible as temporal logic formulas such that any system satisfying them is a sequentially con- sistent memory, and which is sufficiently precise such that every reasonable concrete system that implements a sequen- tially consistent memory satisfies these properties.