Timely Rollback: Specification and Verification

  • Martín Abadi
  • Michael IsardEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)


This paper presents a formal description and analysis of a technique for distributed rollback recovery. The setting for this work is a model for data-parallel computation with a notion of virtual time. The technique allows the selective undo of work at particular virtual times. A refinement theorem ensures the consistency of rollbacks.


State Machine Outgoing Edge Safety Property Visible Property Large Solution 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M.: The prophecy of undo. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 347–361. Springer, Heidelberg (2015) CrossRefGoogle Scholar
  2. 2.
    Abadi, M., Isard, M.: Timely dataflow: A model, in preparation (2014).
  3. 3.
    Abadi, M., Isard, M.: On the flow of data, information, and time. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 73–92. Springer, Heidelberg (2015) CrossRefGoogle Scholar
  4. 4.
    Abadi, M., Lamport, L.: The existence of refinement mappings. Theoretical Computer Science 82(2), 253–284 (1991)CrossRefzbMATHMathSciNetGoogle Scholar
  5. 5.
    Akidau, T., Balikov, A., Bekiroğlu, K., Chernyak, S., Haberman, J., Lax, R., McVeety, S., Mills, D., Nordstrom, P., Whittle, S.: MillWheel: Fault-tolerant stream processing at Internet scale. Proceedings of the VLDB Endowment 6(11), August 2013Google Scholar
  6. 6.
    Alvisi, L., Marzullo, K.: Message logging: Pessimistic, optimistic, causal, and optimal. IEEE Transactions on Software Engineering 24(2), 149–159 (1998)CrossRefGoogle Scholar
  7. 7.
    Elnozahy, E.N., Alvisi, L., Wang, Y., Johnson, D.B.: A survey of rollback-recovery protocols in message-passing systems. ACM Computing Surveys 34(3), 375–408 (2002)CrossRefGoogle Scholar
  8. 8.
    Jefferson, D.R.: Virtual time. ACM Transactions on Programming Languages and Systems 7(3), 404–425 (1985)CrossRefMathSciNetGoogle Scholar
  9. 9.
    Kahn, G.: The semantics of a simple language for parallel programming. In: IFIP Congress, pp. 471–475 (1974)Google Scholar
  10. 10.
    Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)Google Scholar
  11. 11.
    Murray, D.G., McSherry, F., Isaacs, R., Isard, M., Barham, P., Abadi, M.: Naiad: a timely dataflow system. In: ACM SIGOPS 24th Symposium on Operating Systems Principles, pp. 439–455 (2013)Google Scholar
  12. 12.
    Selinger, P.: First-order axioms for asynchrony. In: Mazurkiewicz, Antoni, Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 376–390. Springer, Heidelberg (1997) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.University of California at Santa CruzSanta CruzUSA
  2. 2.Microsoft ResearchMountain ViewUSA

Personalised recommendations