Executing Microservice Applications on Serverless, Correctly
Executing Microservice Applications on Serverless, Correctly
复制标题
DOI：
10.1145/3571206
复制
发表时间：
2023-01
影响因子：
--
通讯作者：
Konstantinos Kallas;Haoran Zhang;R. Alur;Sebastian Angel;Vincent Liu
中科院分区：
文献类型：
--
作者：
Konstantinos Kallas;Haoran Zhang;R. Alur;Sebastian Angel;Vincent Liu
虽然无服务器平台大大简化了云应用程序的配置，配置和管理，但在这些平台上实现正确的服务可能会给程序员带来重大挑战。例如，无服务器基础设施引入了许多传统部署中不存在的故障模式。个别无服务器实例可能会失败，而其他实例则继续取得进展，云提供商可以将正确但缓慢的实例作为资源管理的一部分杀死，并且提供商通常会通过重新执行请求来响应此类失败。对于具有副作用的函数，这些方案可能会创建在服务器部署中不可观察的行为。在本文中，我们提出了mu 2sls，这是一个使用标准Python代码在无服务器上实现微服务应用程序的框架，其中包含两个额外的原语：事务和异步调用。我们的框架编排用户编写的服务，以解决几个挑战，如故障和重新执行，并提供正式的保证，生成的无服务器实现是正确的。为此，我们提出了一种新的服务规范抽象和形式化的无服务器实现，便于推理的正确性，一个给定的应用程序的无服务器实现。这种形式化形成了mu 2sls原型的基础，然后我们使用它来开发一些真实世界的微服务应用程序，并表明生成的无服务器实现的性能实现了显著的可扩展性（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.