Lazy caching in TLA

descriptionPublicationkeyboard_double_arrow_right Article 01 May 1999Publisher:Springer Science and Business Media LLCJournal:Distributed Computing, volume 12, pages 151-174 (issn: 0178-2770,

Copyright policy )

Authors: Ladkin, Peter; Lamport, Leslie; Olivier, Bryan; Roegel, Denis;

doi: 10.1007/s004460050063

Lazy caching in TLA

- Summary
- Subjects
- External Databases
  (1)
- Metrics

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.

Related Organizations

Keywords

lazy caching, [INFO.INFO-OH] Computer Science [cs]/Other [cs.OH], algorithm, correction, verification, algorithme

2inv

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	21
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Top 10%
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Top 10%