Transactional Data Management for Multi-Site Systems: New Approaches and Formal Analysis
AbstractHigh-impact systems, notably systems used in health care, public infrastructure, traffic control, and finance, depend on a data management facility that can tolerate many types of failure. In addition, the prevalent adoption of cloud systems increase the demand for commodity services to provide consistent and efficient data storage services. For commodity services, strong fault tolerance and scalability are necessary. However, achieving the desired level of fault tolerance requires multi-site repli- cation: multiple copies of data are stored at geographically distant sites. Combining such data replication with the transactional consistency guarantees provided by a traditional database system is challenging, and users are usually required to choose between consistency, performance, and fault tolerance. Google's Megastore is among the most mature multi-site data stores providing transactions. However, one challenge with Megastore is that it requires data to be grouped into a set of relatively fine-grained partitions, and transactional consistency is only provided within one partition. In some usage scenarios, this represents a signifficant disadvantage. The main contributions of this thesis are: 1) three new approaches for transactional multi-site data management, including an extension of Megastore to provide cross-partition consistency; 2) a formal-methods-based analysis strategy using Real-Time Maude to assess both performance and correctness; and 3) a formal model of Megastore that provides the first reasonably detailed publicly available description of the Megastore approach to data management in multisite data stores.
List of papers
|1. J. Grov, L. Soares, A. Correia Jr, J. Pereira, R. Oliveira, F. Pedone. \A Pragmatic Protocol for Database Replication in Interconnected Clusters". In: Proc. of the 12th Paciffic Rim International Symposium on Dependable Com- puting (PRDC 2006). IEEE Computer Society, 2006. © 2006 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works. The published version of this paper is available at: https://doi.org/10.1109/PRDC.2006.11|
|2. J. Grov, P. Ölveczky. \Scalable and Fully Consistent Transactions in the Cloud through Hierarchical Validation". In: Proc. of the 6th International Conference on Data Management in Cloud, Grid and P2P Systems (Globe 2013), volume 8059 of Lecture Notes in Computer Science, Springer, 2013. The published version of this paper is available at: https://doi.org/10.1007/978-3-642-40053-7_3|
|3. J. Grov, P. Ölveczky. \Formal Modeling and Analysis of Google's Megastore in Real-Time Maude". In: Speciffication, Algebra, and Software, volume 8373 of Lecture Notes in Computer Science, Springer, 2014. The published version of this paper is available at: https://doi.org/10.1007/978-3-642-54624-2_25|
|4. J. Grov, P. Ölveczky. \Increasing Consistency in Multi-Site Data Stores: Megastore-CGC and its Formal Analysis". Submitted for publication, 2014.|