软件学报

作者：邹沫，谢昊彤，魏卓然，陈海波

单位：邹沫，上海交通大学 软件学院, 上海 20024011,谢昊彤，上海交通大学 软件学院, 上海 20024002,魏卓然，上海交通大学 软件学院, 上海 20024003,陈海波，上海交通大学 软件学院, 上海 20024004

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

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

并发文件系统由于复杂的实现,容易产生死锁、无限循环等终止性漏洞,已有的文件系统证明工作都忽视了终止性的证明.证明了一个并发文件系统AtomFS的终止性,保证了每个文件系统接口在公平调度的条件下都能返回.证明AtomFS接口的终止性要说明当其遇到阻碍时,阻碍源头(其他线程)终将产生进展,促使当前线程阻碍的消除,证明的核心在于说明锁耦合(lock coupling)遍历算法的终止性.然而还存在着两点挑战:(1)文件系统的树形结构允许阻碍的线程分布在多条路径上,全局地识别出多个阻碍源头使证明失去了局部性;(2) rename接口由于需要遍历两条路径,会带来“跨路径阻碍”现象,多个rename可能相互跨路径阻碍成环,导致无法找到阻碍源头.提出了两个核心的技术点来应对这些挑战:(1)使用局部思想仅确定单个阻碍源头;(2)使用偏序法解决跨路径阻碍成环问题.成功地构建了一个终止性证明框架CRL-T,并验证了AtomFS的终止性,所有的证明都在Coq中实现.

来源：2022年第8期

《软件学报》期刊编辑部

查看软件学报杂志2022年第8期