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亿美元的损失。我的研究计划将改善工程师如何构建分布式系统，帮助调试现有的系统，并设计更正确的未来系统。我将通过设计新的形式化方法技术和新的工具，工作在真实的系统，发现更多的错误，比现有的方法更容易使用。我的程序重点有两个方面：* 现有分布式系统的混合模型检查。为了帮助开发人员发现现有系统中的错误，我将开发技术，将抽象模型检查器的速度与具体模型检查器的正确性和易用性相结合，以构建混合模型检查器。我的方法将使用具体的模型检查器从系统的真实的执行中生成日志。这些日志将用于构建系统的抽象模型，可以使用抽象模型检查器进行检查。将使用新的分布式跟踪重放技术来验证属性违规或错误。这些技术将检查更多的分布式系统状态空间，并更快地找到bug。从规范编译分布式系统。为了帮助开发人员构建正确的新系统，我将开发一个编译器，将经过验证的规范转换为功能齐全的实现。该编译器将自动化当今的手动翻译过程，这可能会引入错误，并且还需要大量的时间和精力。这将鼓励设计人员为他们的系统编写更正式的规范。编译器还将保留规范的语义，从而保留正确性属性。这将增加开发人员对系统实现正确性的信心。**这两种方法将在分布式系统建模、分布式逻辑编译、分布式状态空间约简和探索算法、分布式执行的插装和重放等方面产生新的科学知识。我和我的团队将努力将这些新知识整合到强大的开源工具中。这些工具可以被行业从业者用来提高现有和未来分布式系统的正确性。