Compiling Distributed System Models into Implementations

点击翻译按钮获取中文摘要

Cloud computing has revolutionized computing. Enterprises, large and small, are taking advantage of the flexibility and capacity of massive data centers for their infrastructure. However, systems that run in the cloud are notoriously complex to engineer because these systems are designed to scale by executing across many machines. For example, given two events at different hosts, it is not obvious whether one of the events is causally dependent on the other, even if each event has a timestamp. Bugs in cloud-based systems can be subtle and catastrophic. 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 cloud services. Such incidents are increasingly common. Engineers who build cloud-based systems today rely on testing to gain assurance. Unfortunately, attaining reasonable distributed behavior coverage with testing is an established challenge while writing tests is tedious, error-prone, and fundamentally incomplete. State-of-the-art techniques for achieving distributed system correctness are rarely used in practice because they do not work on actual large-scale systems or because they require substantial effort and expertise. There is a growing interest in modeling languages for distributed systems, which can be checked exhaustively or proved to satisfy certain properties. However, today, the developer must manually translate a formal model of their system into an implementation. This process requires intensive effort and may introduce bugs into the implementation. This is one reason why developers rarely model their systems, electing instead to build first and debug later. In the proposed research program I will design and implement techniques to compile formal models of distributed systems, written in a high-level modeling language, into runnable implementations. As part of my research I will create a toolchain that will flip the dominant software engineering process used for cloud-based systems: developers will be able to first create formal models that they can verify, and then later compile these models into code. By deriving a runnable and equivalent implementation for free, developers will be more incentivized to create and curate formal models of their systems. The long-term goal of this research is to incentivize developers to use formal methods earlier in the design/implementation effort to decrease the number of bugs that make it into production systems. This research will generate new scientific knowledge about the modeling of distributed systems and compilation of distributed logic. As part of this research my team will also work to integrate this new knowledge into robust open source tools. These tools can then be used by industry practitioners to develop reliable and maintainable distributed systems more rapidly.