一句话：形式化 ext4 与 C/C++ 弱内存的持久性语义，提出模型检测验证方法并发现编辑器缺陷。
现代文件系统行为复杂，程序员难以理解，容易导致数据损坏等严重软件缺陷。本文形式化 Linux ext4 文件系统的持久性语义，并将其与 C/C++ 的弱内存一致性语义集成，以精确刻画执行文件 I/O 的程序在持久化与并发内存交互下的行为。基于该语义，作者提出一种有效的模型检测验证方法，用于检查使用文件系统的程序。评估中，该方法发现并报告了 vim、emacs、nano 等常用文本编辑器中的缺陷。
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.
@article{paperbot1151,
title = {PerSeVerE: persistency semantics for verification under ext4},
author = {Michalis Kokologiannakis and Ilya Kaysin and Azalea Raad and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434324}
}