{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,23]],"date-time":"2026-08-23T17:43:06Z","timestamp":1787506986712,"version":"build-2736575974"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683289"],"award-info":[{"award-number":["683289"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002261","name":"RFBR","doi-asserted-by":"crossref","award":["18-01-00380"],"award-info":[{"award-number":["18-01-00380"]}],"id":[{"id":"10.13039\/501100002261","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>Although ubiquitous, modern filesystems have rather complex behaviours that are hardly understood by programmers and lead to severe software bugs such as data corruption. As a first step to ensure correctness of software performing file I\/O, we formalize the semantics of the Linux ext4 filesystem, which we integrate with the weak memory consistency semantics of C\/C++. We further develop an effective model checking approach for verifying programs that use the filesystem. In doing so, we discover and report bugs in commonly-used text editors such as vim, emacs and nano.<\/jats:p>","DOI":"10.1145\/3434324","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["PerSeVerE: persistency semantics for verification under ext4"],"prefix":"10.1145","volume":"5","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7905-9739","authenticated-orcid":false,"given":"Michalis","family":"Kokologiannakis","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ilya","family":"Kaysin","sequence":"additional","affiliation":[{"name":"National Research University Higher School of Economics, Russia \/ JetBrains Research, Russia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Azalea","family":"Raad","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8436-0334","authenticated-orcid":false,"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_2_1_2_1","volume-title":"url: https:\/\/en.wikipedia.org\/wiki\/Advanced_Format (visited on","author":"Advanced Format","year":"2020","unstructured":"Advanced Format ( 2020 ). url: https:\/\/en.wikipedia.org\/wiki\/Advanced_Format (visited on May 20, 2020 )."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_1_4_1","volume-title":"ZFS: The Last Word in Filesystems","author":"Oct Jef Bonwick","year":"2020","unstructured":"Jef Bonwick (Oct. 2005 ). ZFS: The Last Word in Filesystems. Library Catalog: blogs.oracle.com. url: https:\/\/blogs.oracle.com\/ bonwick\/zfs% 3A-the-last-word-in-filesystems (visited on June 17, 2020 )."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980024.2872406"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_1_7_1","volume-title":"HAL hal-01406848. url: https:\/\/hal.inria.fr\/hal-01406848\/document (visited on","author":"Chen Ran","year":"2020","unstructured":"Ran Chen, Martin Clochard, and Claude March\u00e9 ( 2016 ). \u201cA Formal Proof of a Unix Path Resolution Algorithm.\u201d In: HAL hal-01406848. url: https:\/\/hal.inria.fr\/hal-01406848\/document (visited on Nov. 16, 2020 )."},{"key":"e_1_2_1_8_1","volume-title":"url: https:\/\/en.wikipedia.org\/wiki\/Copy-on-write (visited on","year":"2020","unstructured":"Copy-on-write ( 2020 ). url: https:\/\/en.wikipedia.org\/wiki\/Copy-on-write (visited on May 20, 2020 )."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451152"},{"key":"e_1_2_1_10_1","volume-title":"GNU Emacs: An extensible, customizable, free\/libre text editor","author":"GNU","year":"2020","unstructured":"GNU Emacs ( 2019 ). GNU Emacs: An extensible, customizable, free\/libre text editor-and more. url: https:\/\/www.gnu.org\/ software\/emacs\/ (visited on June 15, 2020 )."},{"key":"e_1_2_1_11_1","volume-title":"EXT4 File-System Tuning Benchmarks. url: https:\/\/www.phoronix.com\/scan.php ?page=article& item=ext4_linux35_tuning&num=1 (visited on","year":"2020","unstructured":"ext4 benchmarks ( 2012 ). EXT4 File-System Tuning Benchmarks. url: https:\/\/www.phoronix.com\/scan.php ?page=article& item=ext4_linux35_tuning&num=1 (visited on May 20, 2020 )."},{"key":"e_1_2_1_12_1","volume-title":"url: https:\/\/bugs.launchpad.net\/ubuntu\/+source\/linux\/+bug\/317781 (visited on","year":"2020","unstructured":"Ext4 data loss ( 2009 ). url: https:\/\/bugs.launchpad.net\/ubuntu\/+source\/linux\/+bug\/317781 (visited on May 20, 2020 )."},{"key":"e_1_2_1_13_1","volume-title":"ext4 Data Structures and Algorithms. url: https:\/\/www.kernel.org\/doc\/html\/latest\/filesystems\/ext4\/ index. html (visited on","author":"Linux","year":"2020","unstructured":"ext4 Linux kernel ( 2020 ). ext4 Data Structures and Algorithms. url: https:\/\/www.kernel.org\/doc\/html\/latest\/filesystems\/ext4\/ index. html (visited on May 20, 2020 )."},{"key":"e_1_2_1_14_1","volume-title":"ext4: Filesystem corruption on panic. url: https:\/\/bugs.chromium.org\/p\/chromium\/issues\/detail?id= 502898 (visited on","year":"2020","unstructured":"ext4 corruption ( 2015 ). ext4: Filesystem corruption on panic. url: https:\/\/bugs.chromium.org\/p\/chromium\/issues\/detail?id= 502898 (visited on May 20, 2020 )."},{"key":"e_1_2_1_15_1","volume-title":"files: improve the backup procedure to ensure no data is lost. url: https:\/\/git.savannah. gnu.org\/cgit\/nano.git\/commit\/? id=a84cdaaa50a804a8b872f6d468412dadf105b3c5 (visited on","author":"Michalis Kokologiannakis","year":"2020","unstructured":"Michalis Kokologiannakis ( July 2020 ). files: improve the backup procedure to ensure no data is lost. url: https:\/\/git.savannah. gnu.org\/cgit\/nano.git\/commit\/? id=a84cdaaa50a804a8b872f6d468412dadf105b3c5 (visited on July 9, 2020 )."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1489-x"},{"key":"e_1_2_1_19_1","volume-title":"JOE-Joe's Own Editor","author":"JOE","year":"2020","unstructured":"JOE ( 2018 ). JOE-Joe's Own Editor. url: https:\/\/joe-editor. sourceforge.io (visited on June 15, 2020 )."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0022-3"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87603-8_23"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2525528.2525530"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Michalis Kokologiannakis Ilya Kaysin Azalea Raad and Viktor Vafeiadis (Jan. 2021 ). \u201cPerSeVerE: Persistency Semantics for Verification under Ext4 (Supplementary Material).\u201d In: url: https:\/\/plv.mpi-sws.org\/persevere.","DOI":"10.1145\/3434324"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_26_1","volume-title":"url: http:\/\/www.man7.org\/linux\/man-pages \/index.html (visited on","author":"Linux","year":"2020","unstructured":"Linux man pages ( 2020 ). url: http:\/\/www.man7.org\/linux\/man-pages \/index.html (visited on May 20, 2020 )."},{"key":"e_1_2_1_27_1","volume-title":"Overview of the Linux Virtual File System. url: https:\/\/www.kernel.org\/doc\/html\/latest\/filesystems\/ vfs. html (visited on","author":"Richard Gooch","year":"2020","unstructured":"Richard Gooch ( 1999 ). Overview of the Linux Virtual File System. url: https:\/\/www.kernel.org\/doc\/html\/latest\/filesystems\/ vfs. html (visited on May 20, 2020 )."},{"key":"e_1_2_1_28_1","first-page":"33","volume-title":"OSDI 2018","author":"Mohan Jayashree","year":"2018","unstructured":"Jayashree Mohan, Ashlie Martinez, Soujanya Ponnapalli, Pandian Raju, and Vijay Chidambaram ( 2018 ). \u201cFinding CrashConsistency Bugs with Bounded Black-Box Crash Testing.\u201d In: OSDI 2018. Carlsbad, CA, USA: USENIX Association, pp. 33-50. url: https:\/\/www.usenix.org\/system\/files\/osdi18-mohan. pdf (visited on Nov. 16, 2020 )."},{"key":"e_1_2_1_29_1","first-page":"267","volume-title":"OSDI 2008","author":"Musuvathi Madanlal","year":"2008","unstructured":"Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, G\u00e9rard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu ( 2008 ). \u201cFinding and Reproducing Heisenbugs in Concurrent Programs.\u201d In: OSDI 2008. USENIX Association, pp. 267-280. url: https:\/\/www.usenix.org\/legacy\/events\/osdi08\/tech\/full_papers\/musuvathi\/musuvathi. pdf (visited on Nov. 16, 2020 )."},{"key":"e_1_2_1_30_1","volume-title":"The GNU Nano homepage. url: https:\/\/nano-editor","author":"GNU","year":"2020","unstructured":"GNU Nano ( 2019 ). The GNU Nano homepage. url: https:\/\/nano-editor. org (visited on June 15, 2020 )."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814306"},{"key":"e_1_2_1_32_1","first-page":"787","volume-title":"iJournaling: Fine-Grained Journaling for Improving the Latency of Fsync System Call","author":"Park Daejun","unstructured":"Daejun Park and Dongkun Shin ( 2017 ). \u201ciJournaling: Fine-Grained Journaling for Improving the Latency of Fsync System Call.\u201d In: pp. 787-798. url: https:\/\/www.usenix.org\/conference\/atc17\/technical-sessions\/presentation\/park."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3119897"},{"key":"e_1_2_1_34_1","first-page":"433","volume-title":"OSDI","author":"Pillai Thanumalayan Sankaranarayana","year":"2014","unstructured":"Thanumalayan Sankaranarayana Pillai, Vijay Chidambaram, Ramnatthan Alagappan, Samer Al-Kiswany, Andrea C. ArpaciDusseau, and Remzi H. Arpaci-Dusseau (Oct. 2014 ). \u201cAll File Systems Are Not Created Equal: On the Complexity of Crafting Crash-Consistent Applications.\u201d In: OSDI 2014. Broomfield, CO: USENIX Association, pp. 433-448. url: https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/pillai."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_2_1_36_1","volume-title":"The Open Group Base Specifications Issue 7. url: https:\/\/pubs.opengroup.org\/onlinepubs\/9699919799\/ (visited on","author":"POSIX","year":"2020","unstructured":"POSIX ( 2018 ). The Open Group Base Specifications Issue 7. url: https:\/\/pubs.opengroup.org\/onlinepubs\/9699919799\/ (visited on May 20, 2020 )."},{"key":"e_1_2_1_37_1","first-page":"16","volume-title":"Analysis and Evolution of Journaling File Systems","author":"Prabhakaran Vijayan","unstructured":"Vijayan Prabhakaran, Andrea C Arpaci-Dusseau, and Remzi H Arpaci-Dusseau ( 2005 ). \u201cAnalysis and Evolution of Journaling File Systems.\u201d In: p. 16. url: https:\/\/www.usenix.org\/legacy\/events\/usenix05\/tech\/general\/full_papers\/prabhakaran\/ prabhakaran.pdf."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276507"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371079"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360561"},{"key":"e_1_2_1_41_1","volume-title":"url: https:\/\/github.com\/google\/renameio (visited on","year":"2020","unstructured":"renameio ( 2020 ). url: https:\/\/github.com\/google\/renameio (visited on May 20, 2020 )."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815411"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2501620.2501623"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1543135.1542506"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_2"},{"key":"e_1_2_1_46_1","first-page":"1","volume-title":"OSDI","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang ( 2016 ). \u201cPush-Button Verification of File Systems via Crash Refinement.\u201d In: OSDI 2016. Savannah, GA, USA: USENIX Association, pp. 1-16. url: https:\/\/www.usenix.org\/ system\/files\/conference\/osdi16\/osdi16-sigurbjarnarson.pdf."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3124680.3124722"},{"key":"e_1_2_1_48_1","volume-title":"url: https:\/\/sqlite.org\/index. html (visited on","author":"Lite","year":"2020","unstructured":"SQLite ( 2020 ). url: https:\/\/sqlite.org\/index. html (visited on May 20, 2020 )."},{"key":"e_1_2_1_49_1","volume-title":"url: https:\/\/sqlite.org\/atomiccommit. html (visited on","author":"Atomic Commit","year":"2020","unstructured":"Atomic Commit In SQLite ( 2020 ). url: https:\/\/sqlite.org\/atomiccommit. html (visited on May 20, 2020 )."},{"key":"e_1_2_1_50_1","first-page":"1","article-title":"). \u201cScalability in the XFS file system","volume":"1996","author":"Adam Sweeney","year":"1996","unstructured":"Adam Sweeney ( 1996 ). \u201cScalability in the XFS file system. \u201d In: USENIX ATC 1996, pp. 1-14. url: https:\/\/www.usenix.org\/ legacy\/publications\/library\/proceedings\/sd96\/sweeney.html.","journal-title":"USENIX ATC"},{"key":"e_1_2_1_51_1","first-page":"235","volume-title":"Planned Extensions to the Linux Ext2\/Ext3 Filesystem","author":"Ts'o Theodore Y","unstructured":"Theodore Y Ts'o and Stephen Tweedie ( 2002 ). \u201cPlanned Extensions to the Linux Ext2\/Ext3 Filesystem.\u201d In: pp. 235-243. url: http:\/\/www.usenix.org\/publications\/library\/proceedings\/usenix02\/tech\/freenix\/tso.html."},{"key":"e_1_2_1_52_1","volume-title":"LinuxExpo","author":"Stephen C","year":"1998","unstructured":"Stephen C Tweedie ( 1998 ). \u201cJournaling the Linux ext2fs Filesystem.\u201d In: LinuxExpo 1998. url: http:\/\/e2fsprogs.sourceforge. net\/journal-design. pdf (visited on Nov. 16, 2020 )."},{"key":"e_1_2_1_53_1","volume-title":"Vim-the ubiquitous text editor","author":"Vim","year":"2020","unstructured":"Vim ( 2019 ). Vim-the ubiquitous text editor. url: https:\/\/vim. org (visited on June 15, 2020 )."},{"key":"e_1_2_1_54_1","volume-title":"OSDI","author":"Yang Junfeng","year":"2006","unstructured":"Junfeng Yang, Can Sar, and Dawson Engler (Nov. 6, 2006 ). \u201cEXPLODE: a lightweight, general system for finding serious storage system errors.\u201d In: OSDI 2006. Seattle, Washington: USENIX Association, pp. 131-146. url: https:\/\/www.usenix. org\/legacy\/event\/osdi06\/tech\/full_papers\/yang_junfeng\/yang_junfeng. pdf (visited on June 17, 2020 )."},{"key":"e_1_2_1_55_1","first-page":"449","volume-title":"OSDI 2014","author":"Zheng Mai","year":"2014","unstructured":"Mai Zheng, Joseph Tucek, Dachuan Huang, Elizabeth S Yang, Bill W Zhao, Feng Qin, Mark Lillibridge, and Shashank Singh ( 2014 ). \u201cTorturing Databases for Fun and Profit.\u201d In: OSDI 2014. Broomfield, CO: USENIX Association, pp. 449-464. url: https:\/\/www.usenix.org\/system\/files\/conference\/osdi14\/osdi14-paper-zheng_mai. pdf (visited on Nov. 16, 2020 )."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434324","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434324","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:25:34Z","timestamp":1781853934000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434324"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":55,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434324"],"URL":"https:\/\/doi.org\/10.1145\/3434324","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}