Specification and Verification of Distributed Protocols
by Manos Kapritsos and Jon Howell
Note that this is an outdated version of the class. Please go here for the most recent version.
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
