Replication Coordination Analysis and Synthesis

Speaker Name: 
Mohsen Lesani
Speaker Title: 
Assistant Professor
Speaker Organization: 
UC Riverside
Start Time: 
Wednesday, December 12, 2018 - 10:00am
End Time: 
Wednesday, December 12, 2018 - 11:00am
Engineering 2, Room 398
Lindsey Kuper


Distributed system replication is widely used as a means of fault-tolerance and scalability. However, it provides a spectrum of consistency choices that impose a dilemma for clients between correctness, responsiveness and availability. Given a sequential object and its integrity properties, we automatically synthesize a replicated object that guarantees state integrity and convergence and avoids unnecessary coordination. Our approach is based on a novel sufficient condition for integrity and convergence called well-coordination that requires certain orders between conflicting and dependent operations. We statically analyze the given sequential object to decide its conflicting and dependent methods and use this information to avoid coordination. We present novel coordination protocols that are parametric in terms of the analysis results and provide the well-coordination requirements. We implemented a tool called Hamsaz that can automatically analyze the given object, instantiate the protocols and synthesize replicated objects. We have applied Hamsaz to a suite of use-cases and synthesized replicated objects that are significantly more responsive than the strongly consistent baseline.

Mohsen Lesani is an assistant professor at the Computer Science and Engineering Department of the University of California, Riverside. He is broadly interested in formal methods and concurrent and distributed computing. He spent his postdoc at MIT and obtained his PhD from UCLA. He has research experience with Oracle (Sun) Labs and HP Labs. He has received the best paper award from OOPSLA '18.