Lab 2: Remapped disk

In this lab assignment, you will implement a remapped disk that takes a disk with a bad sector and exports an API with no bad sector (but a disk that is one sector smaller).

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/Lab2/BadBlockAPI.v, which is the specification for the disk with a bad sector that you will build upon, and also src/Common/OneDiskAPI.v, which is the specification for a regular disk that your implementation will meet.

Your implementation will all be in src/Lab2/RemappedDiskImpl.v. We provide init and read, and leave you to implement write. Your most important task is to come up with a good abstraction relation for this problem. You will likely find that you discover new conditions needed in the abstraction relation as you work on the proofs.

Submission for this lab is split into two parts:

• Lab 2A: Complete the write implementation and abstraction relation. You should also prove the example abstraction relation theorems, which will catch a variety of bugs. We recommend you try to also prove init_ok and start on read_ok (which may inform your abstraction relation), but you don't have to submit working proofs (that is, you can end those proofs with Admitted.).
• Lab 2B: Complete the rest of the lab. Specifically, you should prove init_ok, read_ok, write_ok, and size_ok.

When you are done with the lab assignment, run make prepare-submit to generate a lab2-handin.tar.gz file, and submit it via the submission web site. Please follow the same submission process for both parts of the lab.

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.