典型文献
基于锁耦合遍历算法的文件系统终止性验证
文献摘要：
并发文件系统由于复杂的实现,容易产生死锁、无限循环等终止性漏洞,已有的文件系统证明工作都忽视了终止性的证明.证明了一个并发文件系统AtomFS的终止性,保证了每个文件系统接口在公平调度的条件下都能返回.证明AtomFS接口的终止性要说明当其遇到阻碍时,阻碍源头(其他线程)终将产生进展,促使当前线程阻碍的消除,证明的核心在于说明锁耦合(lock coupling)遍历算法的终止性.然而还存在着两点挑战:(1)文件系统的树形结构允许阻碍的线程分布在多条路径上,全局地识别出多个阻碍源头使证明失去了局部性;(2)rename接口由于需要遍历两条路径,会带来"跨路径阻碍"现象,多个rename可能相互跨路径阻碍成环,导致无法找到阻碍源头.提出了两个核心的技术点来应对这些挑战:(1)使用局部思想仅确定单个阻碍源头;(2)使用偏序法解决跨路径阻碍成环问题.成功地构建了一个终止性证明框架CRL-T,并验证了AtomFS的终止性,所有的证明都在Coq中实现.
文献关键词：
并发文件系统;终止性;形式化验证;Coq
中图分类号：
作者姓名：
邹沫;谢昊彤;魏卓然;陈海波
作者机构：
上海交通大学 软件学院, 上海 200240
文献出处：
引用格式：
[1]邹沫;谢昊彤;魏卓然;陈海波-.基于锁耦合遍历算法的文件系统终止性验证)[J].软件学报,2022(08):2980-2994
A类：
并发文件系统,AtomFS,rename,偏序法,Coq
B类：
遍历算法,终止性,统由,生死,死锁,系统接口,公平调度,返回,要说,阻碍源,线程,终将,前线,lock,coupling,两点,树形结构,多条,局地,局部性,两条路,成环,定单,CRL,形式化验证
AB值：
0.222212
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
