{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:10:11Z","timestamp":1750223411159,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,3,24]],"date-time":"2017-03-24T00:00:00Z","timestamp":1490313600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CNS-1053143, CCF-1253229, CNS-1563763"],"award-info":[{"award-number":["CNS-1053143, CCF-1253229, CNS-1563763"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2017,3,24]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>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.&lt;!-- END_PAGE_1 --&gt;<\/jats:p>","DOI":"10.1145\/3051092","type":"journal-article","created":{"date-parts":[[2017,3,24]],"date-time":"2017-03-24T14:54:11Z","timestamp":1490367251000},"page":"75-84","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Certifying a file system using crash hoare logic"],"prefix":"10.1145","volume":"60","author":[{"given":"Tej","family":"Chajed","sequence":"first","affiliation":[{"name":"MIT CSAIL, Cambridge, MA"}]},{"given":"Haogang","family":"Chen","sequence":"additional","affiliation":[{"name":"MIT CSAIL, Cambridge, MA"}]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"MIT CSAIL, Cambridge, MA"}]},{"given":"M. Frans","family":"Kaashoek","sequence":"additional","affiliation":[{"name":"MIT CSAIL, Cambridge, MA"}]},{"given":"Nickolai","family":"Zeldovich","sequence":"additional","affiliation":[{"name":"MIT CSAIL, Cambridge, MA"}]},{"given":"Daniel","family":"Ziegler","sequence":"additional","affiliation":[{"name":"MIT CSAIL, Cambridge, MA"}]}],"member":"320","published-online":{"date-parts":[[2017,3,24]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_2_1_2_1","volume-title":"et al. Haskell bindings for the FUSE library","author":"Bobbio J.","year":"2014","unstructured":"Bobbio , J. et al. Haskell bindings for the FUSE library , 2014 . https:\/\/github.com\/m15k\/hfuse. Bobbio, J. et al. Haskell bindings for the FUSE library, 2014. https:\/\/github.com\/m15k\/hfuse."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_1_4_1","volume-title":"Sept.","author":"Chinner D.","year":"2014","unstructured":"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. 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."},{"key":"e_1_2_1_5_1","volume-title":"May","author":"Chinner D.","year":"2014","unstructured":"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. 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."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522712"},{"key":"e_1_2_1_8_1","volume-title":"INRIA","author":"Coq","year":"2016","unstructured":"Coq development team. The Coq Proof Assistant Reference Manual, Version 8.5pl1 . INRIA , Apr. 2016 . http:\/\/coq.inria.fr\/distrib\/current\/refman\/. Coq development team. The Coq Proof Assistant Reference Manual, Version 8.5pl1. INRIA, Apr. 2016. http:\/\/coq.inria.fr\/distrib\/current\/refman\/."},{"key":"e_1_2_1_9_1","volume-title":"a simple Unix-like teaching operating system","author":"Cox R.","year":"2014","unstructured":"Cox , R. , Kaashoek , M.F. , Morris , R.T. Xv 6 , a simple Unix-like teaching operating system , 2014 . http:\/\/pdos.csail.mit.edu\/6.828\/2014\/xv6.html. 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."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29613-5_5"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2008.35"},{"key":"e_1_2_1_12_1","volume-title":"Filesystem in userspace","author":"FUSE","year":"2013","unstructured":"FUSE : Filesystem in userspace , 2013 . http:\/\/fuse.sourceforge.net\/. FUSE: Filesystem in userspace, 2013. http:\/\/fuse.sourceforge.net\/."},{"key":"e_1_2_1_13_1","volume-title":"Mar.","author":"Goldstein A.","year":"2011","unstructured":"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. 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."},{"key":"e_1_2_1_14_1","volume-title":"Operating Systems: An Advanced Course","author":"Gray J.","year":"1978","unstructured":"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. 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."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Hawblitzel C.","year":"2014","unstructured":"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. 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."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_17_1","volume-title":"The Open Group base specifications issue 7","author":"IEEE (The Institute of Electrical and Electronics Engineers) and The Open Group.","year":"2013","unstructured":"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. 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."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0022-3"},{"key":"e_1_2_1_19_1","volume-title":"July","author":"Kara J.","year":"2010","unstructured":"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. 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."},{"key":"e_1_2_1_20_1","volume-title":"Mar.","author":"Kara J.","year":"2012","unstructured":"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. 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."},{"key":"e_1_2_1_21_1","volume-title":"Oct.","author":"Kara J.","year":"2014","unstructured":"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. 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."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2591272.2591276"},{"key":"e_1_2_1_25_1","volume-title":"Dec.","author":"Manana F.","year":"2014","unstructured":"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. 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."},{"key":"e_1_2_1_26_1","volume-title":"Nov.","author":"Mason C.","year":"2008","unstructured":"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. 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."},{"key":"e_1_2_1_27_1","unstructured":"Morton A. {PATCH} ext2\/ext3-ENOSPC bug Mar. 2004. https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/tglx\/history.git\/commit\/?id=5e9087ad3928c9d80cc62b583c3034f864b6d315.  Morton A. {PATCH} ext2\/ext3-ENOSPC bug Mar. 2004. https:\/\/git.kernel.org\/cgit\/linux\/kernel\/git\/tglx\/history.git\/commit\/?id=5e9087ad3928c9d80cc62b583c3034f864b6d315."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26529-2_10"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Pillai T.S.","year":"2014","unstructured":"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. 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."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/121132.121137"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_2"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/357369.357371"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 4th Annual LinuxExpo","author":"Tweedie S.C.","year":"1998","unstructured":"Tweedie , S.C. Journaling the Linux ext2fs filesystem . In Proceedings of the 4th Annual LinuxExpo ( Durham, NC , May 1998 ). Tweedie, S.C. Journaling the Linux ext2fs filesystem. In Proceedings of the 4th Annual LinuxExpo (Durham, NC, May 1998)."},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Wang X.","year":"2014","unstructured":"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. 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."},{"key":"e_1_2_1_36_1","volume-title":"Aug.","author":"Wong D.J.","year":"2014","unstructured":"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. 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."},{"key":"e_1_2_1_37_1","volume-title":"June","author":"Xie M.","year":"2014","unstructured":"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. 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."},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Yang J.","year":"2006","unstructured":"Yang , J. , Twohey , P. , Engler , D. , Musuvathi , M. e Xplode : 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. 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."},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Zheng M.","year":"2014","unstructured":"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. 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."}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3051092","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3051092","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:54:38Z","timestamp":1750222478000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3051092"}},"subtitle":["correctness in the presence of crashes"],"short-title":[],"issued":{"date-parts":[[2017,3,24]]},"references-count":39,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,3,24]]}},"alternative-id":["10.1145\/3051092"],"URL":"https:\/\/doi.org\/10.1145\/3051092","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"type":"print","value":"0001-0782"},{"type":"electronic","value":"1557-7317"}],"subject":[],"published":{"date-parts":[[2017,3,24]]},"assertion":[{"value":"2017-03-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}