Application correctness hinges on subtle behaviors exhibited by storage stack components such as disk drives, file systems and hypervisors. We show how we can formally model subtle storage stack behaviors using an expressive language such as Isar and prove important and interesting properties such as atomicity, consistency and durability. We take an example of a simple key-value store working directly on top of a disk drive. The below proof snippet shows the atomicity theorem for this simple key-value store.

theorem kv_put_atomic_theorem:
shows   "length d > 2 ∧ (Suc idx) < length d  ∧ (list_contains after (kv_put s1 s2 d idx)) ∧ s1~=[] ∧ s2 ~= []
         ⇒
         after!idx=d!idx ∧ after!(Suc idx)=d!(Suc idx)
         ∨
         after!idx=s1 ∧ after!(Suc idx)=s2"
apply(auto)
done

The complete model can be found in this repository.

This repository just contains a single Isabelle theory file that shows the flavor of the proofs that we have discussed in the paper. To step through this theory file, you need Isabelle. Isabelle can be downloaded here. For more details, you can read our paper here.