In this thesis, we show how a view-synchronous group communication service recently specified by Fekete, Lynch, and Shvartsman can be used to support a sequentially consistent replicated data service that load balances queries and tolerates partitioning and merging of the underlying network.
Our work is done in the framework of the I/O automaton model of Lynch and Tuttle.
First, we present an I/O automaton specification that defines the allowed behavior of a sequentially consistent replicated service. Then, we successfully refine this specification to arrive at an I/O automaton that models a distributed implementation of this service. In this implementation, update requests are processed in the same order at all servers of the system, thus guaranteeing mutual consistency of all replicas; query requests are processed at single servers determined by a load-balancing strategy which equalizes the number of queries assigned to each member of the same group. Third, we give a rigorous hierarchical proof that the implementation automaton implements the specification automaton in the sense of trace inclusion. This proof establishes partial correctness of the implementation. Finally, we prove a liveness-related claim that servers are always able to process the queries assigned to them; that is, the servers are never blocked by missing update information.
|
|