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亿美元的损失。****** ******我的研究计划将改善工程师如何构建分布式系统，帮助将现有系统调试并设计更正确的未来系统。I将通过在现实系统上使用新的正式方法和新的系统来实现这一目标，而不是现有的bugs，并且可以使用更多的bugs，并且可以使用更多的bugs，并且可以使用更轻松的bugs，并且可以使用更多的bugs，并且可以使用更容易地使用，并且可以使用bugs，并且可以使用更多的方法来实现。我的程序焦点有两个链：******混合模型检查现有分布式系统。为了帮助开发人员在现有系统中找到错误，我将开发技术，以将抽象模型检查器的速度与混凝土模型检查器的正确性和易用性相结合，以构建混合模型检查器。我的方法将使用混凝土模型检查器从系统的真实执行中生成日志。这些日志将用于构建系统的抽象模型，该模型可以使用抽象模型检查器检查。将使用新的分布式跟踪重播技术验证属性违规或错误。在协同过程中，这些技术将检查更多分布式系统状态空间，并更快地找到错误。******从规格中编译分布式系统。为了帮助开发人员构建正确的新系统，我将开发一个编译器，该编译器将经过验证的规范转换为功能齐全的实现。该编译器将自动化当今的手动翻译过程，这可能会引入错误，并且还需要大量时间和精力。这将鼓励设计师为其系统编写更多正式的规格。编译器还将保留规范的语义，从而保留正确性属性。这将增加开发人员对系统实施的正确性的信心。我和我的团队将努力将这些新知识集成到强大的开源工具中。然后，行业从业人员可以使用这些工具来提高现有和未来分布式系统的正确性。**