Failure Transparency in Stateful Dataflow Systems (Technical Report)

TL;DR

This paper formally proves failure transparency in Apache Flink by modeling its failure handling mechanism, defining a novel observational explainability concept, and demonstrating that the failure-free model accurately abstracts failure-related behaviors.

Contribution

It introduces a formal proof of failure transparency for Apache Flink, modeling its failure handling and establishing correctness through observational semantics.

Findings

Formal proof of failure transparency for Apache Flink

Modeling of failure handling using small-step operational semantics

Establishment of liveness under fair execution assumptions

Abstract

Failure transparency enables users to reason about distributed systems at a higher level of abstraction, where complex failure-handling logic is hidden. This is especially true for stateful dataflow systems, which are the backbone of many cloud applications. In particular, this paper focuses on proving failure transparency in Apache Flink, a popular stateful dataflow system. Even though failure transparency is a critical aspect of Apache Flink, to date it has not been formally proven. Showing that the failure transparency mechanism is correct, however, is challenging due to the complexity of the mechanism itself. Nevertheless, this complexity can be effectively hidden behind a failure transparent programming interface. To show that Apache Flink is failure transparent, we model it in small-step operational semantics. Next, we provide a novel definition of failure transparency based on observational explainability, a concept which relates executions according to their observations. Finally, we provide a formal proof of failure transparency for the implementation model; i.e., we prove that the failure-free model correctly abstracts from the failure-related details of the implementation model. We also show liveness of the implementation model under a fair execution assumption. These results are a first step towards a verified stack for stateful dataflow systems.