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
The problem
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
The SibylFS specification
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
2 points in favour of SibylFS
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
Test results
The real results
You rarely get something for nothing...
Show me the pain!
What could you use this for?
Directly related to SOSP:
Summary
Stepping back a bit
A final slide: what does this mysterious specification look like?