
The ADvanced Systems Laboratory (ADSL)



Provable Storage Stack Semantics
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 keyvalue store working directly on
top of a disk drive. The below proof snippet shows the atomicity theorem for this
simple keyvalue 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. 
