Lab 3: Logging

This lab will introduce you to reasoning about correctness in the presence of crashes, by implementing and proving correctness of a crash-safe log.

To get started, commit your work in the class repo locally and run git pull to merge in the new lab. Run make to compile the starter code for the lab.

We have specified what we expect from a crash-safe in src/Lab3/LogAPI.v. We recommend that you start by reading those definitions. Your implementation will run on top of a regular disk, as defined in src/Common/OneDiskAPI.v, the same disk interface that you implemented in lab 2 on top of the bad-block disk.

The implementation of a log typically works by storing a block header at some fixed address (e.g., zero) and the actual logged data blocks (e.g., at addresses following the header). The number of valid blocks in the log is typically stored in the header itself.

Your implementation will all be in src/Lab3/LogImpl.v. This time, we've provided almost no starter code. Your job is to implement all of the procedures required by the log API, define the abstraction relation, and prove your implementation correct.

Submission for this lab is split into three parts:

When you are done with the lab assignment, run make lab3a-handin.tar.gz to generate a lab3a-handin.tar.gz file (or lab3b and lab3c for parts B and C, respectively). You'll then need to upload it to the submission web site.