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:

• Lab 3A: For this part, you'll implement the API (init, get, append, reset, and recover), and define the abstraction relation (abstr). Note that this time you'll need to figure out how to do the implementation and how the abstraction relation should work entirely on your own. We suggest that you write some examples to check if your abstraction relation makes sense.
• Lab 3B: Prove the correctness of your implementation. It's very likely that you will need to go back and change your implementation and/or abstraction relation in the process of proving correctness.

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

Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.