Lecture Note
Using Crash Hoare Logic for Certifying the FSCQ File System Ch 2
-
University:
Boston University -
Course:
MET CS 201 | Introduction to Programming Academic year:
2021
-
Views:
479
Pages:
12
Author:
StellarStrategist
Developers struggle with partially-updated states
commit 353b67d8ced4dc53281c88150ad295e24bc4b4c5
--- a/fs/jbd/checkpoint.c
+++ b/fs/jbd/checkpoint.c
@@ -504,7 +503,25 @@ int cleanup_journal_tail(journal_t *journal)
spin_unlock(&journal->j_state_lock);
return 1;
}
+
spin_unlock(&journal->j_state_lock);
+
+
/*
+
* We need to make sure that any blocks that were recently written out
+
* --- perhaps by log_do_checkpoint() --- are flushed out before we
+
* drop the transactions from the journal. It’s unlikely this will be
+
* necessary, especially with an appropriately sized journal, but we
+
* need this to guarantee correctness. Fortunately
+
* cleanup_journal_tail() doesn’t get called all that often.
+
*/
+
if (journal->j_flags & JFS_BARRIER)
+
blkdev_issue_flush(journal->j_fs_dev, GFP_KERNEL, NULL);
+
+
+
+
+
+
spin_lock(&journal->j_state_lock);
if (!tid_gt(first_tid, journal->j_tail_sequence)) {
spin_unlock(&journal->j_state_lock);
/* Someone else cleaned up journal so return 0 */
return 0;
}
/* OK, update the superblock to recover the freed space.
* Physical blocks come first: have we wrapped beyond the end of
* the log? */
Mistakes cause data loss [Yang et al. 2006, Pilai et al. 2014, Zheng et
al. 2014] Goal: certify a complete file system under crashes
A file system with a machine-checkable proof
that its implementation meets its specification
under normal execution
and under any sequence of crashes
including crashes during recovery Contributions
CHL: Crash Hoare Logic for persistent storage
Crash condition and recovery semantics
CHL automates parts of proof effort
Proofs mechanically checked by Coq
FSCQ :
the first certified crash-safe file system
Basic Unix-like file system (not parallel)
Simple specification for a subset of POSIX (e.g., no fsync)
About 1.5 years of work, including learning Coq FSCQ
runs standard Unix programs: mv, git, make, ... FSCQ
runs standard Unix programs: mv, git, make, ... FSCQ
runs standard Unix programs: mv, git, make, ... FSCQ
runs standard Unix programs: mv, git, make, ... How to specify what is “correct”?
Need a specification of “correct” behavior before we can prove anything
Look it up in the POSIX standard? How to specify what is “correct”?
Need a specification of “correct” behavior before we can prove anything
Look it up in the POSIX standard?
[...] a power failure [...] can cause data to be lost. The data
may be associated with a file that is still open, with one that has
been closed, with a directory, or with any other internal system
data structures associated with permanent storage. This data
can be lost, in whole or part, so that only careful inspection of
file contents could determine that an update did not occur.
IEEE Std 1003.1, 2013 Edition
POSIX is vague about crash behavior
POSIX’s goal was to specify “common-denominator” behavior
File system implementations have different interpretations
Leads to bugs in higher-level applications [Pillai et al. OSDI’14] This work: “correct” is transactional
Run every file-system call inside a transaction
def create(d, name):
log_begin()
newfile = allocate_inode()
newfile.init()
d.add(name, newfile)
log_commit() This work: “correct” is transactional
Run every file-system call inside a transaction
def create(d, name):
log_begin()
newfile = allocate_inode()
newfile.init()
d.add(name, newfile)
log_commit()
log_begin and log_commit implement a write-ahead log on disk
After crash, replay any committed transaction in the write-ahead log This work: “correct” is transactional
Run every file-system call inside a transaction
def create(d, name):
log_begin()
newfile = allocate_inode()
newfile.init()
d.add(name, newfile)
log_commit()
log_begin and log_commit implement a write-ahead log on disk
After crash, replay any committed transaction in the write-ahead log
Q: How to formally specify both normal-case and crash behavior?
Q: How to specify that it’s safe to crash during recovery itself?
Using Crash Hoare Logic for Certifying the FSCQ File System Ch 2
of 12
Report
Tell us what’s wrong with it:
Thanks, got it!
We will moderate it soon!
Free up your schedule!
Our EduBirdie Experts Are Here for You 24/7! Just fill out a form and let us know how we can assist you.
Take 5 seconds to unlock
Enter your email below and get instant access to your document