PerSeVerE: Persistency Semantics for Verification under Ext4

被引：9
|
作者：
Kokologiannakis, Michalis [1 ]
Kaysin, Ilya [2 ]
Raad, Azalea [3 ]
Vafeiadis, Viktor [1 ]
机构：
[1] MPI SWS, Saarland Informat Campus, Saarbrucken, Germany
[2] Natl Res Univ Higher Sch Econ, JetBrains Res, Moscow, Russia
[3] Imperial Coll London, London, England
来源：
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2021年 / 5卷 / POPL期
基金：
欧洲研究理事会;
关键词：
File Systems; Persistency; Weak Consistency; Model Checking; CONSISTENCY;
D O I：
10.1145/3434324
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页数：29
相关论文
共 43 条
  • [1] Evolving Ext4 for Shingled Disks
    Aghayev, Abutalib
    Ts'o, Theodore
    Gibson, Garth
    Desnoyers, Peter
    [J]. PROCEEDINGS OF FAST '17: 15TH USENIX CONFERENCE ON FILE AND STORAGE TECHNOLOGIES, 2017, : 105 - 119
  • [2] An analysis of Ext4 for digital forensics
    Fairbanks, Kevin D.
    [J]. DIGITAL INVESTIGATION, 2012, 9 : S118 - S130
  • [3] AFEIC: Advanced forensic Ext4 inode carving
    Dewald, Andreas
    Seufert, Sabine
    [J]. DIGITAL INVESTIGATION, 2017, 20 : S83 - S91
  • [4] Competition of Virtualized Ext4, Xfs and Btrfs Filesystems Under Type-2 Hypervisor
    Pesic, Dj
    Djordjevic, B.
    Timcenko, V.
    [J]. 2016 24TH TELECOMMUNICATIONS FORUM (TELFOR), 2016, : 774 - 777
  • [5] Block and Inode Based Analysis on EXT4 File System
    Yudha, Fietyata
    Prayudi, Yudi
    [J]. ADVANCED SCIENCE LETTERS, 2018, 24 (01) : 652 - 655
  • [6] Guaranteeing the Metadata Update Atomicity in EXT4 File system
    Son, Seongbae
    Yoo, Jinsoo
    Won, Youjip
    [J]. PROCEEDINGS OF THE 8TH ASIA-PACIFIC WORKSHOP ON SYSTEMS (APSYS '17), 2017,
  • [7] Performance Analysis of SSD write using TRIM in NTFS and EXT4
    Kim, Giryoung
    Shin, Dongkun
    [J]. 2011 6TH INTERNATIONAL CONFERENCE ON COMPUTER SCIENCES AND CONVERGENCE INFORMATION TECHNOLOGY (ICCIT), 2012, : 422 - 423
  • [8] Tuning the Ext4 Filesystem Performance for Android-Based Smartphones
    Kim, Hyeong-Jun
    Kim, Jin-Soo
    [J]. FRONTIERS IN COMPUTER EDUCATION, 2012, 133 : 745 - 752
  • [9] Adaptive Data Wiping Scheme with Adjustable Parameters for Ext4 File System
    Zhang Peng
    Niu Shaozhang
    Huang Zhenpeng
    Qin Xiaohua
    [J]. CHINESE JOURNAL OF ELECTRONICS, 2017, 26 (02) : 392 - 398
  • [10] LOCKED-Free Journaling: Improving the Coalescing Degree in EXT4 Journaling
    Koo, Kyoungho
    Park, Yongjun
    Won, Youjip
    [J]. 2020 9TH IEEE NON-VOLATILE MEMORY SYSTEMS AND APPLICATIONS SYMPOSIUM (NVMSA 2020), 2020, : 36 - 41
12345