PerSeVerE: persistency semantics for verification under ext4.
File(s)
Published version
OA Location
Author(s)
Kokologiannakis, Michalis
Kaysin, Ilya
Raad, Azalea
Vafeiadis, Viktor
Type
Journal Article
Abstract
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.
Date Issued
2021-01
Date Acceptance
2021-01-01
Citation
Proceedings of the ACM on Programming Languages, 2021, 5, pp.1-29
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
1
End Page
29
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
5
Copyright Statement
© 2021 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License.
License URL
Identifier
https://dl.acm.org/doi/abs/10.1145/3434324
Publication Status
Published
Article Number
POPL
Date Publish Online
2021-01