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

2021
Views:

369

Pages:

12
Author:

StellarStrategist

Approach: Hoare Logic specifications {pre} code {post} SPEC disk_write(a, v ) PRE a 7→ v0 POST a 7→ v CHL extends Hoare Logic with crash conditions {pre} code {post} {crash} SPEC PRE POST CRASH disk_write(a, v ) a 7→ v0 a 7→ v a 7→ v0 ∨ a 7→ v CHL’s disk model matches what most other file systems assume: writing a single block is an atomic operation no data corruption Disk model axiom specs: disk_write, disk_read, and disk_sync Certifying larger procedures pre def bmap(inode, bnum): if bnum >= NDIRECT: indirect = log_read(inode.blocks[NDIRECT]) return indirect[bnum - NDIRECT] else: return inode.blocks[bnum] crash post Certifying larger procedures Need pre/post/crash conditions for each called procedure log_read pre post if return Function bmap return crash Certifying larger procedures CHL’s proof automation chains pre- and postconditions log_read pre post if return Function bmap return crash Certifying larger procedures CHL’s proof automation combines crash conditions log_read pre post if return Function bmap return crash Certifying larger procedures Remaining proof effort: changing representation invariants log_read pre post if return Function bmap return crash Common pattern: representation invariant SPEC PRE log_write(a, v ) disk: log_rep(ActiveTxn, start_state, old_state) old_state: a 7→ v0 POST disk: log_rep(ActiveTxn, start_state, new_state) new_state: a 7→ v CRASH disk: log_rep(ActiveTxn, start_state, any ) log_rep is a representation invariant Connects logical transaction state to an on-disk representation Describes the log’s on-disk layout using many 7→ primitives Specifying an entire system call (simplified) SPEC PRE create(dnum, fn) disk: log_rep(NoTxn, start_state) start_state: dir_rep(tree) ∧ ∃ path, tree[path].inode = dnum ∧ fn ∈ / tree[path] Specifying an entire system call (simplified) SPEC PRE POST create(dnum, fn) disk: log_rep(NoTxn, start_state) start_state: dir_rep(tree) ∧ ∃ path, tree[path].inode = dnum ∧ fn ∈ / tree[path] disk: log_rep(NoTxn, new_state) new_state: dir_rep(new_tree) ∧ new_tree = tree.update(path, fn, empty_file) Specifying an entire system call (simplified) SPEC PRE create(dnum, fn) 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) CRASH disk: log_rep(NoTxn, start_state) ∨ log_rep(NoTxn, new_state) ∨ ∃ s, log_rep(ActiveTxn, start_state, s) ∨ log_rep(CommittedTxn, start_state, new_state) ∨ . . . Specifying log recovery SPEC PRE POST log_recover() disk: log_intact(last_state, committed_state) disk: log_rep(NoTxn, last_state) ∨ log_rep(NoTxn, committed_state) CRASH disk: log_intact(last_state, committed_state) log_recover is idempotent Crash condition implies pre condition ⇒ OK to run log_recover again after a crash