Specifying a Realistic File System
Sidney Amani, Toby Murray (NICTA, University of New South Wales,, Australia)
TL;DR
This paper details the correctness specification of BilbyFs, a high-performance Linux flash file system, emphasizing asynchronous writes and verification of its fsync() implementation using a concise, nondeterministic formal approach.
Contribution
It introduces a formal correctness specification for BilbyFs that uniquely supports asynchronous writes and verifies its fsync() implementation, filling a gap in existing file system verification.
Findings
Verified the correctness of BilbyFs's fsync() implementation
Supported asynchronous writes in the formal specification
Used nondeterminism for concise formal modeling
Abstract
We present the most interesting elements of the correctness specification of BilbyFs, a performant Linux flash file system. The BilbyFs specification supports asynchronous writes, a feature that has been overlooked by several file system verification projects, and has been used to verify the correctness of BilbyFs's fsync() C implementation. It makes use of nondeterminism to be concise and is shallowly-embedded in higher-order logic.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.