PHÂN TÍCH VÀ KIỂM CHỨNG KIẾN TRÚC HAYSTACK TRONG MẠNG XÃ HỘI FACEBOOK

Abstract

Haystack is a storage system architecture optimized for Facebook’s photo application. Current haystack has four main advantages compared to previous versions, including high throughput and low latency, fault tolerance, cost effectiveness, and simplicity. Given the widespread use of the Haystack architecture in Facebook, its validity and other key attributes abstracted from this architecture need to be analyzed and verified with a more precise approach. This paperfocuses 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 crucial properties, including basic property and supplementary properties. Basic property contains Deadlock Freedom. Supplementary properties include synchronous and asynchronous concurrent access, and synchronous concurrent access with the same client, synchronous concurrent 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 are valid, which means that it meets the requirements of the documents of Facebook.