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.