Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 09:44 - 10:06 at Sala II - Synthesis Chair(s): Robbert Krebbers

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 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

09:00 - 10:06: SynthesisResearch Papers at Sala II
Chair(s): Robbert KrebbersDelft University of Technology
09:00 - 09:22
Structuring the Synthesis of Heap-Manipulating ProgramsDistinguished Paper
Research Papers
Nadia PolikarpovaUniversity of California, San Diego, Ilya SergeyYale-NUS College and National University of Singapore
Link to publication DOI Pre-print Media Attached File Attached
09:22 - 09:44
FrAngel: Component-Based Synthesis with Control Structures
Research Papers
Kensen ShiStanford University, Jacob SteinhardtStanford University, Percy LiangStanford University
Link to publication DOI Pre-print Media Attached File Attached
09:44 - 10:06
Hamsaz: Replication Coordination Analysis and Synthesis
Research Papers
Farzin HoushmandUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside
Link to publication DOI Media Attached