PerSeVerE: Persistency semantics for verification under ext4
Summary
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.Paper
-
PerSeVerE: Persistency semantics for verification under ext4.
Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, and Viktor Vafeiadis.
Proc. ACM Program. Lang. 5, POPL, Article 43 (January 2021)
[Pre-print (26 pages)] [@ACM] [Full paper with the technical appendix (33 pages)]
[Artifact @Zenodo]![[Artifacts evaluated & reusable]](aec-reusable.jpg)
![[Artifacts available]](aec-available.jpg)
![[Artifacts evaluated & functional]](aec-functional.jpg)
Implementation
People
- Michalis Kokologiannakis (MPI-SWS)
- Ilya Kaysin (National Research University Higher School of Economics, JetBrains Research)
- Azalea Raad (Imperial College London)
- Viktor Vafeiadis (MPI-SWS)
Related projects
- GenMC: A generic model checker for C/C++