Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • Home
  • Attend
    • Registration Information
    • Registration Discounts
    • Venue, Hotel, and Travel
    • Students and Grants
    • Co-located Events
      • SOUPS 2016
      • HotCloud '16
      • HotStorage '16
  • Program
    • At a Glance
    • Technical Sessions
  • Activities
    • Birds-of-a-Feather Sessions
    • Poster Session
  • Participate
    • Instructions for Authors and Speakers
    • Call for Papers
    • Call for Practitioner Talks
  • Sponsorship
  • About
    • Organizers
    • Help Promote!
    • Questions
    • Past Conferences
  • Home
  • Attend
  • Program
  • Activities
  • Participate
  • Sponsorship
  • About

sponsors

Gold Sponsor
Gold Sponsor
Gold Sponsor
Gold Sponsor
Silver Sponsor
Silver Sponsor
Silver Sponsor
Silver Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Industry Partner
Industry Partner
Industry Partner

help promote

USENIX ATC '16

Get
Help Promote graphics!

connect with us


  •  Twitter
  •  Facebook
  •  LinkedIn
  •  Google+
  •  YouTube

twitter

Tweets by @usenix

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home » Using Crash Hoare Logic for Certifying the FSCQ File System
Tweet

connect with us

Using Crash Hoare Logic for Certifying the FSCQ File System

Authors: 

Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich, MIT CSAIL

Presented at SOSP '15: Link to Paper

Abstract: 

FSCQ is the first file system with a machine-checkable proof (using the Coq proof assistant) that its implementation meets its specification and whose specification includes 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 the file system 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 running 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.

Haogang Chen, MIT CSAIL

Daniel Ziegler, MIT CSAIL

Tej Chajed, MIT CSAIL

Adam Chlipala, MIT CSAIL

M. Frans Kaashoek, MIT CSAIL

Nickolai Zeldovich, MIT CSAIL

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {196219,
author = {Haogang Chen and Daniel Ziegler and Tej Chajed and Adam Chlipala and M. Frans Kaashoek and Nickolai Zeldovich},
title = {Using Crash Hoare Logic for Certifying the {FSCQ} File System},
booktitle = {2016 USENIX Annual Technical Conference (USENIX ATC 16)},
year = {2016},
address = {Denver, CO},
url = {https://www.usenix.org/conference/atc16/technical-sessions/presentation/chen_haogang},
publisher = {USENIX Association},
month = jun,
}
Download

Presentation Audio

MP3 Download

Download Audio

  • Log in or    Register to post comments

Gold Sponsors

Silver Sponsors

Media Sponsors & Industry Partners

© USENIX

  • Privacy Policy
  • Contact Us