Verified Progress Tracking for Timely Dataflow.
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Documents
- Verified Progress Tracking for Timely Dataflow
Final published version, 781 KB, PDF document
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.
Original language | English |
---|---|
Title of host publication | 12th International Conference on Interactive Theorem Proving (ITP 2021) |
Editors | Liron Cohen, Cezary Kaliszyk |
Publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
Publication date | 2021 |
Pages | 1-20 |
Article number | 10 |
ISBN (Print) | {978-3-95977-188-7 |
DOIs | |
Publication status | Published - 2021 |
Event | 12th International Conference on Interactive Theorem Proving - ITP 2021 - Rome / (Virtual Conference), Italy Duration: 29 Jun 2021 → 1 Jul 2021 |
Conference
Conference | 12th International Conference on Interactive Theorem Proving - ITP 2021 |
---|---|
Land | Italy |
By | Rome / (Virtual Conference) |
Periode | 29/06/2021 → 01/07/2021 |
Series | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Volume | 193 |
ISSN | 1868-8969 |
Number of downloads are based on statistics from Google Scholar and www.ku.dk
No data available
ID: 282091882