Persistency Semantics for Verification under Ext4

21 September 2020

Working with files, one can observe weak behaviors: the kernel, the file system, and the hardware affect the order and atomicity of the file operations. Besides similar effects observed in memory, the persistency problem arises: In which state are the files observed upon a crash recovery? Being poorly documented, modern filesystems are hardly understood by programmers, which leads to severe software bugs, such as data corruption.

As a first step towards solving this problem, the formal model of the Linux ext4 has been proposed. In the talk, we’ll cover this model and the extension of GenMC model checker algorithm [1], enabling one to verify software performing file I/O. In addition, there will be presented several bugs in commonly-used text editors (such as vim and nano) revealed by the algorithm.

Speaker: Ilya Kaisin

[1] GenMC model checker http://plv.mpi-sws.org/genmc/

The seminar will be held in google meet on Monday September 21 at 17:30 (google meet room: https://meet.google.com/myu-dhmz-gvu)