In this paper we propose a methodology for verifying the sequential
consistency of caching algorithms.
The scheme combines timestamping and an auxiliary history table
to construct a serial execution `matching' any given execution of the
algorithm.
We believe that this approach is applicable to an interesting class of
sequentially consistent algorithms in which the buffering of cache
updates allows stale values to be read from cache.
We illustrate this methodology by verifying the high level specifications
of the lazy caching and ring algorithms.
