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. © 2013 IFIP International Federation for Information Processing.
CITATION STYLE
Abadi, M., McSherry, F., Murray, D. G., & Rodeheffer, T. L. (2013). Formal analysis of a distributed algorithm for tracking progress. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7892 LNCS, pp. 5–19). https://doi.org/10.1007/978-3-642-38592-6_2
Mendeley helps you to discover research relevant for your work.