Please use this identifier to cite or link to this item: http://hdl.handle.net/2381/39471
Title: SibylFS: Formal specification and oracle-based testing for POSIX and real-world file systems
Authors: Ridge, Tom
Sheets, David
Tuerk, Thomas
Giugliano, Andrea
Madhavapeddy, Anil
Sewell, Peter
First Published: 4-Oct-2015
Publisher: ACM
Citation: SOSP 2015 - Proceedings of the 25th ACM Symposium on Operating Systems Principles, 2015, pp. 38-53
Abstract: Systems depend critically on the behaviour of file systems, but that behaviour differs in many details, both between implementations and between each implementation and the POSIX (and other) prose specifications. Building robust and portable software requires understanding these details and differences, but there is currently no good way to systematically describe, investigate, or test file system behaviour across this complex multi-platform interface. In this paper we show how to characterise the envelope of allowed behaviour of file systems in a form that enables practical and highly discriminating testing. We give a mathematically rigorous model of file system behaviour, SibylFS, that specifies the range of allowed behaviours of a file system for any sequence of the system calls within our scope, and that can be used as a test oracle to decide whether an observed trace is allowed by the model, both for validating the model and for testing file systems against it. SibylFS is modular enough to not only describe POSIX, but also specific Linux, OS X and FreeBSD behaviours. We complement the model with an extensive test suite of over 21 000 tests; this can be run on a target file system and checked in less than 5 minutes, making it usable in practice. Finally, we report experimental results for around 40 configurations of many file systems, identifying many differences and some serious flaws.
DOI Link: 10.1145/2815400.2815411
ISBN: 9781450338349
Links: http://dl.acm.org/citation.cfm?doid=2815400.2815411
http://hdl.handle.net/2381/39471
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Copyright is held by the owner/author(s). Publication rights licensed to ACM. Deposited with reference to the publisher’s open access archiving policy.
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
SOSP15-paper102-submitted.pdfPost-review (final submitted author manuscript)274.52 kBAdobe PDFView/Open


Items in LRA are protected by copyright, with all rights reserved, unless otherwise indicated.