Verified Progress Tracking for Timely Dataflow.

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Standard

Verified Progress Tracking for Timely Dataflow. / Brun, Matthias; Decova, Sára; Lattuada, Andrea; Traytel, Dmitriy.

12th International Conference on Interactive Theorem Proving (ITP 2021). ed. / Liron Cohen; Cezary Kaliszyk. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. p. 1-20 10 (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 193).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Harvard

Brun, M, Decova, S, Lattuada, A & Traytel, D 2021, Verified Progress Tracking for Timely Dataflow. in L Cohen & C Kaliszyk (eds), 12th International Conference on Interactive Theorem Proving (ITP 2021)., 10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics, LIPIcs, vol. 193, pp. 1-20, 12th International Conference on
Interactive Theorem Proving - ITP 2021, Rome / (Virtual Conference), Italy, 29/06/2021. https://doi.org/10.4230/LIPICS.ITP.2021.10

APA

Brun, M., Decova, S., Lattuada, A., & Traytel, D. (2021). Verified Progress Tracking for Timely Dataflow. In L. Cohen, & C. Kaliszyk (Eds.), 12th International Conference on Interactive Theorem Proving (ITP 2021) (pp. 1-20). [10] Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Leibniz International Proceedings in Informatics, LIPIcs Vol. 193 https://doi.org/10.4230/LIPICS.ITP.2021.10

Vancouver

Brun M, Decova S, Lattuada A, Traytel D. Verified Progress Tracking for Timely Dataflow. In Cohen L, Kaliszyk C, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. 2021. p. 1-20. 10. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 193). https://doi.org/10.4230/LIPICS.ITP.2021.10

Author

Brun, Matthias ; Decova, Sára ; Lattuada, Andrea ; Traytel, Dmitriy. / Verified Progress Tracking for Timely Dataflow. 12th International Conference on Interactive Theorem Proving (ITP 2021). editor / Liron Cohen ; Cezary Kaliszyk. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. pp. 1-20 (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 193).

Bibtex

@inproceedings{01041a186e384febac9e5c17add0c98e,
title = "Verified Progress Tracking for Timely Dataflow.",
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{\textquoteright}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.",
author = "Matthias Brun and S{\'a}ra Decova and Andrea Lattuada and Dmitriy Traytel",
year = "2021",
doi = "10.4230/LIPICS.ITP.2021.10",
language = "English",
isbn = "{978-3-95977-188-7",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",
pages = "1--20",
editor = "Cohen, {Liron } and Kaliszyk, {Cezary }",
booktitle = "12th International Conference on Interactive Theorem Proving (ITP 2021)",
note = "12th International Conference on<br/>Interactive Theorem Proving - ITP 2021 ; Conference date: 29-06-2021 Through 01-07-2021",

}

RIS

TY - GEN

T1 - Verified Progress Tracking for Timely Dataflow.

AU - Brun, Matthias

AU - Decova, Sára

AU - Lattuada, Andrea

AU - Traytel, Dmitriy

PY - 2021

Y1 - 2021

N2 - 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.

AB - 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.

U2 - 10.4230/LIPICS.ITP.2021.10

DO - 10.4230/LIPICS.ITP.2021.10

M3 - Article in proceedings

SN - {978-3-95977-188-7

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 1

EP - 20

BT - 12th International Conference on Interactive Theorem Proving (ITP 2021)

A2 - Cohen, Liron

A2 - Kaliszyk, Cezary

PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik

T2 - 12th International Conference on<br/>Interactive Theorem Proving - ITP 2021

Y2 - 29 June 2021 through 1 July 2021

ER -

ID: 282091882