Improving the Construction of Correct Distributed Systems

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

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