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
I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols
by Ma et al. You can also watch the video of the conference presentation of this
paper at SOSP 2019,
here.
Why are we reading this paper?
- Distributed protocols are important to verify, even in isolation from their implementations (as we saw in the Amazon paper).
- This paper articulates the problem of inductive invariants for distributed protocols.
- The paper argues that it might be possible to automate the process of constructing these invariants.
What to learn from this paper?
- Difficulty of stating invariants for a distributed system, at the protocol level.
- Actual invariants vs. inductive invariants.
- Invariant inference techniques.
Answer this question
Both I4 and Armada work at the state-machine level, and both are
reasoning about concurrent execution (whole computers in I4 and threads
in Armada). Could you apply I4's invariant inference to Armada?
What might make I4's distributed protocols better suited to invariant
inference than Armada's concurrent software?
