一句话：提出 mu2sls 框架，以事务和异步调用原语在 Serverless 上正确执行 Python 微服务并提供形式化保证。
在 Serverless 上实现正确的微服务面临实例失败、慢实例被终止和请求重执行等故障模式，这些与副作用结合会产生传统部署中不可观测的行为。本文提出 mu2sls 框架，允许用带事务和异步调用两个原语的标准 Python 代码实现微服务，并自动编排以处理故障与重执行。作者给出服务规约抽象和 Serverless 实现的形式化，以推理正确性，并构建原型。用真实微服务应用评估，生成的 Serverless 实现在保证故障、重执行和并发下正确性的同时，吞吐量达到顺序实现的 3-5 倍，具有显著可扩展性。
While serverless platforms substantially simplify the provisioning, configuration, and management of cloud applications, implementing correct services on top of these platforms can present significant challenges to programmers. For example, serverless infrastructures introduce a host of failure modes that are not present in traditional deployments. Individual serverless instances can fail while others continue to make progress, correct but slow instances can be killed by the cloud provider as part of resource management, and providers will often respond to such failures by re-executing requests. For functions with side-effects, these scenarios can create behaviors that are not observable in serverful deployments. In this paper, we propose mu2sls, a framework for implementing microservice applications on serverless using standard Python code with two extra primitives: transactions and asynchronous calls. Our framework orchestrates user-written services to address several challenges, such as failures and re-executions, and provides formal guarantees that the generated serverless implementations are correct. To that end, we present a novel service specification abstraction and formalization of serverless implementations that facilitate reasoning about the correctness of a given application’s serverless implementation. This formalization forms the basis of the mu2sls prototype, which we then use to develop a few real-world microservice applications and show that the performance of the generated serverless implementations achieves significant scalability (3-5× the throughput of a sequential implementation) while providing correctness guarantees in the context of faults, re-execution, and concurrency.
@article{paperbot2099,
title = {Executing Microservice Applications on Serverless, Correctly},
author = {Konstantinos Kallas and Haoran Zhang and Rajeev Alur and Sebastian Angel and Vincent Liu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571206}
}