- Author:
- Jacob I. Aizikowitz
The thesis addresses the design of multiple-server implementations for services in distributed systems-a generalization of the replication management problem. A frequently used correctness criteria for replication management is that clients of a service not be able to distinguish a single-server implementation from on that involves multiple servers. Our approach formalizes this idea. It is based on viewing a single-server implementation of a service as a specification of that service. A multiple-server implementation is considered correct if it implements this single-server based specification. We show how program proof outlines can be viewed as specifications and, using refinement mappings, define what it means for one proof outline to implement another. The notion of a structural refinement, which formalizes the relationship between a program and the result of performing step-wise refinement, is defined. When one proof outline is a structural refinement of the other, simplified proof obligations can be used to show that the one implements the other. Finally, a methodology for designing a multiple-server implementation of a service is presented. The methodology is based on structural refinement and on viewing proof outlines as specifications. A designer defines a refinement mapping to express the relationship between the state space of a given single-server implementation of a service and the state space of the desired multiple-server implementation. Using this refinement mapping, a provably correct multiple-server implementation is derived from the single server one. Different refinement mappings as well as different single-server based specifications result in different implementations. Examples illustrate the concepts and the methodology.
Cited By
Ramakrishnan R, Sridharan B, Douceur J, Kasturi P, Krishnamachari-Sampath B, Krishnamoorthy K, Li P, Manu M, Michaylov S, Ramos R, Sharman N, Xu Z, Barakat Y, Douglas C, Draves R, Naidu S, Shastry S, Sikaria A, Sun S and Venkatesan R Azure Data Lake Store Proceedings of the 2017 ACM International Conference on Management of Data, (51-63)- Wu H and Kemme B Showing correctness of a replication algorithm in a component based system Proceedings of the 2008 international symposium on Database engineering & applications, (91-99)
- Frølund S and Guerraoui R X-ability Proceedings of the nineteenth annual ACM symposium on Principles of distributed computing, (229-237)
Recommendations
Designing Distributed Services with SDL
An approach to developing distributed services by automatically generating Java implementations from designs expressed using the specification and description language, SDL, is described below.Using a specification exemplar for a distributed meeting ...
Analysis of generalized QBD queues with matrix-geometrically distributed batch arrivals and services
In a quasi-birth---death (QBD) queue, the level forward and level backward transitions of a QBD-type Markov chain are interpreted as customer arrivals and services. In the generalized QBD queue considered in this paper, arrivals and services can occur ...