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

键值/NoSQL存储系统是云计算革命的关键组成部分。今天的键值/NoSQL存储系统处于可用性（即快速读写）、数据一致性（跨多个客户端）和分区容忍度的权衡范围的不同点上。这个项目将更好地描述沿着这个频谱可以实现什么，使这些系统沿着频谱动态适应以满足应用需求，并对真实系统在真实条件下实现的实际可用性和一致性进行基准测试。该项目将遵循两个协同重点。第一个推力将使用可用性、一致性和分区的概率模型来分析它们之间的权衡。然后，它将设计自适应技术，以满足指定可用性约束或一致性约束的SLA（服务水平协议）或SLO（服务水平目标），同时优化其他度量。最后，这些技术将在目前工业中使用的一些领先的键值/NoSQL存储系统中实现。我们的第二个重点是将大量的形式化验证研究应用于键值/NoSQL系统。这里的工作包括使用正式的建模语言来指定键值/NoSQL存储的模型，以及使用标准和统计模型检查来分析和表征这些系统的行为。这项工作将使现有的键值/NoSQL存储系统能够在运行时适应一致性、可用性和分区容忍度之间的权衡，作为提供者和客户需求的功能。它将产生更好的sla和slo，以实用和可实现的方式结合一致性模型和可用性模型。因此，该项目将直接影响键值/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.