MojaveComm: A Robust Group Communication Library for Grid EnvironmentsCristian T¸˘apus¸, David Noblet, and Jason HickeyComputer Science DepartmentCalifornia Institute of Technology{crt,dnoblet,jyh}@cs.caltech.eduAbstractThis paper introduces a fault-tolerant group communi-cation protocol that is aimed at grid and wide area environ-ments. The protocol has two layers. The lower layer pro-vides a total order of messages in one group, while the up-per layer provides an ordering of messages accross groups.The protocol can be used to implement sequential consis-tency. To prove the correctness of our protocol we have useda combination of model checking and mathematical proofs.The paper also presents the behavior of our implementationof the protocol in a simulated environment.1 IntroductionDistributed systems, historically, have proved to be bothdifficult to implement and difficult to reason about. In par-ticular, it is not easy to develop systems that simultaneouslyhave good usability, scalablility, reliability/fault-tolerance,and performance characteristics. Since these properties of-ten tend to work in opposing directions, many current sys-tems choose to sacrifice one in favor of another.One compromise that designers of distributed systemsconsistently make in order to improve performance is theadoption of relaxed consistency models. Unfortunately, theuse of such relaxed semantics often requires the user to havea deep understanding of the underlying system in order towrite correct applications. In the context of a distributedshared memory (DSM) system, for example, these relaxedsemantics can be awkward to use as they tend to deviatesignificantly from the more natural and familiar semanticsprovided by sequential systems.The alternative is to adopt a strict consistency model,such as sequential consistency [8], which preserves the or-der of accesses specified by the programs. It is widely ac-cepted that this is the simplest programming model for dataconsistency. In practice, the sequential consistency modelhas been reluctantly adopted due to concerns about its per-formance. However, recent work in compilers for parallellanguages [7] has shown that sequential consistency is a fea-sible alternative to relaxed models. This paper introducesa group communication infrastructure that enables the im-plementation of the sequential consistency model in a dis-tributed environment.The issue of reliabilty is another critical component inthe development of distributed systems. While the mainconcern in designing such systems is coping with externalfailures, like network or hardware failures, it is often thecase that programming bugs and unpredicted corner casesgenerate most of the problems. In order to combat thisissue, we make use of formal verification mechanisms toguarantee the correctness of our protocol. The use of for-mal methods is invaluable when building reliable systems,as it helps to model the complex interaction between thedifferent entities in a distributed system and can help guidethe design process to yield more robust solutions.The focus of this paper is on the implementation of adistributed group communication protocol [13] for GRIDenvironments. This protocol has two layers: the first layerguarantees the ordering of messages sent within a group;the second layer, sitting on top of it, guarantees the causalordering of messages sent in overlapping groups. This pro-tocol can be easily used to provide sequential consistencywith respect to access of shared data.The major contributions of this paper are: the design andthe implementation of a totally distributed (no central pointof failure) group communication protocol with guaranteesfor a total order of messages, the use of formal methods toshow the correctness of the implementation, and the use ofthe described protocol to implement a GRID service for asequentially consistent distributed shared objects system.The paper is organized as follows. First, we introducethe protocol we designed. Next, we present the two modelcheckers we use and their contribution with respect to thecorrectness of our protocol. Finally, we present preliminaryexperimental results using our prototype implementation inand conclude the paper by discusing differences betweenour approach and other group communication libraries.12 Protocol descriptionThis section presents the two layers of our protocol. Wehave shown the correctness of the upper layer of our pro-tocol and proved the guarantees that it makes in a previouswork [13]. In this paper we focus on the correctness of thelower layer and present how its distributed approach makesit robust in the presence of failures.Although our protocol was designed to be abstract andapplicable in many situations, one of the main goals of theproject was to develop a communication infrastructure forGRID services and to use it to build a distributed sharedobjects system.2.1 OverviewThe system is composed of a set of processes. Processeshave a unique identifier that is persistent across failures. Wedefine a group to be a set of processes. A view of a group isdefined as a subset of the group membership.Processes can belong to several groups at the same time.The upper layer of the protocol relies on the existence of atotal order of messages sent within each group that is pro-vided by the lower layer of the protocol. Additionally, it re-quires that messages sent by one process to different groupsbecome part of the total order in each group in the same se-quence in which the messages were issued. For example, ifa process were to send two messages, m1and m2, to groupsg1and g2respectively, then message m1must become partof the order in group g1before m2becomes part of the or-der in group g2. It is important to notice that we do notrequire that m1is delivered before we can send m2; rather,we simply require that m1obtains a sequence number be-fore m2does. While there is a penalty for implementingthis restriction we do minimize it by separating the taggingof messages with sequence numbers from the actual mes-sage delivery.Each group can have several views and the views canoverlap. Views are local to processes and represent theirimage of the membership of the group. In each group weimplement the Virtual Synchrony [3] model. When a re-quest to join a group is received by a process or when aprocess leaves or is detected to have failed a view change istriggered in the group. The view change is a synchroniza-tion point for the processes that