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

Internet

https://hdl.handle.net/1721.1/137398

Similar Items