|
Abstract.
Replication is a common technique to build reliable and scalable
systems. Traditional strong consistency maintains the same total order
of operations across replicas. This total order is the source of
multiple desirable consistency properties: integrity, convergence and
recency. However, maintaining the total order has proven to inhibit
availability and performance. Weaker notions exhibit responsiveness and
scalability; however, they forfeit the total order and hence its
favorable properties. This project revives these properties with as
little coordination as possible. It presents a tool called Hampa that
given a sequential object with the declaration of its integrity and
recency requirements, automatically synthesizes a
correct-by-construction replicated object that simultaneously
guarantees the three properties. It features a relational object
specification language and a syntax-directed analysis that infers
optimum staleness bounds. Further, it defines coordination-avoidance
conditions and the operational semantics of replicated systems that
provably guarantees the three properties. It characterizes the
computational power and presents a protocol for recency-aware objects.
Hampa uses automatic solvers statically and embeds them in the runtime
to dynamically decide the validity of coordination-avoidance
conditions. The experiments show that recency-aware objects reduce
coordination and response time.
|
|