Title of article
Lazy caching in TLA
Author/Authors
Ladkin، Peter نويسنده , , Lamport، Leslie نويسنده , , Olivier، Bryan نويسنده , , Roegel، Denis نويسنده ,
Issue Information
روزنامه با شماره پیاپی سال 1999
Pages
-150
From page
151
To page
0
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.
Keywords
CSP , Verification , Sequential consistency , Lazy caching protocol , Specification
Journal title
DISTRIBUTED COMPUTING
Serial Year
1999
Journal title
DISTRIBUTED COMPUTING
Record number
6209
Link To Document