Verifying a high-performance crash-safe file system using a tree specification
© 2017 Copyright is held by the owner/author(s). DFSCQ is the first file system that (1) provides a precise specification for fsync and fdatasync, which allow applications to achieve high performance and crash safety, and (2) provides a machine-checked proof that its implementation meets this specif...
Main Authors: | Chen, Haogang, Chajed, Tej, Konradi, Alex, Wang, Stephanie, İleri, Atalay, Chlipala, Adam, Kaashoek, M. Frans, Zeldovich, Nickolai |
---|---|
Other Authors: | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
Format: | Article |
Language: | English |
Published: |
Association for Computing Machinery (ACM)
2021
|
Online Access: | https://hdl.handle.net/1721.1/137398 |
Similar Items
-
Verifying concurrent, crash-safe systems with Perennial
by: Chajed, Tej, et al.
Published: (2021) -
Using Crash Hoare logic for certifying the FSCQ file system
by: Chen, Haogang, et al.
Published: (2021) -
Certifying a file system using crash hoare logic
by: Chajed, Tej, et al.
Published: (2019) -
Verifying a concurrent, crash-safe file system with sequential reasoning
by: Chajed, Tej
Published: (2022) -
Argosy: verifying layered storage systems with recovery refinement
by: Chajed, Tej, et al.
Published: (2021)