Specification and Verification of Distributed Protocols
by Manos Kapritsos and Jon Howell
This course teaches a foundation of concepts that build up to the
ability to model a distributed, asynchronous protocol and prove it safe.
By the end of the course, participants will
- Be able to specify the desired behavior of real-world protocols using
refinement.
- Be able to articulate the guarantees provided by verification.
- Learn how to model protocols and prove them safe.
- Demonstrate mastery by building a distributed sharded key-value store and
proving that it always returns correct results.
Chapter 01: Dafny Basics
This chapter introduces the mathematical subset of Dafny needed to work the exercises in the rest of the course.Lectures
Exercises
Associated Libraries
Chapter 02: Specification
Specification is how we write down what a protocol does. A verification result is only as good as its specification.Lectures
Exercises
Chapter 03: State Machines
This chapter describes state machine models, a general tool we'll use to describe protocols and the environment they work in.Lectures
Exercises
Chapter 04: Invariants
Invariants are the central tool used to prove safety properties of protocols.Lectures
Exercises
Chapter 05: Distributed State Machines
Here we assemble state machines in an idiomatic way to represent a protocol and the environment the protocol operates in.Lectures
Exercises
Associated Libraries
Project 01: Distributed Lock Server
This midterm project demonstrates mastery of the concepts in chapters 1—5.Lectures
Exercises
- DistributedSystem
This file isn't editable because it's a trusted file that specifies how
hosts interact with one another over the network.
- Exercise 01: Midterm Project
Build a distributed lock server. Define how a host implements your
protocol in host.v.dfy; write your safety spec and proof here.
- Host protocol
Define the host state machine here: message type, state machine for executing one
host's part of the protocol.
- Network
This file isn't editable because it's a trusted file that specifies how
the network delivers packets, allowing reorder and duplicate delivery.
Associated Libraries
Chapter 06: Refinement
Refinement helps us write a specification that abstracts away the implementation details of the protocol.Lectures
Exercises
Associated Libraries
Chapter 07: Asynchronous Clients
Most specifications want to capture the idea of linearizability: that clients care about when their interactions happen in real time. This chapter develops a general technique for encoding this constraint into a specification.Lectures
Exercises
Associated Libraries
Chapter 08: Application Correspondence
A refinement proof is meaningless if the verification engineer can hide real behavior behind a meaningless refinement abstraction function. This chapter develops a general technique for establishing a specification that prevents such flaws.Lectures
Exercises
- Exercise 01: Sharded Producer Consumer
How do we prevent a nonsense refinement theorem? For example, suppose the
protocol-level state machine allows arbitrary behavior, but the refinement
abstraction function maps every protocol-level state to the initial spec state,
so it can refine to a bunch of stutter steps?
Associated Libraries
Project 02: Sharded Key-Value Store
This final project demonstrates mastery of the concepts in chapters 1—6.Lectures
Exercises
Associated Libraries
Auxiliary Material:
Lectures
