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:
We also highly recommend starting on put_ok, which is a long proof.
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 firstname.lastname@example.org.