Improving the Construction of Correct Distributed Systems

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

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.**