Filesystem Replication and Software Quality
A few years ago, I did a summer internship with a group at Microsoft that was building a multimaster filesystem replication product. This was a very rewarding experience for several reasons. Now that the replication product has been shipped (in Windows 2003-R2, Vista, and Windows Live Messenger), I was happy to see that my mentor for that summer, Nikolaj
Bjørner, has published a paper containing “lessons learned” from the project: “Models and Software Model Checking of a Distributed File Replication System“. The paper is worth reading, for a few reasons:
- Why is filesystem replication such a hard problem, particularly in the asynchronous, multi-master case?
The paper talks about the basic problem and the approach the group took to solving it.
- Perhaps more interestingly, how do you go about constructing a high-quality implementation of such a product?
I was impressed by the group’s emphasis on correctness. Nikolaj and Dan (the technical lead for the group) both had a CS theory background, so this is perhaps not surprising — but it’s interesting to see some of the practical techniques that they used to ensure they built a correct replication system:
- A detailed specification (on the order of a few hundred pages)
- A prototype of the system in OCaml, written concurrently with the specification but before the real implementation work began
- A high-level, executable specification of the replication protocol in AsmL. This served as both a readable description of the
protocol, as well as a way to automatically generate useful test cases.
- Using model checking to verify the correctness of certain particularly complex aspects of the protocol (distributed garbage collection, conflict resolution).
- A “simulator” that walked a random tree of filesystem operations, pausing after each node to verify that the system had correctly replicated the resulting filesystem state. Once a leaf node in the tree was reached, the simulator then backtracked, exploring another branch of the tree. The simulator was also clearly inspired by model checking techniques. By replacing certain components of the real system with virtualized ones (e.g. using a toy in-memory database), this tool could be used to test large numbers of scenarios very quickly.
- Exhaustive testing. Using the simulator and a cluster of test machines, more than 500 billion test cases were examined.