### 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 formalize this progress tracking protocol and verify its safety. Our formalization is described in detail in our forthcoming ITP'21 paper.

### License

BSD License

### Topics

- Computer science/Algorithms/Distributed

### Session Progress_Tracking

- Auxiliary
- Exchange_Abadi
- Exchange
- Antichain
- Graph
- Propagate
- Combined

### Depends on

- Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

## Cite

×

Progress_Tracking-AFP

    @article{Progress_Tracking-AFP,
      author  = {Matthias Brun and Sára Decova and Andrea Lattuada and Dmitriy Traytel},
      title   = {Formalization of Timely Dataflow's Progress Tracking Protocol},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Progress_Tracking.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Apr 16, 2021 : Isabelle2021