Specifying Crash Safety for Storage Systems

Tuesday, May 19, 2015 - 3:00pm-3:30pm
Authors: 

Haogang Chen, Daniel Ziegler, Adam Chlipala, and M. Frans Kaashoek, MIT CSAIL; Eddie Kohler, Harvard University; Nickolai Zeldovich, MIT CSAIL

Abstract: 

Software that is provably correct has been a long-time goal of computer science. Until recently this goal was realized for only small programs, but over the last decade several large systems have been built that have provable correctness properties. Examples include CompCert, seL4, IronClad, CertiKOS, Bedrock, Termite, Click’s dataplane, and Jitk. One aspect not covered by these systems is reasoning about failures—power failures, hardware faults, or software bugs—which is well-known to be tricky in systems code.

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {189922,
author = {Haogang Chen and Daniel Ziegler and Adam Chlipala and M. Frans Kaashoek and Eddie Kohler and Nickolai Zeldovich},
title = {Specifying Crash Safety for Storage Systems},
booktitle = {15th Workshop on Hot Topics in Operating Systems (HotOS XV)},
year = {2015},
address = {Kartause Ittingen, Switzerland},
url = {https://www.usenix.org/conference/hotos15/workshop-program/presentation/chen_haogang},
publisher = {USENIX Association},
month = may
}
Download
Chen Haogang PDF