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

2021
Views:

410

Pages:

14
Author:

StellarStrategist

Using Crash Hoare Logic for Certifying the FSCQ File System File systems are complex and have bugs # patches for bugs File systems are complex (e.g., Linux ext4 is ∼60,000 lines of code) and have many bugs: 500 ext3 400 300 200 100 0 Jan'04 Jan'05 Jan'06 Jan'07 Jan'08 Jan'09 Jan'10 Jan'11 Cumulative number of patches for file-system bugs in Linux; data from [Lu et al., FAST’13] File systems are complex and have bugs # patches for bugs File systems are complex (e.g., Linux ext4 is ∼60,000 lines of code) and have many bugs: 500 400 300 200 100 ext3 ext4 xfs reiserfs jfs btrfs 0 Jan'04 Jan'05 Jan'06 Jan'07 Jan'08 Jan'09 Jan'10 Jan'11 Cumulative number of patches for file-system bugs in Linux; data from [Lu et al., FAST’13] New file systems (and bugs) are introduced over time File systems are complex and have bugs # patches for bugs File systems are complex (e.g., Linux ext4 is ∼60,000 lines of code) and have many bugs: 500 400 300 200 100 ext3 ext4 xfs reiserfs jfs btrfs 0 Jan'04 Jan'05 Jan'06 Jan'07 Jan'08 Jan'09 Jan'10 Jan'11 Cumulative number of patches for file-system bugs in Linux; data from [Lu et al., FAST’13] New file systems (and bugs) are introduced over time Some bugs are serious: security exploits, data loss, etc. Much research in avoiding bugs in file systems Most research is on finding bugs: Crash injection (e.g., EXPLODE [OSDI’06]) Symbolic execution (e.g., EXE [Oakland’06]) Design modeling (e.g., in Alloy [ABZ’08]) Some elimination of bugs by proving: FS without directories [Arkoudas et al. 2004] BilbyFS [Keller 2014] UBIFS [Ernst et al. 2013] Much research in avoiding bugs in file systems Most research is on finding bugs: Crash injection (e.g., EXPLODE [OSDI’06]) Symbolic execution (e.g., EXE [Oakland’06]) Design modeling (e.g., in Alloy [ABZ’08]) Some elimination of bugs by proving: FS without directories [Arkoudas et al. 2004] BilbyFS [Keller 2014] UBIFS [Ernst et al. 2013] Reduce # bugs Much research in avoiding bugs in file systems Most research is on finding bugs: Crash injection (e.g., EXPLODE [OSDI’06]) Symbolic execution (e.g., EXE [Oakland’06]) Reduce # bugs Design modeling (e.g., in Alloy [ABZ’08]) Some elimination of bugs by proving: FS without directories [Arkoudas et al. 2004] BilbyFS [Keller 2014] UBIFS [Ernst et al. 2013] Incomplete + no crashes Reasoning about crashes is important File system must recover from crash with data intact Crash due to power failure, hardware failures, or software bugs Risk: crashes expose subtle bugs Crashes can expose that a file update involves several disk writes Appending to a file requires three disk writes: Risk: crashes expose subtle bugs Crashes can expose that a file update involves several disk writes Appending to a file requires three disk writes: Risk: crashes expose subtle bugs Crashes can expose that a file update involves several disk writes Appending to a file requires three disk writes: Risk: crashes expose subtle bugs Crashes can expose that a file update involves several disk writes Appending to a file requires three disk writes: Risk: crashes expose subtle bugs Crashes can expose that a file update involves several disk writes Appending to a file requires three disk writes: Risk: crashes expose subtle bugs Crashes can expose that a file update involves several disk writes Appending to a file requires three disk writes: