High-level executable specifications in DistAlgo, directly excutable in Python (If you have Python 3.5 or 3.6 installed, you can simply do "pip install pyDistAlgo" and run "python -m da filename.da" on any example file.) A complete specification of Basic Paxos in DistAlgo, based on Lamport's paper "Paxos Made Simple". A complete specification of vRA Multi-Paxos (Multi-Paxos with preemption and reconfiguration) extended with state reduction and failure detection in DistAlgo, based on van Renesse and Altinbuken's paper "Paxos Made Moderately Complex" but with improvements. Specifications in TLA+ and mechanically-checked proofs in TLAPS A specification and proof of vRA Multi-Paxos extended with state reduction and failure detection |
