CAREER: Principles and Practice of Distributed Updates

许多系统必须定期更新以添加功能、修复错误、修补安全漏洞并消除性能瓶颈。 在某些系统中，更新可以通过简单地停止程序，更新代码和数据，并重新启动新版本来应用，但在关键系统中，即使是短暂的维护中断也是不可接受的。 尽管研究界已经开发出了动态更新程序的技术，但现有的框架只能处理一台机器。为了更新运行在分布式系统上的软件，程序员通常使用ad hoc技术，这些技术很难推理并且容易出错。本项目的目标是开发管理分布式更新的基本原则和实用技术。 一个中心主题是使用双向转换来弥合程序不同版本之间的差距，从而允许多个版本无缝地互操作。 具体的贡献包括开发（一）分布式更新的正式基础，（二）编程抽象的构建和部署更新，（三）自动检查更新的正确性属性的验证工具，以及（四）这些抽象和工具的实际例子的评估。该项目将产生广泛的影响，（i）发现在更新过程中提高分布式系统可靠性的技术，（ii）建立可重用的软件基础设施来管理更新，以及（iii）通过高中外展计划改善K-12教育并增加代表性不足的少数民族在科学中的参与。

Many systems must be periodically updated to add features, fix bugs, patch security vulnerabilities, and eliminate performance bottlenecks. In some systems, updates can be applied by simply halting the program, updating the code and data, and restarting the new version, but in critical systems even brief interruptions for maintenance are unacceptable. Although the research community has developed techniques for updating programs on the fly, existing frameworks only handle a single machine. To update the software running on a distributed system, programmers typically use ad hoc techniques that are difficult to reason about and prone to error.The goal of this project is to develop foundational principles and practical techniques for managing distributed updates. A central theme is the use of bidirectional transformations to bridge the gap between different versions of a program, thereby allowing multiple versions to interoperate seamlessly. Specific contributions include developing (i) formal foundations for distributed updates, (ii) programming abstractions for constructing and deploying updates, (iii) verification tools for checking update correctness properties automatically, and (iv) an evaluation of these abstractions and tools on practical examples. The project will have broad impact by (i) discovering techniques for increasing the reliability of distributed systems during updates, (ii) building reusable software infrastructure for managing updates, and (iii) improving K-12 education and increasing the participation of underrepresented minorities in science through a high school outreach program.