This project is creating and analyzing formal specifications of some fault-tolerant storage systems. We believe that the creation and use of such specifications will produce several benefits:

• They are more accurate and more complete that the informal specifications previously published for the systems.
• The similarities and differences in the specifications make clear the design differences between the systems, and their consequences.
• The specifications can be mechanically verified to confirm some properties of the systems.

We have produced specifications for three storage systems:

• Blue (the storage system used by Hotmail),
• GFS (the Google File System as published in SOSP),
• Chain Replication (an academic design from Cornell)

This web site provides (well, actually, will provide) our report on these specifications, and the specifications themselves. We hope that you will find them educational, and that their simplicity and utility will convince you to formally specify your own (current or future) storage system.

• Andrew Birrell
• Roxana Geambasu

(coming soon)

• Technical Report
• TLA for Chain Replication
• TLA for Blue
• TLA for GFS