Name
Abstract | ||
|---|---|---|
File systems not only have to be functionally correct, they also have to be crash-safe: a power cut while an operation is running must be guaranteed to lead to a consistent state after restart that loses as little information as possible. Specification and verification of crash-safety is particularly difficult for non-redundant write-back caches. This paper defines a novel crash-safety criterion that facilitates specification and verification of order-preserving caches. A power cut is basically observationally equivalent to a retraction of a few of the last executed operations. The approach is modular: It gives simple proof obligations for each individual component and for each refinement in the development. The theory is supported by our interactive theorem prover KIV and proof obligations for crash-safety have been verified for the Flashix flash file system. |
Year | Venue | Field |
|---|---|---|
2017 | IFM | Programming language,Flash file system,Computer science,Modular design,Proof assistant |
DocType | Citations | PageRank |
Conference | 1 | 0.35 |
References | Authors | |
13 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jörg Pfähler | 1 | 82 | 6.28 |
| Gidon Ernst | 2 | 144 | 14.46 |
| Stefan Bodenmüller | 3 | 1 | 0.68 |
| Gerhard Schellhorn | 4 | 769 | 56.43 |
| Wolfgang Reif | 5 | 915 | 95.46 |