License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.10
URN: urn:nbn:de:0030-drops-139057
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13905/
Go to the corresponding LIPIcs Volume Portal

Brun, Matthias ; Decova, Sára ; Lattuada, Andrea ; Traytel, Dmitriy

Verified Progress Tracking for Timely Dataflow

pdf-format:
LIPIcs-ITP-2021-10.pdf (0.8 MB)

Abstract

Large-scale stream processing systems often follow the dataflow paradigm, which enforces a program structure that exposes a high degree of parallelism. The Timely Dataflow distributed system supports expressive cyclic dataflows for which it offers low-latency data- and pipeline-parallel stream processing. To achieve high expressiveness and performance, Timely Dataflow uses an intricate distributed protocol for tracking the computation’s progress. We modeled the progress tracking protocol as a combination of two independent transition systems in the Isabelle/HOL proof assistant. We specified and verified the safety of the two components and of the combined protocol. To this end, we identified abstract assumptions on dataflow programs that are sufficient for safety and were not previously formalized.

BibTeX - Entry

@InProceedings{brun_et_al:LIPIcs.ITP.2021.10,
  author =	{Brun, Matthias and Decova, S\'{a}ra and Lattuada, Andrea and Traytel, Dmitriy},
  title =	{{Verified Progress Tracking for Timely Dataflow}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{10:1--10:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13905},
  URN =		{urn:nbn:de:0030-drops-139057},
  doi =		{10.4230/LIPIcs.ITP.2021.10},
  annote =	{Keywords: safety, distributed systems, timely dataflow, Isabelle/HOL}
}

Keywords: safety, distributed systems, timely dataflow, Isabelle/HOL
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: Software (Isabelle Formalization): https://www.isa-afp.org/entries/Progress_Tracking.html

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