@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"SibylFS" -ob topic.SibylFS.bib sewellbib2.bib}}
  author = {Tom Ridge and
               David Sheets and
               Thomas Tuerk and
               Andrea Giugliano and
               Anil Madhavapeddy and
               Peter Sewell},
  title = {{SibylFS}: formal specification and oracle-based testing for {POSIX}
               and real-world file systems},
  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 \emph{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, OSX and FreeBSD behaviours.  We complement the model
with an extensive test suite of over 21000 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.  
  conf = {SOSP 2015},
  booktitle = {Proceedings of the 25th Symposium on Operating Systems Principles,
               Monterey, CA, USA},
  pages = {38--53},
  year = {2015},
  month = oct,
  optcrossref = {DBLP:conf/sosp/2015},
  project = {},
  opturl = {},
  pdf = {},
  doi = {10.1145/2815400.2815411},
  timestamp = {Fri, 02 Oct 2015 08:59:57 +0200},
  biburl = {},
  bibsource = {dblp computer science bibliography,},
  topic = {SibylFS}