PerSeVerE: persistency semantics for verification under ext4
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis · Proceedings of the ACM on Programming Languages · 2021
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.