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

Research output: Contribution to conferencePaperpeer-review


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.

Original languageEnglish (US)
StatePublished - 2015
Externally publishedYes
Event15th Workshop on Hot Topics in Operating Systems, HotOS 2015 - Warth-Weiningen, Switzerland
Duration: May 18 2015May 20 2015


Conference15th Workshop on Hot Topics in Operating Systems, HotOS 2015

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Hardware and Architecture
  • Information Systems


Dive into the research topics of 'Beyond storage APIs: Provable semantics for storage stacks'. Together they form a unique fingerprint.

Cite this