Automated Reasoning for Replicated Systems

Jul 8, 2020

For global-scale applications such as Amazon, Twitter, Facebook, etc. with users distributed across the world, in order to provide a uniform low-latency and always available service, the application data needs to replicated at multiple servers across the world. Such replicated systems also facilitate other useful properties such as better scalability and fault tolerance, but they are very hard to program since they offer a completely different memory model to the programmers. Since the same data at different replicas can be concurrently updated and the updates can be applied in different orders at different replicas, this can result in subtle concurrency bugs for the applications running on top of replicated systems which can be hard to find through testing-based approaches. In this project, we proposed a number of automated verification techniques to reason about correctness of programs running on top of replicated systems.

Representative Publications:

  1. Semantics, Specification and Automated Verification of Concurrent Libraries in Replicated Systems. Kartik Nagar, Prasita Mukherjee and Suresh Jagannathan. CAV 20
  2. CLOTHO : Directed Test Generation for Weakly Consistent Database Systems. Kia Rahmani, Kartik Nagar, Benjamin Delaware and Suresh Jagannathan. OOPSLA 19.
  3. Automated Parameterized Verification of CRDTs. Kartik Nagar and Suresh Jagannathan. CAV 19.
  4. Automated Detection of Serializability Violations under Weak Consistency. Kartik Nagar and Suresh Jagannathan. CONCUR 18.
  5. Alone Together: Compositional Reasoning and Inference for Weak Isolation. Gowtham Kaki, Kartik Nagar, Mahsa Najafzadeh and Suresh Jagannathan. POPL 18.