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

邹沫(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:
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [52]
  • |
  • 相似文献 [20]
  • | | |
  • 文章评论
    摘要:

    并发文件系统由于复杂的实现,容易产生死锁、无限循环等终止性漏洞,已有的文件系统证明工作都忽视了终止性的证明.证明了一个并发文件系统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.

    参考文献
    [1] Cai M, Huang H, Huang J.Understanding security vulnerabilities in file systems.In:Proc.of the 10th ACM SIGOPS Asia-Pacific Workshop on Systems.2019.8-15.
    [2] Klein G, Elphinstone K, Heiser G, et al.seL4:Formal verification of an OS kernel.In:Proc.of the ACM SIGOPS 22nd Symp.on Operating Systems Principles.2009.207-220.
    [3] Wang J, Zhan NJ, Feng XY, et al.Overview of formal methods.Ruan Jian Xue Bao/Journal of Software, 2019, 30(1):33-61(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [4] Chen H, Ziegler D, Chajed T, et al.Using Crash Hoare logic for certifying the FSCQ file system.In:Proc.of the 25th Symp.on Operating Systems Principles.2015.18-37.
    [5] Sigurbjarnarson H, Bornholt J, Torlak E, et al.Push-button verification of file systems via crash refinement.In:Proc.of the 12th{USENIX}Symp.on Operating Systems Design and Implementation (OSDI 2016).2016.1-16.
    [6] Amani S, Hixon A, Chen Z, et al.Cogent:Verifying high-assurance file system implementations.ACM SIGARCH Computer Architecture News, 2016, 44(2):175-188.
    [7] Zou M, Ding H, Du D, et al.Using concurrent relational logic with helpers for verifying the AtomFS file system.In:Proc.of the 27th ACM Symp.on Operating Systems Principles.2019.259-274.
    [8] Liang H, Feng X.A program logic for concurrent objects under fair scheduling.In:Proc.of the 43rd Annual ACM SIGPLANSIGACT Symp.on Principles of Programming Languages.2016.385-399.
    [9] Lu L, Arpaci-Dusseau AC, Arpaci-Dusseau RH, et al.A study of Linux file system evolution.In:Proc.of the 11th USENIX Conf.on File and Storage Technologies (FAST 2013).2013.31-44.
    [10] Min C, Kashyap S, Lee B, et al.Cross-checking semantic correctness:The case of finding file system bugs.In:Proc.of the 25th Symp.on Operating Systems Principles.2015.361-377.
    [11] Lu S, Park S, Seo E, et al.Learning from mistakes:A comprehensive study on real world concurrency bug characteristics.In:Proc.of the 13th Int'l Conf.on Architectural Support for Programming Languages and Operating Systems.2008.329-339.
    [12] Su XH, Yu Z, Wang TT, et al.A survey on exposing, detecting and avoiding concurrency bugs.Chinese Journal of Computers, 2015, 395(11):93-111(in Chinese with English abstract).[doi:10.11897/SP.J.1016.2015.02215]
    [13] Wang Y, Kelly T, Kudlur M, et al.Gadara:Dynamic deadlock avoidance for multithreaded programs.In:Proc.of the OSDI.2008, 8:281-294.
    [14] Jula H, Tralamazza DM, Zamfir C, et al.Deadlock immunity:Enabling systems to defend against deadlocks.In:Proc.of the OSDI.2008.295-308.
    [15] Burnim J, Jalbert N, Stergiou C, et al.Looper:Lightweight detection of infinite loops at runtime.In:Proc.of the 2009 IEEE/ACM Int'l Conf.on Automated Software Engineering.IEEE, 2009.161-169.
    [16] Carbin M, Misailovic S, Kling M, et al.Detecting and escaping infinite loops with Jolt.In:Proc.of the European Conf.on Objectoriented Programming.Berlin, Heidelberg:Springer, 2011.609-633.
    [17] Lu FM, Zheng JJ, Bao YX, et al.Deadlock detection of multithreaded programs based on lock-augmented segmentation graph.Ruan Jian Xue Bao/Journal of Software, 2021, 32(6):1682-1700(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/6244.htm[doi:10.13328/j.cnki.jos.006244]
    [18] Chen H, Chajed T, Konradi A, et al.Verifying a high-performance crash-safe file system using a tree specification.In:Proc.of the 26th Symp.on Operating Systems Principles.2017.270-286.
    [19] Hawblitzel C, Howell J, Kapritsos M, et al.IronFleet:Proving practical distributed systems correct.In:Proc.of the 25th Symp.on Operating Systems Principles.2015.1-17.
    [20] Gu R, Shao Z, Kim J, et al.Certified concurrent abstraction layers.ACM SIGPLAN Notices, 2018, 53(4):646-661.
    [21] Gu R, Shao Z, Chen H, et al.Certikos:An extensible architecture for building certified concurrent OS kernels.In:Proc.of the 12th{USENIX}Symp.on Operating Systems Design and Implementation (OSDI 2016).2016.653-669.
    [22] Kim J, Sjöberg V, Gu R, et al.Safety and liveness of MCS lock-Layer by layer.In:Proc.of the Asian Symp.on Programming Languages and Systems.Cham:Springer, 2017.273-297.
    [23] Oberhauser J, Chehab RLL, Behrens D, et al.VSync:Push-button verification and optimization for synchronization primitives on weak memory models.In:Proc.of the 26th ACM Int'l Conf.on Architectural Support for Programming Languages and Operating Systems.2021.530-545.
    [24] Liang H, Feng X.Progress of concurrent objects with partial methods.Proc.of the ACM on Programming Languages, 2017, 2(POPL):1-31.
    [25] D'Osualdo E, Farzan A, Gardner P, et al.TaDA live:Compositional reasoning for termination of fine-grained concurrent programs.arXiv preprint arXiv:1901.05750, 2019.
    [26] Liang H, Feng X, Shao Z.Compositional verification of termination-preserving refinement of concurrent programs.In:Proc.of the Joint Meeting of the 23rd EACSL Annual Conf.on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symp.on Logic in Computer Science (LICS).2014.1-10.
    [27] Liang H, Hoffmann J, Feng X, et al.Characterizing progress properties of concurrent objects via contextual refinements.In:Proc.of the Int'l Conf.on Concurrency Theory.Berlin, Heidelberg:Springer, 2013.227-241.
    [28] Leroy X.A formally verified compiler back-end.Journal of Automated Reasoning, 2009, 43(4):363-446.
    [29] Hoffmann J, Marmar M, Shao Z.Quantitative reasoning for proving lock-freedom.In:Proc.of the 28th Annual ACM/IEEE Symp.on Logic in Computer Science.IEEE, 2013.124-133.
    [30] Herlihy M, Shavit N.The Art of Multiprocessor Programming.Morgan Kaufmann Publishers, 2020.
    [31] Ma JB, Fu M, Feng XY.Formal verification of the message queue communication mechanism in μC/OS-II.Journal of Chinese Computer Systems, 2016, 37(6):1179-1184(in Chinese with English abstract).
    [32] Xu FW.Design and implementation of a verification framework for preemptive OS kernels[Ph.D.Thesis].Hefei:University of Science and Technology of China, 2016(in Chinese with English abstract).
    [33] Feng X.Local rely-guarantee reasoning.In:Proc.of the 36th Annual ACM SIGPLAN-SIGACT Symp.on Principles of Programming Languages.2009.315-327.
    [34] Liang HJ.Refinement verification of concurrent programs and its applications[Ph.D.Thesis].Hefei:University of Science and Technology of China, 2014(in Chinese with English abstract).
    [35] Cao HX, Feng XY.Linearizability of a lock-free concurrent skiplist.Journal of Chinese Computer Systems, 2015, 36(6):1158-1164(in Chinese with English abstract).
    [36] Owicki S, Gries D.Verifying properties of parallel programs:An axiomatic approach.Communications of the ACM, 1976, 19(5):279-285.
    [37] Ma D, Fu M, Qiao L, et al.Formal specification and verification of complex kernel data structures.Journal of Chinese Computer Systems, 2019, 40(2):359-366(in Chinese with English abstract).
    [38] Gu HB, Fu M, Qiao L, et al.Formalization and verification of several global properties of SpaceOS.Journal of Chinese Computer Systems, 2019, 40(1):141-148(in Chinese with English abstract).
    [39] Zhang HR, Fu M.Design and implementation of Coq tactics based on Z3.Ruan Jian Xue Bao/Journal of Software, 2017, 28(4):819-826(in Chinese with English abstract).http://www.jos.org.cn/1000-9825/5196.htm[doi:10.13328/j.cnki.jos.005196]
    [40] Schirmer N.Verification of sequential imperative programs in Isabelle/HOL[Ph.D.Thesis].München:Technische Universität München, 2006.
    [41] Sanán D, Zhao Y, Hou Z, et al.Csimpl:A rely-guarantee-based framework for verifying concurrent programs.In:Proc.of the Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems.Berlin, Heidelberg:Springer, 2017.481-498.
    附中文参考文献:
    [3] 王戟,詹乃军,冯新宇,等.形式化方法概貌.软件学报, 2019, 30(1):33-61.http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [12] 苏小红,禹振,王甜甜,等.并发缺陷暴露、检测与规避研究综述.计算机学报, 2015, 395(11):93-111.[doi:10.11897/SP.J.1016.2015.02215]
    [17] 鲁法明,郑佳静,包云霞,等.基于锁增广分段图的多线程程序死锁检测.软件学报, 2021, 32(6):1682-1700.http://www.jos.org.cn/1000-9825/6244.htm[doi:10.13328/j.cnki.jos.006244]
    [31] 马杰波,付明,冯新宇.μC/OS-II中消息队列通信机制的形式化验证.小型微型计算机系统, 2016, 37(6):1179-1184.
    [32] 许峰唯.抢占式操作系统内核验证框架的设计和实现[博士学位论文].合肥:中国科学技术大学, 2016.
    [34] 梁红瑾.并发程序精化验证及其应用[博士学位论文].合肥:中国科学技术大学, 2014.
    [35] 曹红星,冯新宇.一种无锁并发跳表算法的可线性化证明.小型微型计算机系统, 2015, 36(6):1158-1164.
    [37] 马顶,付明,乔磊,等.复杂内核数据结构的形式化描述和验证.小型微型计算机系统, 2019, 40(2):359-366.
    [38] 顾海博,付明,乔磊,等.SpaceOS中若干全局性质的形式化描述和验证.小型微型计算机系统, 2019, 40(1):141-148.
    [39] 张恒若,付明.基于Z3的Coq自动证明策略的设计和实现.软件学报, 2017, 28(4):819-826.http://www.jos.org.cn/1000-9825/5196.htm[doi:10.13328/j.cnki.jos.005196]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

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

京公网安备 11040202500063号