Certifying a File System Using Crash Hoare Logic: Correctness in the Presence of Crashes.
FSCQ is the first file system with a machine-checkable proof that its implementation meets a specification, even in the presence of fail-stop crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient barriers or forgetting to zero o...
| Publicado en: | Communications of the ACM Vol. 60; no. 4; pp. 75 - 85 |
|---|---|
| Autores principales: | , , , , , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Apr2017
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=122295223&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 122295223 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Apr2017 vid: 60 iid: 4 pid: 68 pub: Association for Computing Machinery artinfo: ui: 122295223 10.1145/3051092 ppf: 75 ppct: 10 formats: tig: atl: Certifying a File System Using Crash Hoare Logic: Correctness in the Presence of Crashes. aug: au: Chajed, Tej Haogang Chen Chlipala, Adam Kaashoek, M. Frans Zeldovich, Nickolai Ziegler, Daniel affil: MIT CSAIL, Cambridge, MA su: Electronic file management Hoare logic Computer system failures Information storage & retrieval systems Automation Errors sug: subj: Electronic file management Hoare logic Computer system failures Information storage & retrieval systems Automation Errors ab: FSCQ is the first file system with a machine-checkable proof that its implementation meets a specification, even in the presence of fail-stop crashes. FSCQ provably avoids bugs that have plagued previous file systems, such as performing disk writes without sufficient 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, specified, and proved the correctness of the FSCQ file system. Although FSCQ's design is relatively simple, experiments with FSCQ as a user-level file system show that it is sufficient to run Unix applications with usable performance. FSCQ's specifications and proofs required significantly more work than the implementation, but the work was manageable even for a small team of a few researchers. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2017 holdings: @attributes: islocal: N |
|---|