Improving the Construction of Correct Distributed Systems

改进正确的分布式系统的构建

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

Enterprises, large and small, are taking advantage of the flexibility and capacity of massive data centers (the cloud) for their infrastructure. Data centers, however, depends critically on the correct function of many complex distributed systems to realize scalable and fault-tolerant services. Unfortunately, these systems are notoriously difficult to engineer and bugs may be subtle and have catastrophic consequences. 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 services.******My research program will improve how engineers construct distributed systems, helping to debug existing systems and to design more correct future systems.I will accomplish this by devising new formal methods techniques and new tools that work on real systems, find more bugs, and are easier to use than existing approaches. My program focus has two strands:******Hybrid model checking of existing distributed systems. To help developers find bugs in existing systems I will develop techniques to combine the speed of abstract model checkers with the correctness and ease-of-use of concrete model checkers to build a hybrid model checker. My approach will use a concrete model checker to generate logs from real executions of the system. These logs will be used to construct an abstract model of the system that can be checked using an abstract model checker. Property violations, or bugs, will be verified using new distributed trace replay techniques. In concert these techniques will check more of the distributed system state space and find bugs faster.******Compiling distributed systems from specifications. To help developers construct correct new systems I will develop a compiler that translates a verified specification into a fully functioning implementation. This compiler will automate today's manual translation process, which may introduce errors and also requires substantial time and effort. This will encouraging designers to write more formal specifications for their systems. The compiler will also preserving the semantics of the specification and thereby the correctness properties. This will increase developers' confidence in the correctness of their system implementations.******The above two approaches will generate several kinds of new scientific knowledge bout the modeling of distributed systems, compilation of distributed logic, distributed state space reduction and exploration heuristics, and instrumentation and replay of distributed executions. My team and I will work to integrate this new knowledge into robust open source tools. These tools can then be used by industry practitioners to improve the correctness of existing and future distributed systems.**

大大小小的企业都在利用大规模数据中心（云）的灵活性和容量来构建其基础设施。然而，数据中心关键依赖于许多复杂分布式系统的正确功能来实现可扩展和容错的服务。不幸的是，这些系统非常难以设计，而且错误可能很微妙，并会产生灾难性的后果。例如，2017 年，亚马逊 S3 存储系统中的一个错误给依赖亚马逊 AWS 服务的公司造成了 1.5 亿美元的损失。******我的研究计划将改进工程师构建分布式系统的方式，帮助调试现有的分布式系统系统并设计更正确的未来系统。我将通过设计新的形式化方法技术和新工具来实现这一目标，这些技术和新工具可在真实系统上工作，发现更多错误，并且比现有方法更易于使用。我的程序重点有两个方面：******现有分布式系统的混合模型检查。为了帮助开发人员发现现有系统中的错误，我将开发一些技术，将抽象模型检查器的速度与具体模型检查器的正确性和易用性相结合，以构建混合模型检查器。我的方法将使用具体模型检查器从系统的实际执行中生成日志。这些日志将用于构建系统的抽象模型，可以使用抽象模型检查器进行检查。将使用新的分布式跟踪重放技术来验证属性违规或错误。这些技术将共同检查更多的分布式系统状态空间并更快地发现错误。******根据规范编译分布式系统。为了帮助开发人员构建正确的新系统，我将开发一个编译器，将经过验证的规范转换为功能齐全的实现。该编译器将使当今的手动翻译过程自动化，这可能会引入错误，并且还需要大量的时间和精力。这将鼓励设计人员为其系统编写更正式的规范。编译器还将保留规范的语义，从而保留正确性属性。这将增加开发人员对其系统实现的正确性的信心。******以上两种方法将产生几种关于分布式系统建模、分布式逻辑编译、分布式状态空间缩减和探索的新科学知识分布式执行的启发式、检测和重放。我和我的团队将努力将这些新知识整合到强大的开源工具中。然后，行业从业者可以使用这些工具来提高现有和未来分布式系统的正确性。**