The ADvanced Systems Laboratory (ADSL)
Publication abstract
| :: | Home |
| :: | Projects |
| :: | People |
| :: | Pictures |
| :: | Publications |
| :: | Software |
| :: | Sponsors |
| :: | Internal |
Beyond Storage APIs: Provable Semantics for Storage Stacks
Ramnatthan Alagappan,
Vijay Chidambaram,
Thanumalayan Sankaranarayana Pillai,
Aws Albarghouthi,
Andrea C. Arpaci-Dusseau,
Remzi H. Arpaci-Dusseau
Department of Computer Sciences,
University of Wisconsin-Madison
Abstract:
Applications are deployed upon deep, diverse storage stacks that are constructed on-demand. Although many storage stacks share a common API to allow portability, application behavior differs in subtle ways depending upon unspecified properties of the underlying storage
stack. Currently, there is no way to test whether an application will behave correctly on a given storage stack: corruption or data loss could occur at any point in the application lifetime. We argue that we require an expressive language for specifying the complex storage guarantees required by different applications. The same language can be used to write a high-level specification capturing the design of different storage-stack layers. Given the required guarantees, and the storage-stack specifications, we can prove that stacks constructed dynamically (by composing different storage-stack layers) provide the guarantees required by the application.
Available as:
PDF,
BibTex
Isabelle Proofs
Publications