CSR: Medium: Availability-Consistency Tradeoffs in Key-Value and NoSQL Storage Systems

Key-Value/NoSQL存储系统是云计算革命的关键组件。当今的Key-Value/NoSQL存储系统在可用性(即快速读取和写入)、数据一致性(跨多个客户端)和分区容忍度之间处于不同的折衷范围。这个项目将更好地描述在这个频谱上可以实现的东西，使这些系统沿着频谱动态适应以满足应用需求，并对真实系统在真实条件下实现的实际可用性和一致性进行基准测试。该项目将遵循两个协同推进。第一个重点将使用可用性、一致性和分区的概率模型来分析这些之间的权衡。然后，它将设计自适应技术，以满足指定可用性约束或一致性约束的SLA(服务级别协议)或SLO(服务级别目标)，同时优化其他度量。最后，这些技术将在当今业界使用的一些领先的Key-Value/NoSQL存储系统中实施。我们的第二个目标是将大量的正式验证研究应用于Key-Value/NoSQL系统。本文的工作包括使用形式化建模语言为Key-Value/NoSQL存储指定模型，以及使用标准和统计模型检查来分析和表征这些系统的行为。这项工作将赋予现有的Key-Value/NoSQL存储系统在运行时适应一致性、可用性和分区容错之间权衡的能力，作为提供商和客户需求的函数。它将产生更好的SLA和SLO，以实用和可实现的方式将一致性模型和可用性模型结合在一起。因此，该项目将直接影响Key-Value/NoSQL存储系统的大型开发人员和用户社区。该项目将产生开放软件和有意义的数据集。

Key-value/NoSQL storage systems are a key component of the cloud computing revolution. Today's key-value/NoSQL storage systems lie at different points on the tradeoff spectrum of availability (i.e., fast reads and writes) vs. data consistency (across multiple clients) vs. partition-tolerance. This project will better characterize what is achievable along this spectrum, to make these systems dynamically adapt along the spectrum to meet application requirements, and to benchmark the actual availability and consistency achieved by real systems under real conditions.The project will follow two synergistic thrusts. The first thrust will use probabilistic models for availability, consistency, and partitions to analyze the tradeoffs among these. Then it will design adaptive techniques to meet an SLA (Service Level Agreement) or SLO (Service Level Objective) which specifies either an availability constraint or a consistency constraint, while optimizing the other metric. Finally, these techniques will be implemented in some of the leading key-value/NoSQL storage systems in use today in industry. Our second thrust will apply the large body of formal verification research to key-value/NoSQL systems. The work herein includes use of a formal modeling language to specify models for key-value/NoSQL stores, and use of standard as well as statistical model-checking to analyze and characterize the behavior of these systems.This work will imbue existing key-value/NoSQL storage systems with the ability to adapt to the tradeoffs between consistency, availability, and partition-tolerance, as a function of provider and customer requirements, at run-time. It will lead to better SLAs and SLOs that combine both consistency models and availability models in a practical and achievable way. Thus, the project will directly impact the large developer and user communities of key-value/NoSQL storage systems. The project will produce open software and meaningful datasets.