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
- 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.
Read the paper
Using Crash Hoare Logic for Certifying the FSCQ File System
by Chen et al.
Why are we reading this paper?
More separation logic.
New specification (to incorporate crash safety).
Well-written paper, doubly so when considering a systems audience.
What to learn from this paper?
See what it means to extend a program logic, to incorporate crash safety.
Notice how verification, like software development, requires layers of abstraction (though often more layers than for normal development).
Understand the limitations of this system.
Answer this question
The model of the disk in FSCQ is more complicated than the one used in the
lab. FSCQ models a disk that is asynchronous: disk_write() returns as soon as
the disk controller has accepted the block but the disk controler may have not
written it to the disk yet. What aspect of the disk_write
specification captures this asynchronous behavior?
If the file system writes two blocks (e.g., B1 and then B2) to the disk using
disk_write(), and then a crash happens, what blocks does the disk store? For
example, if B2 is on the disk, is B1 on the disk too?