Abstract
Tracking the progress of computations can be both important and delicate in distributed systems. In a recent distributed algorithm for this purpose, each processor maintains a delayed view of the pending work, which is represented in terms of points in virtual time. This paper presents a formal specification of that algorithm in the temporal logic TLA, and describes a mechanically verified correctness proof of its main properties.
Chapter PDF
Similar content being viewed by others
References
Bonichon, R., Delahaye, D., Doligez, D.: Zenon: An extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 151–165. Springer, Heidelberg (2007)
Chandramouli, B., Goldstein, J., Maier, D.: On-the-fly progress detection in iterative stream queries. Proc. VLDB Endow. 2(1), 241–252 (2009)
Chandy, K.M., Misra, J.: Proofs of distributed algorithms: An exercise. In: Hoare, C.A.R. (ed.) Developments in Concurrency and Communication, pp. 305–332. Addison-Wesley, Boston (1990)
Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: Verifying safety properties with the tLA + proof system. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 142–148. Springer, Heidelberg (2010)
Jefferson, D.R.: Virtual time. ACM Trans. Program. Lang. Syst. 7(3), 404–425 (1985)
Lamport, L.: The TLA Toolbox, http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)
Merz, S., Vanzetto, H.: Automatic verification of TLA + proof obligations with SMT solvers. In: Bjørner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 289–303. Springer, Heidelberg (2012)
Naiad: Web page, http://research.microsoft.com/en-us/projects/naiad/
Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)
Rodeheffer, T.L.: The Naiad clock protocol: Specification, model checking, and correctness proof. Tech. Rep. MSR-TR-2013-20, Microsoft Research, Redmond (February 2013), http://research.microsoft.com/apps/pubs/?id=183826
Samadi, B.: Distributed Simulation, Algorithms and Performancs Analysis. Ph.D. thesis, University of California, Los Angeles (1985), Tech. Rep. CSD-850006, http://ftp.cs.ucla.edu/tech-report/198_-reports/850006.pdf
Tucker, P.A., Maier, D., Sheard, T., Fegaras, L.: Exploiting punctuation semantics in continuous data streams. IEEE Trans. Knowl. Data Eng. 15(3), 555–568 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Abadi, M., McSherry, F., Murray, D.G., Rodeheffer, T.L. (2013). Formal Analysis of a Distributed Algorithm for Tracking Progress. In: Beyer, D., Boreale, M. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2013 2013. Lecture Notes in Computer Science, vol 7892. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38592-6_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-38592-6_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38591-9
Online ISBN: 978-3-642-38592-6
eBook Packages: Computer ScienceComputer Science (R0)