Systems distributed across several computers are essential for modern infrastruc- ture, and their reliability is reliant on the correctness of the constituent computers’ failure-handling protocols. Correctness in such systems is often understood as fail- ure transparency, a property that enables to use a system as if no failures occur in it; in other words, it states that there is a high-level model of the system, from which the failures are abstracted away. This work proves that failure transparency is provided by the Asynchronous Barrier Snapshotting protocol used in Apache Flink, a prominent distributed stateful dataflow system. This protocol is formal- ized in operational semantics for the first time in this thesis. As no prior definition of failure transparency is suitable for this formalization, a novel definition is pro- posed, applicable to systems expressed in small-step operational semantics with explicit failure-related rules. The work demonstrates how failure transparency can be proven by reasoning about each execution as a whole, presenting a proof tech- nique convenient for proofs about checkpoint-recovery protocols. The results are a first step towards a verified stateful dataflow programming stack.

System fördelade över flera datorer är väsentliga för den moderna infrastrukturen, och deras tillförlitlighet är baserad på korrektheten i protokollen som hanterar fel i de ingående datorerna. Riktigheten förstås ofta som failure transparency, en egenskap som gör det möjligt att använda ett system som om inga fel uppstår i det; med andra ord står det att det finns en högnivåmodell av systemet, från vilken miss- lyckandena abstraheras bort. Detta arbete bevisar att feltransparens tillhandahålls av protokollet Asynchronous Barrier Snapshotting som används i Apache Flink, en framträdande representant för distribuerade system med stateful dataflöde. Den första operativa semantiken för protokollet presenteras; Dessutom, eftersom det inte fanns någon definition av feltransparens för modeller i småstegsoperativ se- mantik, föreslås en ny definition, tillämplig på system uttryckta i småstegsoperativa semantik med explicita felrelaterade regler. Beviset visar hur misslyckandetrans- parens kan bevisas genom att resonera om varje exekvering som helhet, vilket gör det praktiskt i bevis om protokoll för återställning av checkpoints. Resultaten är ett första steg mot en verifierad stack för stateful dataflödesprogrammering.