Formalization and Analysis of Haystack Architecture from Process Algebra Perspective

As a storage system architecture optimized for Facebook’s photo application, Haystack has four main advantages than before, including high throughput and low latency, fault-tolerance, cost-effectiveness and simplicity. With its widespread use, its validity and other major properties abstracted from the architecture need to be analyzed in a formal framework. However, to the best of our knowledge, there is nearly no research conducted to describe the communications and properties in Haystack. In this paper, we focus on the internal design of serving and uploading a photo of Haystack architecture and apply Communicating Sequential Processes (CSP) to formalize them in detail. By feeding the models into the model checker Process Analysis Toolkit (PAT), we have verified some crucial properties, including basic property and supplementary properties. Basic property contains Deadlock Freedom. Supplementary properties include synchronous concurrent access, asynchronous concurrent access, synchronous concurrent access with the same client, synchronous concurrent upload and synchronous concurrent upload with the same client. Finally, according to the verification results, we believe that from the CSP’s perspective, the properties of Haystack architecture is valid, which means that it meets the requirements of the documents of Facebook.