Certifying a file system using crash hoare logic
FSCQ is the frst fle system with a machine-checkable proof that its implementation meets a specifcation, even in the presence of fail-stop crashes. FSCQ provably avoids bugs that have plagued previous fle systems, such as performing disk writes without suffcient barriers or forgetting to zero out di...
| Main Authors: | , , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM)
2019
|
| Online Access: | https://hdl.handle.net/1721.1/122622 |
| _version_ | 1811086883760898048 |
|---|---|
| author | Chajed, Tej Chen, Haogang Chlipala, Adam Kaashoek, M. Frans Zeldovich, Nickolai Ziegler, Daniel Todd |
| author2 | Massachusetts Institute of Technology. Laboratory for Computer Science |
| author_facet | Massachusetts Institute of Technology. Laboratory for Computer Science Chajed, Tej Chen, Haogang Chlipala, Adam Kaashoek, M. Frans Zeldovich, Nickolai Ziegler, Daniel Todd |
| author_sort | Chajed, Tej |
| collection | MIT |
| description | FSCQ is the frst fle system with a machine-checkable proof that its implementation meets a specifcation, even in the presence of fail-stop crashes. FSCQ provably avoids bugs that have plagued previous fle systems, such as performing disk writes without suffcient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover its state correctly without losing data. To state FSCQ's theorems, this paper introduces the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels. CHL also reduces the proof effort for developers through proof automation. Using CHL, we developed, specifed, and proved the correctness of the FSCQ fle system. Although FSCQ's design is relatively simple, experiments with FSCQ as a user-level fle system show that it is suffcient to run Unix applications with usable performance. FSCQ's specifcations and proofs required signifcantly more work than the implementation, but the work was manageable even for a small team of a few researchers. |
| first_indexed | 2024-09-23T13:36:03Z |
| format | Article |
| id | mit-1721.1/122622 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T13:36:03Z |
| publishDate | 2019 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/1226222022-10-01T15:58:39Z Certifying a file system using crash hoare logic correctness in the presence of crashes Chajed, Tej Chen, Haogang Chlipala, Adam Kaashoek, M. Frans Zeldovich, Nickolai Ziegler, Daniel Todd Massachusetts Institute of Technology. Laboratory for Computer Science Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science FSCQ is the frst fle system with a machine-checkable proof that its implementation meets a specifcation, even in the presence of fail-stop crashes. FSCQ provably avoids bugs that have plagued previous fle systems, such as performing disk writes without suffcient barriers or forgetting to zero out directory blocks. If a crash happens at an inopportune time, these bugs can lead to data loss. FSCQ's theorems prove that, under any sequence of crashes followed by reboots, FSCQ will recover its state correctly without losing data. To state FSCQ's theorems, this paper introduces the Crash Hoare logic (CHL), which extends traditional Hoare logic with a crash condition, a recovery procedure, and logical address spaces for specifying disk states at different abstraction levels. CHL also reduces the proof effort for developers through proof automation. Using CHL, we developed, specifed, and proved the correctness of the FSCQ fle system. Although FSCQ's design is relatively simple, experiments with FSCQ as a user-level fle system show that it is suffcient to run Unix applications with usable performance. FSCQ's specifcations and proofs required signifcantly more work than the implementation, but the work was manageable even for a small team of a few researchers. National Science Foundation (U.S.) (Award CNS-1053143) National Science Foundation (U.S.) (Award CCF-1253229) 2019-10-18T13:28:41Z 2019-10-18T13:28:41Z 2017-04 2019-10-04T16:17:23Z Article http://purl.org/eprint/type/JournalArticle 0001-0782 https://hdl.handle.net/1721.1/122622 Chajed, Tej et al. "Certifying a file system using crash hoare logic: correctness in the presence of crashes." Communications of the ACM 60, 4 (April 2017): 75-84 © 2017 The Authors en http://dx.doi.org/10.1145/3051092 Communications of the ACM Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Association for Computing Machinery (ACM) Prof. Chlipala via Phoebe Ayers |
| spellingShingle | Chajed, Tej Chen, Haogang Chlipala, Adam Kaashoek, M. Frans Zeldovich, Nickolai Ziegler, Daniel Todd Certifying a file system using crash hoare logic |
| title | Certifying a file system using crash hoare logic |
| title_full | Certifying a file system using crash hoare logic |
| title_fullStr | Certifying a file system using crash hoare logic |
| title_full_unstemmed | Certifying a file system using crash hoare logic |
| title_short | Certifying a file system using crash hoare logic |
| title_sort | certifying a file system using crash hoare logic |
| url | https://hdl.handle.net/1721.1/122622 |
| work_keys_str_mv | AT chajedtej certifyingafilesystemusingcrashhoarelogic AT chenhaogang certifyingafilesystemusingcrashhoarelogic AT chlipalaadam certifyingafilesystemusingcrashhoarelogic AT kaashoekmfrans certifyingafilesystemusingcrashhoarelogic AT zeldovichnickolai certifyingafilesystemusingcrashhoarelogic AT zieglerdanieltodd certifyingafilesystemusingcrashhoarelogic AT chajedtej correctnessinthepresenceofcrashes AT chenhaogang correctnessinthepresenceofcrashes AT chlipalaadam correctnessinthepresenceofcrashes AT kaashoekmfrans correctnessinthepresenceofcrashes AT zeldovichnickolai correctnessinthepresenceofcrashes AT zieglerdanieltodd correctnessinthepresenceofcrashes |