Using concurrent relational logic with helpers for verifying the AtomFS file system
| Autor: | Ronghui Gu, Dong Du, Haibo Chen, Haoran Ding, Mo Zou, Ming Fu |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
File system
Multi-core processor Linearizability Programming language Computer science Concurrency 020207 software engineering 02 engineering and technology Thread (computing) computer.software_genre Nondeterministic algorithm Linearization 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing computer Rename |
| Zdroj: | SOSP |
| DOI: | 10.1145/3341301.3359644 |
| Popis: | Concurrent file systems are pervasive but hard to correctly implement and formally verify due to nondeterministic interleavings. This paper presents AtomFS, the first formally-verified, fine-grained, concurrent file system, which provides linearizable interfaces to applications. 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, this paper presents Concurrent Relational Logic with Helpers (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 directly in C code. All the proofs are mechanized in Coq. Evaluations show that AtomFS speeds up file system workloads by utilizing fine-grained, multicore concurrency. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|