|
Abstract.
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.
|
|