Lecture preparation

Assignment

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.
• Abstraction layers.

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?