Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch

This page documents the KIV formalization of

Stefan Bodenmüller, Gerhard Schellhorn, Wolfgang Reif:
Modular Integration of Crashsafe Caching into a Verified Virtual File System Switch.
Presented at iFM 2020.

Project Overview gives an overview of the entire specification hierarchy.

KIV-Projects always link to an overview which gives the dependency graph of specifications. Clicking on one specification gives its text, and links to a theorem base summary (which lists names of theorems) and a theorem base listing (which shows the full sequent for each theorem). From there individual theorems and the full details of each proof are accessible.

Data Refinement of AFS

The interface of the flash file system core is defined by the ASM specification afs-asm, in which the persistent state of the file system is abstractly defined as two heaps dirs and files. The virtual file system switch is implemented by the ASM specification vfs-asm using afs-asm as a submachine. Caching is integrated via the ASM specification cache-asm. The actual caching data structures are outsourced in submachines icache-asm, pcache-asm, tcache-asm etc. Furthermore cache-asm is both a refinement (proven in cache-refine) and a client of afs-asm.

Proving Crash Safety

The recovery proof obligation guarantees that the integration of cache-asm maintains crash safety for crashes occuring in synced states.

For crashes in non-synced states (in particular during fsync), Write-Prefix Crash Consistency is proven in the specifications cache-sync, cache-crash-refine, and vfs-crash-refine. In cache-sync the forward simulation =r is performed on the level of Cache with the commuting diagram theorems over the following operations:

• writebegin: refine-writebegin
• writepage: refine-writepage and refine-writepage-skip
• writesize: refine-writesize-skip
• truncate: refine-truncate and refine-truncate-skip

In cache-crash-refine this forward simulation is lifted to AFS. This yields the corresponding theorems:

• writebegin: writebegin-run
• writepage: writepage-run and writepage-run-fail resp. writepage-run-stutter
• writesize: writesize-run-fail resp. writesize-run-stutter
• truncate: truncate-run and truncate-run-fail

These theorems are then used in vfs-crash-refine to prove the final theorems refine-write and refine-truncate over the VFS operations.

Used basic libraries:

• The basic KIV library with basic data types
• The KIV separation library gives an embedding of Separation Logic with separation formulas and reasoning support
• The Flashix common library with data types specifically defined for the Flashix file system

Back to the overview of all KIV projects.
For general informations on KIV and a download site for the whole system refer to this page.

[Imprint] [Data Privacy Statement] [E-Mail]