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.