All File Systems Are Not Created Equal: On the Complexity of Crafting Crash-Consistent Applications
Abstract from the paper: We present the first comprehensive study of application- level crash-consistency protocols built atop modern file systems. We find that applications use complex update protocols to persist state, and that the correctness of these protocols is highly dependent on subtle behaviors of the underlying file system, which we term persistence properties. We develop a tool named B OB that empir- ically tests persistence properties, and use it to demon- strate that these properties vary widely among six pop- ular Linux file systems. We build a framework named A LICE that analyzes application update protocols and finds crash vulnerabilities, i.e., update protocol code that requires specific persistence properties to hold for cor- rectness. Using A LICE , we analyze eleven widely-used systems (including databases, key-value stores, version control systems, distributed systems, and virtualization software) and find a total of 60 vulnerabilities, many of which lead to severe consequences. We also show that A LICE can be used to evaluate the effect of new file- system designs on application-level consistency.