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.