sibylfs.io

Tom Ridge, SOSP'15, 2015-10-05

with David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, Peter Sewell
University of Leicester, University of Cambridge

A true story...

The POSIX specification for libc's open

POSIX, man pages, libc docs, bug reports, StackOverflow, the web, OS implementation code, file system implementation code... so many details!

The problem

It's hard to be sure what file systems are supposed to do
It's hard to be sure what real-world file systems actually do

The problem

It's hard to be sure what file systems are supposed to do
It's hard to be sure what real-world file systems actually do
And manually trying to pin down and analyse all the differences between all the libc/OS/file-system combinations is infeasible

How can we provide better specifications?

How can we validate real-world systems against these specifications?

These are fundamental and important questions...

SibylFS

What is SibylFS?

SibylFS is simultaneously

A file system specification
A test oracle that can be used to check real-world traces of file system behaviour

The SibylFS specification

Precise, unambiguous ✔
Maintainable, comprehensive, detailed ✔
Variants for POSIX, Linux, Mac, FreeBSD ✔
A "formal" specification: a machine can understand it ✔

The SibylFS test oracle

A trace is a sequence of calls and returns at the libc interface:

# processing file 'link___link_nonempty_dir1__d2__sl_dotdot_d2___nonempty_dir1__nonexist_4-int.trace' ...
        @type trace
        #####################################
        # Test link___link_nonempty_dir1__d2__sl_dotdot_d2___nonempty_dir1__nonexist_4
        #####################################
     5: mkdir "empty_dir1" 0o777
        RV_none
     6: mkdir "empty_dir2" 0o777
        RV_none
     7: mkdir "nonempty_dir1" 0o777
        RV_none
     8: mkdir "nonempty_dir1/d2" 0o777
        RV_none
     9: open "nonempty_dir1/d2/f3.txt" [O_CREAT;O_WRONLY] 0o666
        RV_num(3)
    10: write! (FD 3) "Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor inc" 83
        RV_num(83)

...

    28: link "nonempty_dir1/d2/sl_dotdot_d2" "nonempty_dir1/nonexist_4"
        RV_none

...

The SibylFS test oracle

A checked trace is similar to a trace, but bad steps are identified

# processing file 'exec_link___link_nonempty_dir1__d2__sl_dotdot_d2___nonempty_dir1__nonexist_4-int.trace' ...
        # processing file 'link___link_nonempty_dir1__d2__sl_dotdot_d2___nonempty_dir1__nonexist_4-int.trace' ...
        @type trace
        #####################################
        # Test link___link_nonempty_dir1__d2__sl_dotdot_d2___nonempty_dir1__nonexist_4
        #####################################
     6: mkdir "empty_dir1" 0o777
     7: Tau
     8: RV_none
     9: mkdir "empty_dir2" 0o777
    10: Tau
...
    73: link "nonempty_dir1/d2/sl_dotdot_d2" "nonempty_dir1/nonexist_4"
    74: Tau
    75: EPERM
# 
# Fatal error:     75: EPERM
#    no result states
# 
# Error: 
#    The spec permitted:
# RV_none
# 
# Error:     75: EPERM
#    unexpected results: EPERM
#    allowed are only: RV_none
#    continuing execution with RV_none

# trace not accepted

2 points in favour of SibylFS

Unlike traditional test suites, no need to write boring test code ✔
Checking traces is fast ✔

These advantages allow combinatorial testing across a wide range of file systems

Combinatorial testing

A script is just a sequence of calls at the libc interface. These can be easily generated.

 @type script
 #####################################
 # Test link___link_nonempty_dir1__d2__sl_dotdot_d2___nonempty_dir1__nonexist_4
 #####################################
 mkdir "empty_dir1" 0o777
 mkdir "empty_dir2" 0o777
 mkdir "nonempty_dir1" 0o777
 mkdir "nonempty_dir1/d2" 0o777
 open "nonempty_dir1/d2/f3.txt" [O_CREAT;O_WRONLY] 0o666
 write! (FD 3) "Lorem ipsum dolor sit amet, consectetur adipisicing elit, sed do eiusmod tempor inc" 83
 close (FD 3)
 ... // further setup commands
 link "nonempty_dir1/d2/sl_dotdot_d2" "nonempty_dir1/nonexist_4"
 ...

Combinatorial testing at scale

We tested >40 libc/OS/filesystem combinations
With >20k scripts for each
With multiple testing iterations

Test results

Implementation error codes are quite often non-POSIX (and the SibylFS spec tells you exactly what these deviations are)
Path resolution, particularly when a trailing slash is involved, is variable, non-POSIX
Treatment of paths referencing symlinks, particularly when the path ends in a trailing slash, is highly variable
Various overlay filesystems, and FUSE filesystems, mess up things like permissions
posixovl/VFAT (posix emulation on top of VFAT) gets link count wrong when rename overwrites a file that is linked elsewhere; possible to get to a state where the filesystem contains no files, but there is no free space (space leak)
OpenZFS on Linux 3.13.0-34 (Ubuntu Trusty): files opened with O_APPEND would not seek to the end of the file before write or pwrite (probably causing applications that use this functionality to fail)
OpenZFS on OS/X: possible to execute a sequence of calls which leads to the calling process hanging using 100% CPU, unresponsive to signals; volume cannot be unmounted, machine cannot be shut down; force unmounting may cause storage device to become unusable until next system restart
Permissions: the Linux implementation of permissions should give the same behaviour from one kernel version to the next; however, we found test scripts involving file and directory access that failed on Linux kernel 3.13 and succeeded on 3.14 which we believe is due to a buggy 3.13 implementation of permissions in edge cases

The real results

SibylFS is very accurate: trace acceptance (e.g. for Linux/ext4) is almost 100%
Things can only get better over time: virtuous circle between specification and real-world testing

You rarely get something for nothing...

Show me the pain!

The process of constructing the spec: edit spec, test, analyse/debug, repeat... for every platform of interest.
At this point I have probably hand-analysed more than 1k traces.
It took an incredibly long time, and was pretty boring, but the results of the analyses are captured in the spec.
This work only has to be done once, and everyone can benefit.
Another pain point: constructing the spec to match the traces: for maintainability, we do not want the spec to degenerate into a mass of special cases.
Another pain point: constructing the spec so that it can be used for testing, efficiently.

What could you use this for?

As a specification, to complement POSIX, or to understand particular Linux, Mac or FreeBSD behaviours
To identify all differences between file systems and OSes, and how particular file systems differ from POSIX

Directly related to SOSP:

Testing new file systems e.g. FSCQ
SibylFS as a high quality model e.g. "Scalable commutativity rule" (SOSP'13), and many others

Summary

SibylFS is a formal specification of file system behaviour
SibylFS is a test oracle that can be used to check file system behaviour
SibylFS is usable in practice for combinatorial testing and analysis of file systems

Stepping back a bit

The process we used here (develop a formal spec, and use it for testing) is a general process that could be used e.g. to provide specifications of other core components of computer systems.
TCP/IP, relaxed memory models, TLS etc.

A final slide: what does this mysterious specification look like?

My poster has an excerpt from the specification.
I think it is really readable.
I'd love to explain it to you at the poster session, then you can decide what you think!