Refinement and Separation: Modular Verification of Wandering Trees

Flash memory does not allow in-place updates like conventional hard disks. Therefore all file systems must maintain an index that maps identifiers for files and directories to the address of their most recently written version. For efficiency, the index is typically implemented as a Wandering Search Tree. However, the verification of Wandering Trees is challenging since it has to deal with multiple aspects at once: the algorithmic complexity of search trees, trees in RAM that are partially loaded from snapshots on flash, where only modified parts are incrementally saved, and the efficient representation of trees as pointer structures. This paper proposes a modular solution that allows verifying each aspect separately. The solution has been mechanized in the theorem prover KIV.