Lazy caching in TLA

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Lazy caching in TLA

Source

Distributed Computing archive
Volume 12 , Issue 2-3 (June 1999) table of contents
Special issue: Verification of lazy caching

Pages: 151 - 174

Year of Publication: 1999

ISSN:0178-2770

Authors

Peter Ladkin	Universität Bielefeld, Technische Fakultät, Postfach 10 01 31, D-33501 Bielefeld, Germany
Leslie Lamport	Sytems Research Center, i30 Lytton Avenue, Palo Alto, CA
Bryan Olivier	Kattenburgergracht 17, Appt. E, NL-1018 KN Amsterdam, The Netherlands
Denis Roegel	LORIA, Campus Scientifique, B.P. 239, F-54506 Vandeouvre-les-Nancy Cedex, France

Publisher

Springer-Verlag London, UK

Bibliometrics

Downloads (6 Weeks): n/a, Downloads (12 Months): n/a, Citation Count: 4

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	10.1007/s004460050063

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Martín Abadi , Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, v.82 n.2, p.253-284, May 31, 1991 [doi>10.1016/0304-3975(91)90224-P]
	2	2. Abadi M, Lamport L, Merz S: Refining specifications. To appear.
	3	Yehuda Afek , Geoffrey Brown , Michael Merritt, Lazy caching, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.182-205, Jan. 1993 [doi>10.1145/151646.151651]
	4	4. Ashcroft EA: Proving assertions about parallel programs. J Comput Syst Sci 10:110-135 (1975).
	5	K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
	6	Richard A. De Millo , Richard J. Lipton , Alan J. Perlis, Social processes and proofs of theorems and programs, Communications of the ACM, v.22 n.5, p.271-280, May 1979 [doi>10.1145/359104.359106]
	7	Urban Engberg , Peter Grønning , Leslie Lamport, Mechanical Verification of Concurrent Systems with TLA, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.44-55, June 29-July 01, 1992
	8	Rob Gerth, Sequential consistency and the lazy caching algorithm, Distributed Computing, v.12 n.2/3, p.57-59, June 1999 [doi>10.1007/s004460050057]
	9	9. Lam SS, Shankar AU: Protocol verification via projections. IEEE Transactions on Software Engineering SE-10(4):325-342 (1984).
	10	10. Lamport L: What good is temporal logic? In: Mason REA (ed) Information Processing 83: Proceedings of the IFIP 9th World Congress, pp 657-668, Paris, September 1983. IFIP, North-Holland, Amsterdam.
	11	Leslie Lamport, A simple approach to specifying concurrent systems, Communications of the ACM, v.32 n.1, p.32-45, Jan. 1989 [doi>10.1145/63238.63240]
	12	Leslie Lamport, Hybrid Systems in TLA+, Hybrid Systems, p.77-102, January 1993
	13	13. Lamport L: How to write a long formula. Formal Aspects of Computing 6:580-584 (1994). First appeared as Research Report 119, Digital Equipment Corporation, Systems Research Center.
	14	Leslie Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.3, p.872-923, May 1994 [doi>10.1145/177492.177726]
	15	15. Lamport L: How to write a proof. American Mathematical Monthly 102(7):600-608 (1995).
	16	Leslie Lamport, How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor, IEEE Transactions on Computers, v.46 n.7, p.779-782, July 1997 [doi>10.1109/12.599898]
	17	Leslie Lamport , Stephan Merz, Specifying and Verifying Fault-Tolerant Systems, Proceedings of the Third International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.41-76, September 19-23, 1994
	18	Leslie Lamport , Lawrence C. Paulson, Should your specification language be typed, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.502-526, May 1999 [doi>10.1145/319301.319317]
	19	Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1996
	20	Zohar Manna , Amir Pnueli, Completing the temporal picture, Theoretical Computer Science, v.83 n.1, p.97-130, June 21, 1991
	21	Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
	22	22. Owicki S, Gries D: An axiomatic proof technique for parallel programs I. Acta Informatica 6(4):319-340 (1976).

CITED BY 4

	Rajnish Ghughal , Abdel Mokkedem , Ratan Nalumasu , Ganesh Gopalakrishnan, Using “test model-checking” to verify the Runway-PA8000 memory model, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.231-239, June 28-July 02, 1998, Puerto Vallarta, Mexico
	Shaz Qadeer, Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking, IEEE Transactions on Parallel and Distributed Systems, v.14 n.8, p.730-741, August 2003
	Wim H. Hesselink, Eternity variables to prove simulation of specifications, ACM Transactions on Computational Logic (TOCL), v.6 n.1, p.175-201, January 2005
	Wim H. Hesselink, Universal extensions to simulate specifications, Information and Computation, v.206 n.1, p.108-128, January, 2008