Relational Reasoning for Mergeable Replicated Data Types

Abstract: Programming geo-replicated distributed systems is challenging given the complexity of reasoning about different evolving states on different replicas. Existing approaches to this problem impose a significant burden on application developers to consider the effect of how operations performed on one replica are witnessed and applied on others. To alleviate these challenges, we present a fundamentally different approach to programming in the presence of replicated state. Our insight is based on the use of invertible relational specifications of an inductively-defined data type as a mechanism to capture salient aspects of the data type relevant to how its different instances can be safely merged in a replicated environment. Importantly, because these specifications only address a data type's (static) structural properties, their formulation does not require exposing low-level system-level details concerning asynchrony, replication, visibility, etc. As a consequence, our framework enables the correct-by-construction synthesis of rich merge functions over arbitrarily complex (i.e., composable) data types. In this talk, I'll show that the use of a rich relational specification language allows us to extract sufficient conditions to automatically derive merge functions that have meaningful non-trivial convergence properties.

Bio: KC Sivaramakrishnan is an Assistant Professor in the Computer Science and Engineering department at Indian Institute of Technology, Madras. He works on the intersection of Programming Languages and (Concurrent, Parallel, Distributed) Systems. He leads the Multicore OCaml project which extends the OCaml programming language with support for lightweight concurrency and shared memory parallelism. He led the development of MultiMLton, a multicore-aware runtime for MLton Standard ML compiler and Quelea, a language for programming over distributed databases. He has held research positions at University of Cambridge, Microsoft Research Cambridge, and Samsung Research. He obtained his PhD from Purdue University developing functional programming abstractions for weakly consistent systems.