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
An Empirical Study on the Correctness of Formally Verified Distributed Systems
by Fonseca et al.
Why are we reading this paper?
- Verified systems make many assumptions. This paper looks at bugs in those assumptions, using verified distributed systems as their case study.
- Fun read with many concrete examples.
What to learn from this paper?
- What could go wrong with a "verified" system.
- What does it mean to have the wrong assumption.
- How to start going about ensuring your assumptions are reasonable?
Answer this question
The lab infrastructure has a shim layer to read and write disk blocks. Could
a bug like V3, which is described in Section 4.2 ("Disk Operations"), affect the
correctness of your lab 4 solution?
