FMitF: Track I: Automatic Migration to Serverless Infrastructure, Correctly and Efficiently

无服务器计算有望彻底改变许多云服务中的计算结构，这些服务为现代世界提供了动力。不幸的是，虽然无服务器架构的操作和成本优势使其成为当今面向服务器部署的一个有吸引力的替代方案，但对于拥有现有服务的用户来说，由于架构之间的一些基本差异，迁移到新的范式可能具有挑战性。该项目的新颖之处在于探索从更传统的应用程序体系结构到无服务器范式的自动迁移的需求、机会和限制。为了实现这些目标，研究人员为期望的迁移开发了一个正式的正确性概念，并在传统微服务词汇表和无服务器基础设施词汇表之间进行了可证明的正确和系统的转换。然后，正确的翻译将被迭代优化，以创建更有效的实现。最后，将这些技术集成到实际的可部署系统中，并在实际代码和工作负载上对其进行评估。该项目的影响是使云服务的开发更简单、更高效。该项目在正式方法和分布式系统的交叉点上训练研究生，让本科生参与研究，并以公开可用的课程材料和开源软件工件的形式传播结果。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Serverless computing promises to revolutionize the computation is structured in many of the cloud services that power the modern world. Unfortunately, while the operational and cost benefits of serverless architectures make it an attractive alternative to today’s server-oriented deployment, for users with existing services, migrating to the new paradigm can be challenging due to some fundamental differences between the architectures. The project’s novelties are the exploration of the requirements, opportunities, and limitations of automatic migration from more traditional application architectures to the serverless paradigm. To meet these goals, the researchers develop a formal notion of correctness for the desired migration as well as a provably correct and methodical translation between the vocabulary of traditional microservices and that of serverless infrastructure. The correct translation will then be iteratively optimized to create successively more efficient implementations. Finally, these techniques are integrated into practical and deployable systems, which are evaluated on real code and workloads. The project’s impacts are to make the development of cloud services both simpler and more efficient. The project trains graduate students at the intersection of formal methods and distributed systems, engages undergraduate students in research, and disseminates results in the form of publicly available course materials and open-source software artifacts.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.