Title: Specifying and Verifying Correctness of Mergeable Replicated Data Types

Speaker: Kartik Nagar    (bio) (bio)

Kartik Nagar is an Assistant Professor at Department of CSE, IIT Madras. He completed his PhD from IISc Bangalore, after which he was a postdoc at Purdue University. His research interests are in Automated Formal Verification, Program Analysis and Programming Languages, with emphasis on developing practical verification techniques for concurrent and distributed systems.

When: Tuesday, 04 June 2024 at 1900 hrs (IST)       

Abstract:
Modern decentralized applications often use multiple replicas/copies of data, each of which can be independently operated, to minimize data access latency, provide fault tolerance and improve scalability. Mergeable Replicated Data Types (MRDTs) have emerged as a systematic approach to the problem of ensuring that replicas remain eventually consistent despite concurrent conflicting updates. MRDTs draw inspiration from the Git version control system, where each update creates a new version and any two versions can be merged explicitly through a user-defined merge function. The full flexibility offered by MRDTs in terms of creating and merging arbitrary versions severely complicates the design and development of correct MRDT implementations. In this talk, I will present two orthogonal approaches for specification and verification of MRDTs: a highly expressive, axiomatic event-based specification approach supported by a semi-automated verification procedure, and a more intuitive (but restrictive) linearizability based specification approach supported by fully automated verification.