Lecture preparation

Before lecture, read the paper assigned below, and submit two items to the submission website:

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?

What to learn from this paper?

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?