Compiling Distributed System Models into Implementations

将分布式系统模型编译为实现

• 批准号: RGPIN-2020-05203
• 负责人: Beschastnikh, Ivan
• 金额: $ 2.55万
• 依托单位: University of British Columbia
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2020
• 资助国家: 加拿大
• 起止时间: 2020-01-01 至 2021-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=715495
• 关键词: Compiling; Distributed; System; Models; into

Cloud computing has revolutionized computing. Enterprises, large and small, are taking advantage of the flexibility and capacity of massive data centers for their infrastructure. However, systems that run in the cloud are notoriously complex to engineer because these systems are designed to scale by executing across many machines. For example, given two events at different hosts, it is not obvious whether one of the events is causally dependent on the other, even if each event has a timestamp. Bugs in cloud-based systems can be subtle and catastrophic. For example, in 2017 a bug in Amazon's S3 storage system caused $150 million of dollars in damage for the companies that rely on Amazon AWS cloud services. Such incidents are increasingly common. Engineers who build cloud-based systems today rely on testing to gain assurance. Unfortunately, attaining reasonable distributed behavior coverage with testing is an established challenge while writing tests is tedious, error-prone, and fundamentally incomplete. State-of-the-art techniques for achieving distributed system correctness are rarely used in practice because they do not work on actual large-scale systems or because they require substantial effort and expertise. There is a growing interest in modeling languages for distributed systems, which can be checked exhaustively or proved to satisfy certain properties. However, today, the developer must manually translate a formal model of their system into an implementation. This process requires intensive effort and may introduce bugs into the implementation. This is one reason why developers rarely model their systems, electing instead to build first and debug later. In the proposed research program I will design and implement techniques to compile formal models of distributed systems, written in a high-level modeling language, into runnable implementations. As part of my research I will create a toolchain that will flip the dominant software engineering process used for cloud-based systems: developers will be able to first create formal models that they can verify, and then later compile these models into code. By deriving a runnable and equivalent implementation for free, developers will be more incentivized to create and curate formal models of their systems. The long-term goal of this research is to incentivize developers to use formal methods earlier in the design/implementation effort to decrease the number of bugs that make it into production systems. This research will generate new scientific knowledge about the modeling of distributed systems and compilation of distributed logic. As part of this research my team will also work to integrate this new knowledge into robust open source tools. These tools can then be used by industry practitioners to develop reliable and maintainable distributed systems more rapidly.

云计算彻底改变了计算。大大小小的企业都在利用大规模数据中心的灵活性和容量来构建其基础设施。然而，众所周知，在云中运行的系统设计起来非常复杂，因为这些系统旨在通过在多台机器上执行来进行扩展。例如，给定不同主机上的两个事件，即使每个事件都有时间戳，但其中一个事件是否因果依赖于另一个事件并不明显。基于云的系统中的错误可能很微妙，也可能是灾难性的。例如，2017 年，亚马逊 S3 存储系统的一个错误给依赖亚马逊 AWS 云服务的公司造成了 1.5 亿美元的损失。此类事件越来越普遍。 如今构建基于云的系统的工程师依靠测试来获得保证。不幸的是，通过测试获得合理的分布式行为覆盖是一个既定的挑战，而编写测试是乏味的、容易出错的，而且从根本上来说是不完整的。用于实现分布式系统正确性的最先进技术很少在实践中使用，因为它们不适用于实际的大规模系统，或者因为它们需要大量的努力和专业知识。 人们对分布式系统的建模语言越来越感兴趣，这些语言可以进行详尽的检查或证明满足某些属性。然而，如今，开发人员必须手动将其系统的正式模型转换为实现。此过程需要大量工作，并且可能会在实施中引入错误。这就是为什么开发人员很少对其系统进行建模，而是选择先构建然后再调试的原因之一。 在拟议的研究计划中，我将设计和实现技术，以将用高级建模语言编写的分布式系统的正式模型编译为可运行的实现。 作为我研究的一部分，我将创建一个工具链，该工具链将翻转用于基于云的系统的主要软件工程流程：开发人员将能够首先创建他们可以验证的正式模型，然后将这些模型编译为代码。通过免费导出可运行且等效的实现，开发人员将更有动力创建和管理其系统的正式模型。这项研究的长期目标是激励开发人员在设计/实现工作的早期使用正式方法，以减少进入生产系统的错误数量。 这项研究将产生关于分布式系统建模和分布式逻辑编译的新科学知识。作为这项研究的一部分，我的团队还将努力将这些新知识整合到强大的开源工具中。然后，行业从业者可以使用这些工具更快地开发可靠且可维护的分布式系统。