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
Go to the corresponding LIPIcs Volume Portal

Abadi, Martín

The Prophecy of Timely Rollback (Invited Talk)

41.pdf (0.2 MB)


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

  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 =		{},
  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

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI