Lazy Caching in TLA

Peter Ladkin , Leslie Lamport , Bryan Olivier , Denis Roegel (1)

1 MODEL - MODEL (Méthodes formelles et applications)

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.

Mots clés: verification; algorithm; correction; algorithme; lazy caching

Domaines: Autre [cs.OH]

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