Abstract
FSCQ is the first file system with a machine-checkable proof that its implementation meets a specification, even in the presence of fail-stop 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 its state 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 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.<!-- END_PAGE_1 -->
- Amani, S., Hixon, A., Chen, Z., Rizkallah, C., Chubb, P., O'Connor, L., Beeren, J., Nagashima, Y., Lim, J., Sewell, T., Tuong, J., Keller, G., Murray, T., Klein, G., Heiser, G. Cogent: Verifying high-assurance file system implementations. In Proceedings of the 21th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (Atlanta, GA, Apr. 2016), 175--188. Google ScholarDigital Library
- Bobbio, J. et al. Haskell bindings for the FUSE library, 2014. https://github.com/m15k/hfuse.Google Scholar
- Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N. Using Crash Hoare Logic for certifying the FSCQ file system. In Proceedings of the 25th ACM Symposium on Operating Systems Principles (SOSP) (Monterey, CA, Oct. 2015). Google ScholarDigital Library
- Chinner, D. xfs: Fix double free in xlog_recover_commit_trans, Sept. 2014. http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=88b863db97a18a04c90ebd57d84e1b7863114dcb.Google Scholar
- Chinner, D. xfs: xfs_dir_fsync() returns positive errno, May 2014. https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=43ec1460a2189fbee87980dd3d3e64cba2f11e1f.Google Scholar
- Chlipala, A. Mostly-automated verification of low-level programs in computational separation logic. In Proceedings of the 2011 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) (San Jose, CA, June 2011), 234--245. Google ScholarDigital Library
- Clements, A.T., Kaashoek, M.F., Zeldovich, N., Morris, R.T., Kohler, E. The scalable commutativity rule: Designing scalable software for multicore processors. In Proceedings of the 24th ACM Symposium on Operating Systems Principles (SOSP) (Farmington, PA, Nov. 2013), 1--17. Google ScholarDigital Library
- Coq development team. The Coq Proof Assistant Reference Manual, Version 8.5pl1. INRIA, Apr. 2016. http://coq.inria.fr/distrib/current/refman/.Google Scholar
- Cox, R., Kaashoek, M.F., Morris, R.T. Xv6, a simple Unix-like teaching operating system, 2014. http://pdos.csail.mit.edu/6.828/2014/xv6.html.Google Scholar
- Ernst, G., Pfahler, J., Schellhorn, G., Reif, W. Inside a verified flash file system: Transactions & garbage collection. In Proceedings of the 7th Working Conference on Verified Software: Theories, Tools and Experiments (San Francisco, CA, July 2015). Google ScholarDigital Library
- Freitas, L., Woodcock, J., Butterfield, A. POSIX and the verification grand challenge: A roadmap. In Proceedings of 13th IEEE International Conference on Engineering of Complex Computer Systems (Belfast, Northern Ireland, Mar.-Apr. 2008), 153--162. Google ScholarDigital Library
- FUSE: Filesystem in userspace, 2013. http://fuse.sourceforge.net/.Google Scholar
- Goldstein, A. ext4: Handle errors in ext4_rename, Mar. 2011. https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=ef6078930263bfcdcfe4dddb2cd85254b4cf4f5c.Google Scholar
- Gray, J. Notes on data base operating systems. In Operating Systems: An Advanced Course, R. Bayer, R.M. Graham, and G. Seegmuller, eds. Springer-Verlag, London, UK, 1978, 393--481. Google ScholarDigital Library
- Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B. Ironclad Apps: End-to-end security via automated full-system verification. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) (Broomfield, CO, Oct. 2014), 165--181. Google ScholarDigital Library
- Hoare, C.A.R. An axiomatic basis for computer programming. Commun. ACM 12 10 (Oct. 1959), 576--580. Google ScholarDigital Library
- IEEE (The Institute of Electrical and Electronics Engineers) and The Open Group. The Open Group base specifications issue 7, 2013 edition (POSIX.1-2008/Cor 1-2013), Apr. 2013.Google Scholar
- Joshi, R., Holzmann, G.J. A mini challenge: Build a verifiable filesystem. Formal Aspects Comput. 19, 2 (June 2007), 269--272. Google ScholarCross Ref
- Kara, J. ext3: Avoid filesystem corruption after a crash under heavy delete load, July 2010. https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=f25f624263445785b94f39739a6339ba9ed3275d.Google Scholar
- Kara, J. jbd2: Issue cache flush after checkpointing even with internal journal, Mar. 2012. http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=79feb521a44705262d15cc819a4117a447b11ea7.Google Scholar
- Kara, J. ext4: Fix overflow when updating superblock backups after resize, Oct. 2014. http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=9378c6768e4fca48971e7b6a9075bc006eda981d.Google Scholar
- Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Norrish, M., Kolanski, R., Sewell, T., Tuch, H., Winwood, S. seL4: Formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP) (Big Sky, MT, Oct. 2009), 207--220. Google ScholarDigital Library
- Leroy, X. Formal verification of a realistic compiler. Commun. ACM 52, 7 (July 2009), 107--115. Google ScholarDigital Library
- Lu, L., Arpaci-Dusseau, A.C., Arpaci-Dusseau, R.H., Lu, S. A study of Linux file system evolution. In Proceedings of the 11th USENIX Conference on File and Storage Technologies (FAST) (San Jose, CA, Feb 2013), 31--44. Google ScholarDigital Library
- Manana, F. Btrfs: Fix race between writing free space cache and trimming, Dec. 2014. http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=55507ce3612365a5173dfb080a4baf45d1ef8cd1.Google Scholar
- Mason, C. Btrfs: Prevent loops in the directory tree when creating snapshots, Nov. 2008. http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=ea9e8b11bd1252dcbc23afefcf1a52ec6aa3c113.Google Scholar
- Morton, A. {PATCH} ext2/ext3-ENOSPC bug, Mar. 2004. https://git.kernel.org/cgit/linux/kernel/git/tglx/history.git/commit/?id=5e9087ad3928c9d80cc62b583c3034f864b6d315.Google Scholar
- Ntzik, G., da Rocha Pinto, P., Gardner, P. Fault-tolerant resource reasoning. In Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS) (Pohang, South Korea, Nov.-Dec. 2015).Google ScholarCross Ref
- Pillai, T.S., Chidambaram, V., Alagappan, R., Al-Kiswany, S., Arpaci-Dusseau, A.C., Arpaci-Dusseau, R.H. All file systems are not created equal: On the complexity of crafting crash-consistent applications. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) (Broomfield, CO, Oct. 2014), 433--448. Google ScholarDigital Library
- Reynolds, J.C. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (Copenhagen, Denmark, July 2002), 55--74. Google ScholarDigital Library
- Rosenblum, M., Ousterhout, J. The design and implementation of a log-structured file system. In Proceedings of the 13th ACM Symposium on Operating Systems Principles (SOSP) (Pacific Grove, CA, Oct. 1991), 1--15. Google ScholarDigital Library
- Schellhorn, G., Ernst, G., Pfahler, J., Haneberg, D., Reif, W. Development of a verified flash file system. In Proceedings of the ABZ Conference (Toulouse, France, June 2014). Google ScholarDigital Library
- Schlichting, R.D., Schneider, F.B. Fail-stop processors: An approach to designing fault-tolerant computing systems. ACM Trans. Comput. Syst. 1, 3 (1983), 222--238. Google ScholarDigital Library
- Tweedie, S.C. Journaling the Linux ext2fs filesystem. In Proceedings of the 4th Annual LinuxExpo (Durham, NC, May 1998).Google Scholar
- Wang, X., Lazar, D., Zeldovich, N., Chlipala, A., Tatlock, Z. Jitk: A trustworthy in-kernel interpreter infrastructure. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) (Broomfield, CO, Oct. 2014), 33--47. Google ScholarDigital Library
- Wong, D.J. ext4: Fix same-dir rename when inline data directory overflows, Aug. 2014. https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=d80d448c6c5bdd32605b78a60fe8081d82d4da0f.Google Scholar
- Xie, M. Btrfs: Fix broken free space cache after the system crashed, June 2014. https://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id=e570fd27f2c5d7eac3876bccf99e9838d7f911a3.Google Scholar
- Yang, J., Twohey, P., Engler, D., Musuvathi, M. eXplode: A lightweight, general system for finding serious storage system errors. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI) (Seattle, WA, Nov. 2006), 131--146. Google ScholarDigital Library
- Zheng, M., Tucek, J., Huang, D., Qin, F., Lillibridge, M., Yang, E.S., Zhao, B.W., Singh, S. Torturing databases for fun and profit. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) (Broomfield, CO, Oct. 2014), 449--464. Google ScholarDigital Library
Index Terms
- Certifying a file system using crash hoare logic: correctness in the presence of crashes
Recommendations
Verifying a high-performance crash-safe file system using a tree specification
SOSP '17: Proceedings of the 26th Symposium on Operating Systems PrinciplesDFSCQ is the first file system that (1) provides a precise specification for fsync and fdatasync, which allow applications to achieve high performance and crash safety, and (2) provides a machine-checked proof that its implementation meets this ...
Comments