====== Formally Verified Concurrent File System (AtomFS) and CRL-H Framework ======

===== News =====
  *2019 Aug. 27: our AtomFS paper has been accepted by SOSP 2019

===== Overview =====
Concurrent file systems are pervasive but hard to correctly implement and formally verify due to nondeterministic interleavings. We present AtomFS, the first formally-verified concurrent file system with our CRL-H framework, which provides linearizable interfaces to applications. 
We have successfully applied CRL-H to verify the linearizability of AtomFS. All the proofs are mechanized in Coq. Evaluations show that AtomFS speeds up file system workloads by utilizing multicore concurrency.



===== CRL-H Framework =====
The standard way to prove linearizability requires modeling linearization point of each operation---the moment when its effect becomes visible atomically to other threads. We observe that path inter-dependency, where one operation (like rename) breaks the path integrity of other operations, makes the linearization point external and thus poses a significant challenge to prove linearizability.

To overcome the above challenge, we propose __C__oncurrent __R__elational __L__ogic with __H__elpers (CRL-H), a framework for building verified concurrent file systems. CRL-H is made powerful through two key contributions: (1) extending prior approaches using fixed linearization points with a helper mechanism where one operation of the thread can logically help other threads linearize their operations; (2) combining relational specifications and rely-guarantee conditions for relational and compositional reasoning. We have successfully applied CRL-H to verify the linearizability of AtomFS. All the proofs are mechanized in Coq. 

===== People =====
=== Faculties ===
  *[[pub:members:Haibo Chen]]  
=== Students ===
  *[[pub:members:Mo Zou]], Haoran Ding, [[http://dongd.info/|Dong Du]]
=== Collaborators ===
  *Ming Fu
  *[[https://www.cs.columbia.edu/~rgu/|Ronghui Gu]]

===== Publication =====
  *[**SOSP 2019**] Using Concurrent Relational Logic with Helpers for Verifying the AtomFS File System. Mo Zou, Haoran Ding, Dong Du, Ming Fu, Ronghui Gu, Haibo Chen. Proceedings of the 27th ACM Symposium on Operating Systems Principles. [{{:publications:sosp19-zou.pdf|paper}}]

===== Source Code =====

Coming soon
===== Acknowledgements =====
We sincerely thank our shepherd Don Porter, the PDOS group and the anonymous reviewers for their insightful comments.
We thank Xinyu Feng and Hongjin Liang for their advices on CRL-H and proofs of AtomFS.
We also thank Mingkai Dong for his initial effort in helping implement the AtomFS file system.
This work is supported in part by the National Key Research & Development Program (No. 2016YFB1000104), and the National Natural Science Foundation of China (No. 61772335).