The lazy caching algorithm of Afek, Brown, and Merrit (1993) allows the use of local caches with delayed updates. The memory model is not atomic (linearizable) but only sequentially consistent in the sense of Lamport. The late Rob Gerth has made proving sequential consistency for the lazy caching algorithm into a benchmark for verification models.
We have used our theory of specifications and simulations to prove the correctness of this algorithm. This has resulted in two papers:
Since we follow the approach of Lamport and others, liveness is a critical aspect of our specification of sequential consistency. The second paper is needed to introduce and prove soundness of the new concept of splitting simulations. The proofs of both papers have been constructed and verified with the proof assistant PVS. Available is a proof script for both papers and a shorter proof script for the first paper. In the second verification, the algorithm specific aspects take more than 90 % of the CPU time.
Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink