1 Search Results for "Van Geffen, Jacob"

Synthesis-Aided Crash Consistency for Storage Systems

Authors: Jacob Van Geffen, Xi Wang, Emina Torlak, and James Bornholt

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Reliable storage systems must be crash consistent - guaranteed to recover to a consistent state after a crash. Crash consistency is non-trivial as it requires maintaining complex invariants about persistent data structures in the presence of caching, reordering, and system failures. Current programming models offer little support for implementing crash consistency, forcing storage system developers to roll their own consistency mechanisms. Bugs in these mechanisms can lead to severe data loss for applications that rely on persistent storage. This paper presents a new synthesis-aided programming model for building crash-consistent storage systems. In this approach, storage systems can assume an angelic crash-consistency model, where the underlying storage stack promises to resolve crashes in favor of consistency whenever possible. To realize this model, we introduce a new labeled writes interface for developers to identify their writes to disk, and develop a program synthesis tool, DepSynth, that generates dependency rules to enforce crash consistency over these labeled writes. We evaluate our model in a case study on a production storage system at Amazon Web Services. We find that DepSynth can automate crash consistency for this complex storage system, with similar results to existing expert-written code, and can automatically identify and correct consistency and performance issues.

Cite as

Jacob Van Geffen, Xi Wang, Emina Torlak, and James Bornholt. Synthesis-Aided Crash Consistency for Storage Systems. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 35:1-35:26, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

  author =	{Van Geffen, Jacob and Wang, Xi and Torlak, Emina and Bornholt, James},
  title =	{{Synthesis-Aided Crash Consistency for Storage Systems}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{35:1--35:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.35},
  URN =		{urn:nbn:de:0030-drops-182285},
  doi =		{10.4230/LIPIcs.ECOOP.2023.35},
  annote =	{Keywords: program synthesis, crash consistency, file systems}
  • Refine by Author
  • 1 Bornholt, James
  • 1 Torlak, Emina
  • 1 Van Geffen, Jacob
  • 1 Wang, Xi

  • Refine by Classification
  • 1 Computer systems organization → Secondary storage organization
  • 1 Software and its engineering → Search-based software engineering

  • Refine by Keyword
  • 1 crash consistency
  • 1 file systems
  • 1 program synthesis

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2023

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail