SibylFS ======= Paper: "SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems" Ridge et al. (SOSP'15) Source code: https://sibylfs.github.io/ Available but hasn't seen significant development since the paper came out Why this paper? Example of what you can do if you have a spec Testing many implementations Black box: doesn't require access to implementation internals Check invariants on the specification No proofs, but formal spec for POSIX There is no single reference implementation of POSIX Detailed, sophisticated specification Handles non-determinism Finds corner cases Influenced POSIX standard What is POSIX? A standard aiming to specify the Unix interface Informally, one set of man pages for all Unix implementations Why is there a spec? Many Unix implementations loosely derived from Bell Labs / AT&T / BSD Implementations differed slightly in the details of system calls, semantics Many implementations were closed source, making it hard to reverse-engineer Challenging to develop portable applications How is it decided with is OK and what is incorrect? Experts working on different Unix forks got together, tried to reach agreement Result: POSIX specifies the agreed-on core Leaves room for implementations to be different Important standard How do people test file systems today? Run test cases and see what file systems does No standard test set for all file systems File systems behave differently Sometimes multiple outcomes are possible Several error codes are ok Sometimes file systems behave differently for same input Trailing / on pathnames What is right? What the POSIX standard says? Often too informal What popular applications expect? Many test cases check for crashes or other "serious" bugs Kernel crashes File system starts returning EROFS, EIO, etc. ... Not crashing is important but fairly weak specification Overview of SibylFS Workload (one of their test cases) -> [ FS implementation ] -> Trace of events (invoke syscall, return from syscall, etc) -> [ SibylFS oracle ] -> Allowed or disallowed by spec, plus some helpful debug information Test generator + hand-written tests script Goal is to drive the system into exhibiting interesting behaviors Test scripts Some setup file system commands Sequence of file system commands to test behavior Can have many processes; each command issued by a specific process Test has no expected return values -- just needs to drive the file system Test executor Runs scripts and produces traces Traces are invocations (name, arguments, etc.) and return (name, results) SibylFS spec Abstract state Labeled transitions: call, return, "internal" tau SibylFS test Run test script on model of file system Match model against trace non-determinism: one state may transition to several states Output: checked traces if error (trace not allowed), display error e.g., returned wrong error code What is SibylFS? Spec written in Lem Lem is a DSL for writing executable specs, by one of the paper co-authors Abstract state Implementations of FS calls on that state An executable tester Returns if a trace is ok or not ok Challenge: non-determinism Spec shouldn't be deterministic Good spec doesn't nail down all implementation details E.g., spec shouldn't say what inode number stat should return Source of non-determinism in POSIX Several possible errors are ok Depends on order of checks in implementation which one is returned The number of bytes read It is allowed to be less than the number of bytes requested The order of dir entries returned by readdir The interleaving of systems calls by different processes Solution: next-state enumeration SibylFS computes all possible next states from a given state and API call for example, one for each possible error code special operator helps write non-deterministic model: Figure 6 SibylFS explicitly maintains all possible file system states apply transition to all possible current states produces new set of possible states Contain state explosion trace tells order don't need to try all possible interleavings later trace operations will likely collapse many possible states Challenge: non-determinism in directory listing Several sources of non-determinism: POSIX doesn't specify order of directory listing Concurrent modification to directory Listing isn't atomic Another process may delete an entry while listing What is spec under concurrency modifications? if an entry is not modified it will be returned if an entry is deleted concurrently, it may be returned or not if an entry is created concurrently, it may be returned or not authors believe an entry may never be returned twice subsequent calls cannot return it again not clear if this is true of POSIX or actual implementations SibylFS must track all changes to a directory since an opendir a set of "must" entries a set of "may" entries Specification is more complex than implementation! What's the value of such a complex spec? Helps developers understand what behavior they can rely on Can check many file systems for compliance Challenge: non-determinism from concurrency Several processes may interact with the file system concurrently Interleaving at the granularity of calls No support for concurrency inside file system This could be avoided by asking the file system how it interleaved calls But that breaks black-box approach Approach: internal tau transition actually executes operation Call logs the arguments in the trace, remembers for execution Tau transition executes the call, determines possible results Trace does not include tau transition Cannot tell from the trace when actual execution occurred Return gives the result to calling process, logs result in trace The SybilFS model labeled transition system main transitions are API calls (invocation or return) separate to allow for interleaving of calls from different processes os_label: labels are call + arguments, or call result + return values, or tau list of commands the state fid table group table pid table map of directories map of files ... transition is a function from (state, label) to finite set of states os_trans: state -> label -> set of states some states are special correspond to POSIX undefined, unspecified, or implementation defined trace = sequence of labels Writing the model Standard software engineering ideas: modularity, function calls, .. Decouple spec into smaller modules: Underlying FS state: directories, files Operations on the abstract state Resolve pathnames Perform operation on "inodes" Process state: processes, file descriptors, .. Operations for whole system calls Parametrize spec with feature flags to support different Unix variants Leverage DSL support for writing non-deterministic transitions Test generation Special-purpose tool: try every system call with every combination of args Ad-hoc algorithms to avoid generating too many tests Manual equivalance partitioning Based on the properties of the file system state Special cases: read/write Need to test sequences of calls Manual 21,000 tests Measure test coverage of model (98%) Seems focused on testing the model rather than testing the implementation Black-box approach means no visibility into FS implementation Good for testing logical corner cases, not as good for testing impl corner cases Results Good news: ignoring errors and permissions, behavior is similar File systems get the common behavior right But many corner cases with problems/errors Problems in POSIX specification error clauses are out of sync e.g., link, mkdir, and open Defects OS X: pwrite(fd, -10, ...) -10 becomes big integer, oops sends SIGXFSZ to process, typically killing it posixovl/VFAT failure to decrement hard link count on rename openZFS on OS X figure 8 sequence calling process consumes 100% of CPU and ignores signals Platform conventions Linux ignores off in pwrite(fd, off, ..) when fd is opened with O_APPEND Nasty for applications that platforms have their own conventions Invariant violations a call which returns an error should not change FS state FreeBSD: open(d, O_DIR|O_CREAT|O_EXCL) -> ENOTDIR + newly created file Error codes Linux: unlink of directory should return EPERM But LSB says EISDIR OSX: rename("/", ..) -> EISDIR should return EBUSY or EINVAL Pathname resolution Linux: link /dir/ /f.txt/ -> EEXIST, but better to return ENOTDIR OSX: symlink(s1, d) symlink(s2, s1) readlink s2/ -> content of s1, but better to return EINVAL Limitations No concurrency inside file system No crashes These apply to both the spec and the test harness Cannot model non-atomic execution: the tau is a single atomic transition Cannot drive the FS implementation into interesting races or crashes Summary Specification for black-box testing of file systems Handles different types of non-determinism Executable specification: can decide if a trace is allowed Finds problems in corner cases