Overview
Atlassian Sourcetree is a free Git and Mercurial client for Windows.
Atlassian Sourcetree is a free Git and Mercurial client for Mac.
deepspeclabs
Exercises for DSSS refinement/crashes
Preface
Please do not post public copies of this repository (e.g., by making a public copy of it in your Github account) or post your solutions. We plan to use this material for a class at MIT this coming fall semester.
Exercise 1: implement and prove StatDB's implementation of Mean.
The current StatDB code does not properly implement the mean
function.
If you run statdbcli, you will see that it always returns 0:
% make bin/statdbcli ... % ./bin/statdbcli Mean: Just 0 Enter a number to add: 5 Mean: Just 0 Enter a number to add: 1 Mean: Just 0 Enter a number to add: 0 Mean: Just 0 ...
Your job is to implement the mean
function in src/StatDb/StatDbImpl.v
,
and to prove that it is correct, by fixing up the proof at the bottom of
that same file.
Exercise 2: bad sector remapping.
src/RemappedDisk
contains a partial implementation of badsector
remapping. The idea is to take a disk that has a bad sector, and make
it look like a fully working disk by remapping the bad sector to another
sector (the last sector). For simplicity, we assume there is exactly
one bad sector.
We provide an implementation of read
in src/RemappedDisk/RemappedDiskImpl.v
.
Your job is to fill in several other parts of that file:

Implement
write
. 
Fill in the abstraction relation
remapped_abstraction
. 
Finish the proof at the bottom of the file, which includes (1) fixing up the proof of the existing
read
implementation based on your abstraction, (2) proving yourwrite
implementation with your abstraction, and (3) proving that the existinginit
implementation establishes your abstraction in the initial state.
Exercise 3: replicated disk without recovery
src/ReplicatedDisk
contains a partial implementation of a replicated disk.
remapping. The idea is to use two physical disks so that if one fails, the
application can continue with the remaining one. If a fails and is replaced
with a new one, the implementation should fix up the new disk to reflect all the
writes the nonfailed disk has seen. We assume that both disks won't fail at
the same time.
We provide an implementation of read
in src/ReplicatedDisk/ReplicatedDiskImpl.v
.
Your job is to fill in several other parts of that file:

Implement
write
. 
Complete the spec for
write_ok
and prove it. Using thestep
ltac this proof is straightforward. 
To get some confidence that your
write_ok
spec is correct, also provewrite_read_check_ok
, which verifies that a read after a write observes the effect of the write. Using thestep
ltac this proof is straightforward. 
Complete the spec for
init_ok
and prove it. This is a bit challenging sinceInit
callsinit_at
to initialize each block recursively. So, you will also have to write the spec for and proveinit_at_ok
. Your proof ofinit_at_ok
will use induction.
Exercise 4: replicated disk with recovery
Your job is to finish the proof of correctness
for recovery. Specifically, finish these proofs in
src/ReplicatedDisk/ReplicatedDiskImpl.v
:

Prove
Recover_rok
. 
Prove
Recover_ok
. 
Prove
Write_rok
.
You will need to understand the details of fixup
and the predicates
used in the postconditions of fixup
's correctness theorems. We plan
to cover this in lecture.