Abstract: Despite recent advances, guaranteeing the correctness of large-scale distributed systems through formal verification remains a challenge. Network and node failures are inevitable in these systems, and handling failures at an appropriate level closely relates to the ease of formal reasoning. Unfortunately, existing approaches either completely hide these failures behind an atomic state machine replication (SMR) interface or expose all network-level details, making it difficult to reason about the core system properties. This talk discusses a novel, compositional, atomic distributed object (ADO) model for modeling and verifying strongly consistent distributed systems that combines the best of both options. The object-oriented API abstracts over protocol-specific details and decouples high-level correctness reasoning from implementation choices. We demonstrate that proving properties even of composite distributed systems can be straightforward thanks to the ADO model. Widely-used protocols, such as multi-Paxos, Raft, and Chain Replication, refine the ADO semantics and can be easily verified using the ADO model. The ADO model can be extended to model and verify the reconfiguration protocol of Raft and multi-Paxos and the consensus protocols under Byzantine environments.

Short Bio: Ji-Yong Shin is an Assistant Professor at the Khoury College of Computer Sciences at Northeastern University. He received his Ph.D. from Cornell University and was an Associate Research Scientist at Yale University. His research interest is designing systems, including distributed systems, cloud storage systems, and operating systems, and formally verifying them.