License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2015.1
URN: urn:nbn:de:0030-drops-54452
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5445/
Abadi, MartÃn
The Prophecy of Timely Rollback (Invited Talk)
Abstract
Techniques for rollback recovery play a central role in ensuring fault-tolerance in many distributed systems. This talk addresses the formal specification and analysis of those techniques. In particular, we will discuss the relevance of prophecy variables (auxiliary program variables whose values are defined in terms of current program state and future behavior) to reasoning about systems with undo operations. We will then focus on a model for data-parallel computation with a notion of virtual time. In this model, rollbacks allow the selective undo of work at particular virtual times. A refinement theorem ensures the consistency of rollbacks.
This talk is largely based on joint work with Michael Isard.
BibTeX - Entry
@InProceedings{abadi:LIPIcs:2015:5445,
author = {Mart{\'i}n Abadi},
title = {{The Prophecy of Timely Rollback (Invited Talk)}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {1--1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-90-3},
ISSN = {1868-8969},
year = {2015},
volume = {41},
editor = {Stephan Kreutzer},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5445},
URN = {urn:nbn:de:0030-drops-54452},
doi = {10.4230/LIPIcs.CSL.2015.1},
annote = {Keywords: Dataflow, refinement, rollback}
}
|
Keywords: |
|
Dataflow, refinement, rollback |
|
Collection: |
|
24th EACSL Annual Conference on Computer Science Logic (CSL 2015) |
|
Issue Date: |
|
2015 |
|
Date of publication: |
|
07.09.2015 |
