基于锁耦合遍历算法的文件系统终止性验证
作者:
作者单位:

作者简介:

邹沫(1994-),男,博士生,主要研究领域为操作系统,形式化验证;
魏卓然(1998-),男,主要研究领域为操作系统,形式化验证;
谢昊彤(1999-),男,主要研究领域为操作系统,形式化验证;
陈海波(1982-),男,博士,教授,博士生导师,CCF杰出会员,主要研究领域为操作系统,并行与分布式系统.

通讯作者:

陈海波,E-mail:haibochen@sjtu.edu.cn

中图分类号:

TP311

基金项目:

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


Verification of Termination for File System Based on Lock Coupling Traversal
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

邹沫,谢昊彤,魏卓然,陈海波.基于锁耦合遍历算法的文件系统终止性验证.软件学报,2022,33(8):2980-2994

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-08
  • 最后修改日期:2022-01-10
  • 录用日期:
  • 在线发布日期: 2022-02-22
  • 出版日期: 2022-08-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号