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

作者简介:

通讯作者:

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

中图分类号:

TP311

基金项目:

国家杰出青年基金(61925206)


Verification of Termination for a 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, we face two major challenges applying the idea. (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, we may find multiple sources of obstruction globally, which leads to the loss of locality in proof; (2) The rename operation need 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 paper 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. We have successfully built a framework called CRL-T for termination verification and apply it to verify the termination of AtomFS. All the proofs are mechanized in Coq.

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

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

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

京公网安备 11040202500063号