DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2023.35

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)

Abstract

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

@InProceedings{vangeffen_et_al:LIPIcs.ECOOP.2023.35,
  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}
}

Document

DOI: 10.4230/LIPIcs.SNAPL.2015.262

Hardware-Software Co-Design: Not Just a Cliché

Authors: Adrian Sampson, James Bornholt, and Luis Ceze

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)

Abstract

The age of the air-tight hardware abstraction is over. As the computing ecosystem moves beyond the predictable yearly advances of Moore's Law, appeals to familiarity and backwards compatibility will become less convincing: fundamental shifts in abstraction and design will look more enticing. It is time to embrace hardware-software co-design in earnest, to cooperate between programming languages and architecture to upend legacy constraints on computing. We describe our work on approximate computing, a new avenue spanning the system stack from applications and languages to microarchitectures. We reflect on the challenges and successes of approximation research and, with these lessons in mind, distill opportunities for future hardware-software co-design efforts.

Cite as

Adrian Sampson, James Bornholt, and Luis Ceze. Hardware-Software Co-Design: Not Just a Cliché. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 262-273, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{sampson_et_al:LIPIcs.SNAPL.2015.262,
  author =	{Sampson, Adrian and Bornholt, James and Ceze, Luis},
  title =	{{Hardware-Software Co-Design: Not Just a Clich\'{e}}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{262--273},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.262},
  URN =		{urn:nbn:de:0030-drops-50301},
  doi =		{10.4230/LIPIcs.SNAPL.2015.262},
  annote =	{Keywords: approximation, co-design, architecture, verification}
}

Search Results

Documents authored by Bornholt, James

Synthesis-Aided Crash Consistency for Storage Systems

Abstract

Cite as

Hardware-Software Co-Design: Not Just a Cliché

Abstract

Cite as

Thanks for your feedback!

Could not send message