基于锁耦合遍历算法的文件系统终止性验证  

Verification of Termination for File System Based on Lock Coupling Traversal

作　　者：邹沫 谢昊彤 魏卓然 陈海波[1] ZOU Mo;XIE Hao-Tong;WEI Zhuo-Ran;CHEN Hai-Bo(School of Software,Shanghai Jiao Tong University,Shanghai 200240,China)

机构地区：[1]上海交通大学软件学院,上海200240

出　　处：《软件学报》2022年第8期2980-2994,共15页Journal of Software

基　　金：国家杰出青年科学基金(61925206)。

摘　　要：并发文件系统由于复杂的实现,容易产生死锁、无限循环等终止性漏洞,已有的文件系统证明工作都忽视了终止性的证明.证明了一个并发文件系统Atom FS的终止性,保证了每个文件系统接口在公平调度的条件下都能返回.证明Atom FS接口的终止性要说明当其遇到阻碍时,阻碍源头(其他线程)终将产生进展,促使当前线程阻碍的消除,证明的核心在于说明锁耦合(lock coupling)遍历算法的终止性.然而还存在着两点挑战:(1)文件系统的树形结构允许阻碍的线程分布在多条路径上,全局地识别出多个阻碍源头使证明失去了局部性;(2)rename接口由于需要遍历两条路径,会带来“跨路径阻碍”现象,多个rename可能相互跨路径阻碍成环,导致无法找到阻碍源头.提出了两个核心的技术点来应对这些挑战:(1)使用局部思想仅确定单个阻碍源头;(2)使用偏序法解决跨路径阻碍成环问题.成功地构建了一个终止性证明框架CRL-T,并验证了Atom FS的终止性,所有的证明都在Coq中实现.Termination bugs such as deadlocks and infinite loops are common in concurrent file systems due to complex implementations.Existing efforts on file system verification have ignored the termination property.Based on a verified concurrent file system,AtomFS,this paper presents the verification of its termination property,which ensures that every method call will always return under fair scheduling.Proving a method’s termination requires to show that when the method is blocked,the source thread of the obstruction will make progress.The core lies in showing the termination of the lock coupling traversal.However,two major challenges applying the idea are as following.(1)The file system is in the shape of a tree and allows threads that block others to diverge on its traversal.As a result,multiple sources of obstruction globally might be found,which leads to the loss of locality in proof,(2)The rename operation needs to traverse on two paths and could bring obstruction across the path.It not only leads to more difficulty in source location,but also could cause the failure in finding the source of obstruction when two renames block each other.This study handles these challenges through two key techniques:(1)Only recognizing each local blocking chain for source location;(2)Determining partial orders of obstruction among threads.A framework called CRL-T have been successfully built for termination verification and apply it to verify the termination of AtomFS.All the proofs are mechanized in Coq.

关 键 词：并发文件系统 终止性 形式化验证 COQ 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]