Sciweavers

ACTA
2006

Refinement verification of the lazy caching algorithm

14 years 1 days ago
Refinement verification of the lazy caching algorithm
The lazy caching algorithm of Afek, Brown, and Merrit (1993) is a protocol that allows the use of local caches with delayed updates. It results in a memory model that is not atomic (linearizable) but only sequentially consistent as defined by Lamport. In Distributed Computing 12 (1999), specifying and proving sequential consistency for the lazy caching algorithm was made into a benchmark for verification models. The present note contains such a specification and proof. It provides a simulation from ementation to the abstract specification. The concrete verification only relies on the state space and the next-state relation. All behavioural aspects are treated in theories independent of the specific algorithm. The proofs of the underlying theories and of the concrete algorithm have been verified with the proof assistant PVS. Key words: Sequential consistency, cache coherence, mechanical verification, simulation, weak fairness
Wim H. Hesselink
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2006
Where ACTA
Authors Wim H. Hesselink
Comments (0)