Correctness of Paxos with Replica-Set-Specific Views

We present a specification and proof of correctness for the Paxos replicated state machine consensus protocol in which replica-set-change is implemented with replica-set-specific views.

tr-2004-45.ps
PostScript file
tr-2004-45.pdf
PDF file
tr-2004-45-big-map.pdf
PDF file

Details

TypeTechReport
NumberMSR-TR-2004-45
Pages125
InstitutionMicrosoft Research
> Publications > Correctness of Paxos with Replica-Set-Specific Views