Formalizing the Chain Replication Protocol
This book collects materials used in the formalization of an important distributed algorithm, by Schneider and van Renesse, called Chain Replication. The chain replication algorithm provides a fault-tolerant distributed storage system and guarantees a strong consistency property. The material here includes: the original Schneider and van Renesse paper; a summary of the formalization method, by Bickford & Guaspari; a detailed outline of the formalization by Bickford; and a Nuprl library providing a formal account based on the Logic of Events described by Bickford and Constable.
- Formalizing Chain Replication [pdf], Bickford and Guaspari, explains the formalization and its relation to the original informal algorithm of van Renesse and Schneider.
- Chain Replication for Supporting High Throughput and Availability [pdf] [html], van Renesse and Schneider, is the original work being formalized and reformulated here.
- Verifying Chain Replication using Events [pdf], Bickford, is an exposition of the formalization. It is a pdf file with links to html renditions of formal material.
- Event Systems is library of formal material containing the work described. The previous document ("Verifying...") with its links can be considered an expository entry point to the material.
- Logic of Events, Bickford and Constable, is a technical report describing a logic for distributed computing that has the explanatory and technical power of constructive logics of computation.