Automatically Verifying Replicated Data Types
COM3 Level 2
MR21, COM3 02-61
Abstract:
Replicated Data Types (RDTs) have emerged as a principled approach for developing replicated implementations of basic data structures such as counter, flag, set, map, etc. While the correctness of RDTs is generally specified using the notion of strong eventual consistency--which guarantees that replicas that have received the same set of updates would converge to the same state--a more expressive specification which relates the converged state to updates received at a replica would be more beneficial to RDT users. Replication-aware linearizability is one such specification, which requires all replicas to always be in a state which can be obtained by linearizing the updates received at the replica. In this talk, I discuss recent work on developing a novel fully automated technique for verifying replication-aware linearizability for Mergeable Replicated Data Types (MRDTs).
Bio:
KC Sivaramakrishnan is an Assistant Professor in the Department of Computer Science and Engineering at IIT Madras and the CTO at Tarides. He is interested in the intersection of programming languages and (concurrent, distributed, parallel, operating, secure) systems. He led the work on Multicore OCaml, a decade-long project to add concurrency and parallelism to the OCaml programming language. Multicore OCaml was merged into the OCaml language and released as part of OCaml 5.0. In the past, KC was a senior research fellow at the University of Cambridge Computer Lab, and he obtained his PhD and MS from Purdue University. His awards include the SIGPLAN Programming Languages Software Award, Royal Commission for the Exhibition of 1851 Fellowship, Darwin College Cambridge research fellowship, Maurice H. Halstead Memorial award for outstanding research in software engineering, and distinguished paper awards at ICFP and PADL.