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 that can automatically analyze the given object, instantiate the protocols and synthesize replicated objects. We have applied the tool to a suite of use-cases and synthesized replicated objects that are significantly more responsive than the strongly consistent baseline.
Thu 17 JanDisplayed time zone: Belfast change
09:00 - 10:06 | |||
09:00 22mTalk | Structuring the Synthesis of Heap-Manipulating ProgramsDistinguished Paper Research Papers Nadia Polikarpova University of California, San Diego, Ilya Sergey Yale-NUS College and National University of Singapore Link to publication DOI Pre-print Media Attached File Attached | ||
09:22 22mTalk | FrAngel: Component-Based Synthesis with Control Structures Research Papers Kensen Shi Stanford University, Jacob Steinhardt Stanford University, Percy Liang Stanford University Link to publication DOI Pre-print Media Attached File Attached | ||
09:44 22mTalk | Hamsaz: Replication Coordination Analysis and Synthesis Research Papers Farzin Houshmand University of California, Riverside, Mohsen Lesani University of California, Riverside Link to publication DOI Media Attached |