摘要：分布式共识与一致性协议难以分析，却又是云服务的基础；因此，在部署之前通常会经过严格的证明与形式化验证。然而，这种严谨性却很少被应用于协议的修改上——而协议修改在生产环境中频繁发生，极易危及系统安全性。本文通过提出一种面向分布式协议的自动优化器——DistOptimize，有效消除了人为修改带来的安全风险。DistOptimize将学术界语言中的吞吐量优化技术移植到生产环境所使用的框架中，并在Rocq语言中验证重写后的正确性，同时借助校准与基于整数线性规划（ILP）的搜索空间导航机制，实现优化结果的自动化应用。经测试，该方法应用于基础分布式协议以及AWS实际使用的协议时，可使吞吐量提升高达4倍，且延迟增加不超过0.3毫秒。
主题：| 分布式、并行与集群计算（cs.DC）；数据库（cs.DB） 引用格式：| arXiv:2610.39017 [cs.DC] | （或
arXiv:2610.39017v1 [cs.DC] 本版本） | https://doi.org/10.48550/arXiv.2610.39017
点击了解更多信息
由 DataCite 提供的 arXiv 发布 DOI
提交历史
访问论文：
查看PDF
HTML（实验性）
TeX源代码
附加功能
音频摘要
当前浏览上下文：
参考文献与引用
Google 学术搜索
Semantic Scholar
书签
机构
arXivLabs 是一个框架，允许合作者直接在我们的网站上开发并共享新的 arXiv 功能。
无论是个人还是与 arXivLabs 合作的组织，都已认同并践行我们所倡导的开放、社区、卓越以及用户数据隐私等价值观。arXiv 致力于这些价值理念，并且只与同样秉持这些理念的合作伙伴开展合作。
您是否有一个能为 arXiv 社区创造价值的项目构想？欢迎了解更多关于 arXivLabs 的信息。