Lab 4: Replicated disk
This lab will introduce you to reasoning about a limited form of concurrency
(in the form of one of the disks failing in the background), as well as to
reasoning about crash recovery.
In this lab assignment, you will implement a disk replication system. The API
you'll be using provides access to two disks. It allows a single disk to fail at
any time (this failure is fail-stop, so you don't need to handle restoring a
disk). You'll implement a single-disk API by replicating over the two disks,
which should hide failure of either disk.
There are two main challenges in this lab:
- Concurrency. A disk can fail at any time, which is a concurrent
behavior you need to address.
- Recovery. In this lab you'll need a recovery procedure to fix up the
disk after a crash. Your implementation (particularly for write) will
need this recovery procedure to have the atomic crash behavior expected for the
single-disk API.
The source code provided for this lab is as follows:
- src/Lab4/TwoDiskBaseAPI.v
defines the low-level semantics of two disks where one of them can fail at any time.
- src/Lab4/TwoDiskAPI.v
provides an alternative way of looking at the low-level semantics in terms of
the two_disks_are predicate. This allows re-stating the semantics in
a way that avoids reasoning about the possibility of the disk failing at every
possible step.
src/Lab4/TwoDiskImpl.v
proves that the TwoDiskAPI is a valid specification for TwoDiskBaseAPI.
- src/Lab4/ReplicatedDiskImpl.v
contains a skeleton implementation of a single replicated disk (OneDiskAPI,
which you already saw in labs 2 and 3) on top of the two possibly-failing
disks (TwoDiskAPI). Your job for this lab is to finish this implementation.
The other files in
src/Lab4 implement Haskell extraction, if you want to
run your replicated disk implementation with the help of
make bin/replicate-nbd.
Submission for this lab is split into four parts:
- Lab 4A:
Implement read and prove the intermediate specifications
for read, write, and size. You should also
spend some time reading through all of ReplicatedDiskImpl.v to
see what the upcoming assignments are.
- Lab 4B:
Write a specification for recovery. Admitting the proof (and even before
fully implementing recovery), prove that your specification is idempotent
(its crash condition implies its precondition) and
that read, write, and size are correct using
your recovery specification.
- Lab 4C:
Implement fixup (the core of the recovery loop). Write a
specification and, admitting the proof your implementation meets this
specification, prove the overall recovery procedure against your
specification.
- Lab 4D:
Prove your implementation of fixup meets your specification.
Note the exercises in the assignment! We'll be going back and forth in the
file, unlike in previous labs. Make sure to look for the labeled exercises for
each handin and complete all of them. Specifications from earlier weeks will
be important in later ones, so you should read the entire assignment and keep
it in mind while working.
We expect that in later weeks you'll need to go back
and fix your specifications as you start proving, so keep this in mind when
assessing how much work each handin of the lab is.
Submit your work to the submission web site as in previous labs.
