Skip to Main content Skip to Navigation
Journal articles

Lazy Caching in TLA

Peter Ladkin Leslie Lamport Bryan Olivier Denis Roegel 1
1 MODEL - MODEL (Méthodes formelles et applications)
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We address the problem, proposed by Gerth, of verifying that a simplified version of the lazy caching algorithm of Afek, Brown, and Merritt is sequentially consistent. We specify the algorithm and sequential consistency in TLA+, a formal specification language based on TLA (the Temporal Logic of Actions). We then describe how to construct and check a formal TLA correctness proof.
Document type :
Journal articles
Complete list of metadata
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:41:03 AM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM


  • HAL Id : inria-00098997, version 1



Peter Ladkin, Leslie Lamport, Bryan Olivier, Denis Roegel. Lazy Caching in TLA. Distributed Computing, Springer Verlag, 1999, 12 (2-3), pp.151-174. ⟨inria-00098997⟩



Record views