paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Consistent Updates for Scalable Microservices

可扩展微服务的一致性更新
POPL 10(POPL)2026匹配度 1/10 · 该论文研究微服务混合模式更新的一致性形式化框架与算法,属于分布式系统与形式语义方向;与用户关注的 PL/AI 交叉、静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析均无直接关系。引用 1 inbox
Devora Chait-Roth, Kedar S. Namjoshi, Thomas Wies
crossref: 2026-09-10

AI 速览

一句话:提出微服务混合模式更新的形式化框架与保证一致性的算法,并证明忽略语义的方法必然导致不一致。

在线服务通常以可扩展微服务架构实现,同构 worker 处理客户端请求并将持久状态写入后端数据存储。服务功能需要在线更新而不中断请求处理,但其核心困难在于:新旧版本的 worker 通过数据存储交互会产生混合模式行为,从而引发不一致。已有的规避混合模式的方法要么资源翻倍、要么吞吐减半,代价高昂;不受控的滚动更新则可能导致严重服务失败。理想情况下,更新应对每个客户端表现为原子生效。本文提出一个形式化框架来刻画这一直觉,并建立用于推理更新一致性的基础理论。基于该理论,作者首次给出保证混合模式更新一致性的算法,其依赖服务动作的语义性质(如交换性);同时证明任何语义无关的混合模式更新方法都必然允许不一致,说明这种语义依赖不可避免。

问题
微服务在线更新时,新旧版本 worker 通过共享数据存储交互产生混合模式行为,导致状态不一致;规避混合模式代价高,滚动更新又有严重失败风险。
方法
提出形式化框架刻画更新对客户端原子生效的直觉,建立更新一致性推理的基础理论,并基于服务动作的语义性质(如交换性)设计保证一致性的混合模式更新算法。
评估
以理论证明方式评估:给出的算法保证混合模式更新的一致性,并证明任何语义无关的混合模式更新方法必然允许不一致(不可能性结论)。
原文摘要(Abstract)

Online services are commonly implemented with a scalable microservice architecture, where isomorphic workers process client requests, recording persistent state in a backend data store. To maintain service, modifications to service functionality must be made on the fly - i.e., as the service continues to process client requests - but doing so is challenging. The central difficulty is that of avoiding inconsistencies from mixed-mode operation, caused by workers of current and new versions interacting via the data store. Some update methods avoid mixed-mode altogether, but only at the cost of substantial inefficiency - by doubling resources (memory and compute), or by halving throughput. The alternative is an uncontrolled “rolling” update, which runs the risk of serious service failures arising from inconsistent mixed-mode behavior. Ideally, it should appear to every client that a service update takes effect atomically; this ensures that a client is not exposed to inconsistent mixed-mode behavior. In this paper, we introduce a framework that formalizes this intuition and develop foundational theory for reasoning about update consistency. We apply this theory to derive the first algorithms that guarantee consistency for mixed-mode updates. The algorithms rely on semantic properties of service actions, such as commutativity. We show that this is unavoidable, by proving that any semantically oblivious mixed-mode update method must allow inconsistencies.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{ChaitRothNW26,
  title = {Consistent Updates for Scalable Microservices},
  author = {Devora Chait-Roth and Kedar S. Namjoshi and Thomas Wies},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {POPL},
  year = {2026},
  doi = {10.1145/3776700}
}