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

Clc Number:

TP311

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:September 08,2021
  • Revised:January 10,2022
  • Adopted:
  • Online: February 22,2022
  • Published: August 06,2022
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063