PerSeVerE: persistency semantics for verification under ext4.

File Description SizeFormat 
3434324.pdfPublished version894.58 kBAdobe PDFView/Open
Title: PerSeVerE: persistency semantics for verification under ext4.
Authors: Kokologiannakis, M
Kaysin, I
Raad, A
Vafeiadis, V
Item 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.
Issue Date: Jan-2021
Date of Acceptance: 1-Jan-2021
DOI: 10.1145/3434324
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.
Publication Status: Published
Open Access location:
Article Number: POPL
Online Publication Date: 2021-01
Appears in Collections:Computing

This item is licensed under a Creative Commons License Creative Commons