1. 1

Abstract: “Implementing correct and deterministic parallel programs is challenging. Even though concurrency constructs exist in popular programming languages to facilitate the task of deterministic parallel programming, they are often too low level, or do not compose well due to underlying blocking mechanisms. In this report, we present the detailed proofs of the linearizability, lock-freedom, and determinism properties of FlowPools, a deterministic concurrent dataflow abstraction presented in [1].”