Recent projects
Aegean: Replication beyond the client-server model
Aegean is a new approach that allows fault-tolerant replication to be implemented beyond the confines of the client-server model. In today's computing, where services are rarely standalone, traditional replication protocols such as Primary-Backup, Paxos, and PBFT are not directly applicable, as they were designed for the client-server model. When services interact, these protocols run into a number of problems, affecting both correctness and performance. In this project, we rethink the design of replication protocols in the presence of interactions between services and introduce new techniques that accommodate such interactions safely and efficiently. Our experiments so far show that a prototype implementation of Aegean not only ensures correctness in the presence of service interactions, but can further improve throughput by an order of magnitude.
Publications
Remzi Can Aksoy, Manos Kapritsos, Aegean: Replication Beyond the Client-Server Model, 27th ACM Symposium on Operating Systems Principles (SOSP '19)[PDF] [Video] [Slides]
I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols
Designing and implementing distributed systems correctly is a very challenging task. Formal verification has been successfully used to prove the correctness of distributed systems. At the heart of formal verification lies a computer-checked proof with an inductive invariant. Finding this inductive invariant, however, is the most difficult part of the proof. Alas, current proof techniques require inductive invariants to be found manually---and painstakingly---by the developer. In this project we propose a new approach, Incremental Inference of Inductive Invariants (I4), to automatically generate inductive invariants for distributed protocols. The essence of our idea is simple: the inductive invariant of a finite instance of the protocol can be used to infer a general inductive invariant for the infinite distributed protocol. In I4, we create a finite instance of the protocol; use a model checking tool to automatically derive the inductive invariant for this finite instance; and generalize this invariant to an inductive invariant for the infinite protocol. Our experiments show that I4 can prove the correctness of several distributed protocols like Chord, 2PC and Transaction Chains with little to no human effort.
Publications
Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, Karem A. Sakallah, I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols, 27th ACM Symposium on Operating Systems Principles (SOSP '19)[PDF] [Video] [Slides]
Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, Karem A. Sakallah, Towards Automatic Inference of Inductive Invariants, 17th Workshop on Hot Topics in Operating Systems (HotOS '19)
[PDF] [Slides]