Timely Rollback: Specification and Verification

详细信息    查看全文

• 作者：Mart铆n Abadi (16)
  Michael Isard (17)
  
  16. University of California at Santa Cruz ; Santa Cruz ; California ; USA
  17. Microsoft Research ; Mountain View ; California ; USA
  
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9058
• 期：1
• 页码：19-34
• 全文大小：273 KB
• 参考文献：1. Abadi, M The prophecy of undo. In: Egyed, A, Schaefer, I eds. (2015) Fundamental Approaches to Software Engineering. Springer, Heidelberg, pp. 347-361 CrossRef
  2. Abadi, M., Isard, M.: Timely dataflow: A model, in preparation (2014). https://users.soe.ucsc.edu/~abadi/allpapers-chron.html
  3. Abadi, M, Isard, M On the flow of data, information, and time. In: Focardi, R, Myers, A eds. (2015) Principles of Security and Trust. Springer, Heidelberg, pp. 73-92 CrossRef
  4. Abadi, M, Lamport, L (1991) The existence of refinement mappings. Theoretical Computer Science 82: pp. 253-284 CrossRef
  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 2013
  6. Alvisi, L, Marzullo, K (1998) Message logging: Pessimistic, optimistic, causal, and optimal. IEEE Transactions on Software Engineering 24: pp. 149-159 CrossRef
  7. Elnozahy, EN, Alvisi, L, Wang, Y, Johnson, DB (2002) A survey of rollback-recovery protocols in message-passing systems. ACM Computing Surveys 34: pp. 375-408 CrossRef
  8. Jefferson, DR (1985) Virtual time. ACM Transactions on Programming Languages and Systems 7: pp. 404-425 CrossRef
  9. Kahn, G.: The semantics of a simple language for parallel programming. In: IFIP Congress, pp. 471鈥?75 (1974)
  10. Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002)
  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鈥?55 (2013)
  12. Selinger, P First-order axioms for asynchrony. In: Mazurkiewicz, Antoni, Winkowski, J eds. (1997) CONCUR鈥?7: Concurrency Theory. Springer, Heidelberg, pp. 376-390 CrossRef
  
• 作者单位：NASA Formal Methods
• 丛书名：978-3-319-17523-2
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

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.