Formal Modeling and Analysis of Google’s Megastore in Real-Time Maude
Cloud systems need to replicate data to ensure scalability and high availability. To enable their use for applications where consistency of the data is important, cloud systems should provide transactions. Megastore, developed and widely applied at Google, is one of very few cloud data stores that provide transactions; i.e., both data replication, fault tolerance, and data consistency. However, the only publicly available description of Megastore is short and informal. To facilitate the widespread study, adoption, and further development of Megastore’s novel approach to transactions on replicated data, a much more detailed and precise description is needed. In this paper, we describe an executable formal model of Megastore in Real-Time Maude that we have developed. Our model is the result of many iterations resulting from correcting design flaws uncovered during Real-Time Maude analysis. We describe our model and explain how it can be simulated for QoS estimation and model checked to verify functional correctness.
KeywordsModel Check Entity Group Message Delay Partial Order Reduction Statistical Model Check
Unable to display preview. Download preview PDF.
- 2.Baker, J., et al.: Megastore: Providing scalable, highly available storage for interactive services. In: CIDR (2011), http://www.cidrdb.org
- 4.Campbell, D.G., Kakivaya, G., Ellis, N.: Extreme scale with full SQL language support in Microsoft SQL Azure. In: SIGMOD 2010, pp. 1021–1024. ACM (2010)Google Scholar
- 6.Corbett, J.C., et al.: Spanner: Google’s globally-distributed database. In: OSDI 2012, pp. 251–264. USENIX Association, Berkeley (2012)Google Scholar
- 9.Lamport, L.: Paxos made simple. ACM Sigact News 32(4), 18–25 (2001)Google Scholar
- 19.Skeirik, S., Bobba, R.B., Meseguer, J.: Formal analysis of fault-tolerant group key management using ZooKeeper. In: IEEE International Symposium on Cluster Computing and the Grid, pp. 636–641 (2013)Google Scholar
- 21.Weikum, G., Vossen, G.: Concurrency Control and Recovery in Database Systems. Morgan Kaufman Publishers (2001)Google Scholar