Formal Modeling and Analysis of Google’s Megastore in Real-Time Maude

  • Jon Grov
  • Peter Csaba Ölveczky
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


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.


Model Check Entity Group Message Delay Partial Order Reduction Statistical Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    AlTurki, M., Meseguer, J.: PVeStA: A parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386–392. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  2. 2.
    Baker, J., et al.: Megastore: Providing scalable, highly available storage for interactive services. In: CIDR (2011),
  3. 3.
    Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theoretical Computer Science 360(1-3), 386–414 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 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
  5. 5.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  6. 6.
    Corbett, J.C., et al.: Spanner: Google’s globally-distributed database. In: OSDI 2012, pp. 251–264. USENIX Association, Berkeley (2012)Google Scholar
  7. 7.
    Eckhardt, J., Mühlbauer, T., AlTurki, M., Meseguer, J., Wirsing, M.: Stable availability under denial of service attacks through formal patterns. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 78–93. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  8. 8.
    Grov, J., Ölveczky, P.C.: Scalable and fully consistent transactions in the cloud through hierarchical validation. In: Hameurlain, A., Rahayu, W., Taniar, D. (eds.) Globe 2013. LNCS, vol. 8059, pp. 26–38. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  9. 9.
    Lamport, L.: Paxos made simple. ACM Sigact News 32(4), 18–25 (2001)Google Scholar
  10. 10.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96, 73–155 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  12. 12.
    Ölveczky, P.C., Caccamo, M.: Formal simulation and analysis of the CASH scheduling algorithm in Real-Time Maude. In: Baresi, L., Heckel, R. (eds.) FASE 2006. LNCS, vol. 3922, pp. 357–372. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)CrossRefzbMATHGoogle Scholar
  14. 14.
    Ölveczky, P.C., Meseguer, J., Talcott, C.L.: Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude. Formal Methods in System Design 29(3), 253–293 (2006)CrossRefzbMATHGoogle Scholar
  15. 15.
    Ölveczky, P.C., Thorvaldsen, S.: Formal modeling, performance estimation, and model checking of wireless sensor network algorithms in Real-Time Maude. Theoretical Computer Science 410(2-3), 254–280 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Ölveczky, P.C., Meseguer, J.: Specification of real-time and hybrid systems in rewriting logic. Theor. Comput. Sci. 285(2), 359–405 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Ölveczky, P.C., Meseguer, J.: Semantics and pragmatics of Real-Time Maude. Higher-Order and Symbolic Computation 20(1-2), 161–196 (2007)CrossRefzbMATHGoogle Scholar
  18. 18.
    Patterson, S., Elmore, A.J., Nawab, F., Agrawal, D., El Abbadi, A.: Serializability, not serial: concurrency control and availability in multi-datacenter datastores. Proc. VLDB Endow. 5(11), 1459–1470 (2012)CrossRefGoogle Scholar
  19. 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
  20. 20.
    Stonebraker, M., Cattell, R.: 10 rules for scalable performance in ‘simple operation’ datastores. Commun. ACM 54(6), 72–80 (2011)CrossRefGoogle Scholar
  21. 21.
    Weikum, G., Vossen, G.: Concurrency Control and Recovery in Database Systems. Morgan Kaufman Publishers (2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Jon Grov
    • 1
    • 2
  • Peter Csaba Ölveczky
    • 1
    • 3
  1. 1.University of OsloNorway
  2. 2.Bekk Consulting ASNorway
  3. 3.University of Illinois at Urbana-ChampaignUSA

Personalised recommendations