1. Course Syllabus¶
1.1. Lectures (Weeks 1-7)¶
The list of topics below is a subject of possible minor changes.
Foundations of Distributed Computing
- Week 1: Introduction and Basic Results
- Module Logistics
- Asynchronous Communication Model
- Failure Modes
- Time, Ordering of events, Vector Clocks
- Lamport’s distributed locking
- Week 2: SMR and Consensus
- State Machine Replication
- Two-Phase Commit
- Distributed consensus and its properties
- Paxos and its variants
- Week 3: Byzantine Fault Tolerance
- FLP Impossibility
- Viewstamped Replication and Raft
- CAP Theorem, PACELC
- Byzantine generals problem
- Practical Byzantine Fault-Tolerance
Verification Techniques and Tools
- Week 4: Linearizability, Refinement, and Simulations
- Linearizablity
- Refinement and Proof by Simulation
- Week 5: Hoare-style Reasoning and Auxiliary State
- Owicki-Gries Proofs and Auxiliary Variables
- Rely-Guarantee Reasoning
- Verifying Linearisability with Auxiliary Variables and RG
- Proving Paxos linearisable
- Week 6: TLA+ and Model Checking
- TLA+ and PlusCal
- Tool demo: Examples of specifying systems in TLA+
Mid-Term Break
- Week 7: More TLA+; Ivy
- Tool demo: using TLA+ for Smart Contracts
- Effectively Propositional logic
- Interactive Invariant Inference
- Tool demo: Ivy and its applications
1.2. Classical papers to review¶
For your review project, you only need to choose one paper from the following list.
- The Part-Time Parliament
- Viewstamped Replication: A New Primary Copy Method to Support Highly-Available Distributed Systems
- Fast Paxos
- Paxos Made Moderately Complex
- Distributed Snapshots: Determining Global States of Distributed Systems
- Forward and Backward Simulations Part I: Untimed Systems
- An Axiomatic Proof Technique for Parallel Programs I
- Proving Liveness Properties of Concurrent Programs
1.3. Papers to present at the seminars¶
Below is the tentative list of suggested papers. Each week we will have two presentations by the module attendees. Papers in the following list are grouped according to the common themes. Even not all of them will appear at seminars, you might want to check them out for relevant information on your chosen presentation subjects.
If there is a paper you’d like to discuss that is not in the following list, please, feel free to suggest it!
Deductive Verification
- IronFleet: Proving Practical Distributed Systems Correct
- Verdi: A Framework for Implementing and Formally Verifying Distributed Systems
- Planning for Change in a Formal Verification of the Raft Consensus Protocol
- Chapar: Certified Causally Consistent Distributed Key-Value Stores
- TLC: Temporal Logic of Distributed Components
- Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
- Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
(Semi-)Automated Verification
- Ivy: Safety Verification by Interactive Generalization
- Paxos Made EPR: Decidable Reasoning about Distributed Protocols
- Reducing Liveness to Safety in First-Order Logic
- Modularity for Decidability of Deductive Verification with Applications to Distributed Systems
- I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols
- PSync: a partially synchronous language for fault-tolerant distributed algorithms
Mechanised Reasoning about BFT
- Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq
- Asphalion: trustworthy shielding against Byzantine faults
- SMT and POR beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms
- A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms
- Survey on Parameterized Verification with Threshold Automata and the Byzantine Model Checker
Verified Blockchain (and similar) Protocols
- The Bitcoin Backbone Protocol: Analysis and Applications
- Mechanising Blockchain Consensus
- Formalizing Nakamoto-Style Proof of Stake
- Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity
- Fast and secure global payments with Stellar
- On the Formal Verification of the Stellar Consensus Protocol
- Algorand: Scaling Byzantine Agreements for Cryptocurrencies
- Towards a Verified Model of the Algorand Consensus Protocol in Coq
Testing an Model Checking
- Compositional programming and testing of dynamic distributed systems
- Why is random testing effective for partition tolerance bugs?
- An Empirical Study on the Correctness of Formally Verified Distributed Systems
- SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems
- Inferring and Asserting Distributed System Invariants
Conflict-free Replicated Data Types
- Mergeable Replicated Data Types
- Verifying replicated data types with typeclass refinements in Liquid Haskell
Related Techniques