Lecture preparation
Before lecture, read the paper assigned below, and submit two items
to the
submission website:
- Submit your own question about the paper (e.g., what you find most
confusing about the paper or the paper's general context/problem), before
lecture (i.e., 1pm). You cannot use the question below. To the extent
possible, during lecture we will try to answer questions submitted
beforehand.
- Submit your answer for the question below, before the beginning of the lecture.
Also keep in mind that you will need to write a
paper summary for your choice of papers
throughout the semester.
Assignment
Read the paper
IronFleet: Proving Practical Distributed Systems Correct
by Hawblitzel et al.
Why are we reading this paper?
- Distributed systems is an important domain for formal verification.
- Significant progress in verifying practical-looking examples of distributed systems.
- Using new tools we have not seen before: Dafny and TLA.
What to learn from this paper?
- How IronFleet handles concurrency and failures, which are the typical hard problems in distributed systems.
- How IronFleet separates reasoning about code vs. the network protocol.
- How IronFleet proves liveness properties.
Answer this question
In the IronFleet paper, what is the spec for an overall
system, what is the code that they prove meets the spec, and
what is the sequence of arguments (e.g., different types of refinement)
that the authors use in their proof? Which of these proof arguments
are machine-checked, and which are done on paper?
