Verifying a high-performance crash-safe file system using a tree specification

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...

Full description

Bibliographic Details
Main Authors: Chen, Haogang (Author), Chajed, Tej (Author), Konradi, Alex (Author), Wang, Stephanie (Author), İleri, Atalay (Author), Chlipala, Adam (Author), Kaashoek, M. Frans (Author), Zeldovich, Nickolai (Author)
Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory (Contributor)
Format: Article
Language:English
Published: Association for Computing Machinery (ACM), 2021-11-04T19:09:59Z.
Subjects:
Article
Online Access:Get fulltext

Internet

Get fulltext

Similar Items