Flo: a Semantic Foundation for Progressive Stream Processing
summary
Flo formalizes two semantic guarantees: streaming progress (operators must emit meaningful partial outputs for unbounded inputs) and eager execution (operators remain deterministic under dynamically arriving data). A lightweight type system classifies bounded vs unbounded streams, forbids top-level fold on unbounded streams, and enables nested graphs/windows. Proof obligations are local to each operator; composition yields deterministic, fresh outputs (paper proves this). A prototype embeds these concepts as Rust types in Hydro (used to implement Paxos-like components), and models Flink, LVars, and DBSP semantics.
AI-written summary · about
chapters (10)
- 0:00Flo introduction
- 1:29Streams and design principles
- 2:32Flow as meta-language
- 3:57Correctness proof obligations
- 4:58Determinism with eager execution
- 8:49Streaming progress behavior
- 10:14Bounded vs unbounded streams
- 11:41Nested graphs processing
- 12:22Hydro implementation
- 13:49Q&A
related talks
01h 02mHydroflow: A Compiler Target for Fast, Correct Distributed Programs
19mFlow: An Introduction
38mDeploying Stateful FaaS on Streaming Dataflows
43mStream Processing and Applications in the Modern Age
19mFunctional Meaning for Parallel Streaming
24mStateful Functions: Flexible like a Microservice, Consistent like a Monolith
38mSelf-managed and automatically reconfigurable stream processing
38mPolyglot Actor Model on Flink Stateful Functions