University:
Boston University
Course:
MET CS 201 | Introduction to Programming
Academic year:

2021
Views:

290

Pages:

19
Author:

SpaceCadet101

CHL’s recovery semantics create is atomic, if log_recover runs after every crash: SPEC create(dnum, fn) ON CRASH log_recover() PRE disk: log_rep(NoTxn, start_state) start_state: dir_rep(tree) ∧ ∃ path, tree[path].inode = dnum ∧ fn ∈ / tree[path] POST disk: log_rep(NoTxn, new_state) new_state: dir_rep(new_tree) ∧ new_tree = tree.update(path, fn, empty_file) RECOVER disk: log_rep(NoTxn, start_state) ∨ log_rep(NoTxn, new_state) CHL summary Key ideas: crash conditions and recovery semantics CHL benefit: enables precise failure specifications Allows for automatic chaining of pre/post/crash conditions Reduces proof burden CHL cost: must write crash condition for every function, loop, etc. Crash conditions are often simple (above logging layer) FSCQ : building a file system on top of CHL File system design is close to v6 Unix, plus logging, minus symbolic links Implementation aims to reduce proof effort Reducing proof effort Reuse proven components E.g., finding a free object in a bitmap allocator Typical C code: iterate over each 64-bit chunk in a 4KB block, use bitwise operations to find a zero bit Less proof effort: use marshaling library; decode bitmap block into 32,768-element array of 1-bit elements; loop over array Many precise internal abstraction layers Files: inode; block-level file; byte-level file Directory: directory entries; filename encoding; tree structure Simpler specifications No hard links ⇒ logical state is a tree, not a graph Evaluation What bugs do FSCQ ’s theorems eliminate? How much development effort is required for How well does FSCQ perform? FSCQ ? FSCQ ’s theorems eliminate many bugs One data point: once theorems proven, no implementation bugs Did find some mistakes in spec, as a result of end-to-end checks E.g., forgot to specify that extending a file should zero-fill FSCQ ’s theorems eliminate many bugs One data point: once theorems proven, no implementation bugs Did find some mistakes in spec, as a result of end-to-end checks E.g., forgot to specify that extending a file should zero-fill Common classes of bugs found in Linux file systems: Bug class Eliminated in FSCQ ? Violating file or directory invariants Improper handling of corner cases Returning incorrect error codes Resource-allocation bugs Mistakes in logging and recovery logic Misusing the logging API Bugs due to concurrent execution Low-level programming errors Yes Yes Some Some Yes Yes No concurrency Yes Implementing CHL and FSCQ in Coq Total of ∼30,000 lines of verified code, specs, and proofs Comparison: xv6 file system is ∼3,000 lines of code Change effort proportional to scope of change Reordering disk writes: ∼1,000 lines in F SCQ L OG Indirect blocks: ∼1,500 lines in inode layer Buffer cache: ∼300 lines in F SCQ L OG, ∼600 lines in rest of FSCQ Optimize log layout: ∼150 lines in F SCQ L OG Modest incremental effort, partially due to CHL’s proof automation and FSCQ ’s internal layers Change effort proportional to scope of change Reordering disk writes: ∼1,000 lines in F SCQ L OG Indirect blocks: ∼1,500 lines in inode layer Buffer cache: ∼300 lines in F SCQ L OG, ∼600 lines in rest of FSCQ Optimize log layout: ∼150 lines in F SCQ L OG Modest incremental effort, partially due to CHL’s proof automation and FSCQ ’s internal layers Change effort proportional to scope of change Reordering disk writes: ∼1,000 lines in F SCQ L OG Indirect blocks: ∼1,500 lines in inode layer Buffer cache: ∼300 lines in F SCQ L OG, ∼600 lines in rest of FSCQ Optimize log layout: ∼150 lines in F SCQ L OG Modest incremental effort, partially due to CHL’s proof automation and FSCQ ’s internal layers Change effort proportional to scope of change Reordering disk writes: ∼1,000 lines in F SCQ L OG Indirect blocks: ∼1,500 lines in inode layer Buffer cache: ∼300 lines in F SCQ L OG, ∼600 lines in rest of FSCQ Optimize log layout: ∼150 lines in F SCQ L OG Modest incremental effort, partially due to CHL’s proof automation and FSCQ ’s internal layers Change effort proportional to scope of change Reordering disk writes: ∼1,000 lines in F SCQ L OG Indirect blocks: ∼1,500 lines in inode layer Buffer cache: ∼300 lines in F SCQ L OG, ∼600 lines in rest of FSCQ Optimize log layout: ∼150 lines in F SCQ L OG Modest incremental effort, partially due to CHL’s proof automation and FSCQ ’s internal layers Performance comparison File-system-intensive workload Software development: git, make LFS benchmark mailbench: qmail-like mail server Compare with other (non-certified) file systems xv6 (similar design, written in C) ext4 (widely used on Linux), in non-default synchronous mode to match FSCQ’s guarantees Running on an SSD on a laptop Running time for benchmark workload Running time (seconds) 80 70 60 50 40 30 20 10 0 FSCQ fscq xv6 slower than xv6 due to overhead of extracted Haskell Running time for benchmark workload Running time (seconds) 80 70 60 50 40 30 20 10 0 FSCQ FSCQ fscq xv6 ext4 slower than xv6 due to overhead of extracted Haskell slower than ext4 due to simple write-ahead logging design Opportunity: change semantics to defer durability Running time (seconds) 80 70 60 50 40 30 20 10 0 fscq xv6 ext4 ext4-async slower than xv6 due to overhead of extracted Haskell FSCQ slower than ext4 due to simple write-ahead logging design Deferred durability (ext4’s default mode) allows for big improvement FSCQ Directions for future research Formalizing deferred durability (e.g., fsync) Certifying a parallel (multi-core) file system Certifying applications with CHL (database, key-value store, ...) Conclusions CHL helps specify and prove crash safety Crash conditions Recovery execution semantics FSCQ : first certified crash-safe file system Usable performance 1.5 years of effort, including learning Coq and building CHL Many open problems and potential for fundamental contributions