Lab 3: Atomic pair

In this lab assignment, you will implement an API that reads and writes a pair of blocks. The catch is that your write implementation must be atomic with respect to crashes.

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 recommend you first briefly read src/Lab3/AtomicPairAPI.v, which is the precise specification for the atomic pair API that you will implement. You will have access to a normal disk, the same disk whose API you implemented in Lab 2.

Your implementation will all be in src/Lab3/AtomicPairImpl.v. This time, we've provided only stubs. You will implement the entire API, 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 (get, put, and init) and write an abstraction relation. 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'd like you to write some examples to check if your abstraction relation makes sense.
• Lab 3B: We plan to provide some more help with the abstraction relation after Lab 3A is due (including examples). Only the init_ok and get_ok proofs are assigned, but you'll probably spend some time fixing your abstraction relation.

  We also highly recommend starting on put_ok, which is a long proof.

• Lab 3C: The rest of the lab is due, which is just put_ok. All the interesting crash reasoning is in this function.

When you are done with the lab assignment, run make prepare-submit to generate a lab3-handin.tar.gz file. You'll need to rename it to lab3[abc]-handin.tar.gz for each sub-part before submitting it via 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.