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); define the abstraction relation (abstr); and prove the abstraction examples (abst_*_ok).

  Recall that the lab infrastructure provides you with loop combinators, foreach and for_range, which you can find in src/Spec/Loop.v. You should use them whenever you are iterating over items (either lists or block numbers) in your implementation, so that you can use their associated specs in your proofs.

  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 additional examples to check if your abstraction relation makes sense.

• Lab 3B: Prove the correctness of your init and get implementations. 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. Proving get ensures that your invariant is strong enough to capture all of the information needed to reason about the contents of the log that get returns.

• Lab 3C: Prove the correctness of the rest of your implementation.

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.