某中心团队因自动化推理研究荣获最佳论文奖

SOSP论文描述了用于验证新型S3数据存储服务的轻量级形式化方法

会议：SOSP 2021
相关出版物：《使用轻量级形式化方法验证某中心S3中的键值存储节点》

在近期举行的ACM操作系统原理研讨会（SOSP）上，某中心云服务团队凭借采用自动化推理技术验证ShardStore——新型S3存储节点微服务——功能正确性的研究成果获得最佳论文奖。某中心简单存储服务（S3）是核心对象存储服务，具备高速、低成本和高可靠性特点。ShardStore运行在存储硬件上，负责持久化存储S3对象数据，是对底层数据存储与访问方式的彻底重构。

由于ShardStore对S3可靠性至关重要，必须确保其不存在缺陷。形式化验证通过数学方式定义软件关键属性，并严格证明系统永不违反这些规范，即数学层面证明无缺陷。自动化推理则是自动寻找这些证明的方法。

轻量级验证突破

传统形式化验证需要付出相当于系统开发10倍的工作量，对于S3这样的大型系统并不实用。针对ShardStore，团队开发了新型轻量级自动化推理方法，在保持传统形式化证明优势的同时显著降低开销。该方法发现ShardStore代码中16个潜在缺陷，这些缺陷通过传统测试方法难以发现且耗时费力。采用该方法后，待验证软件规范的代码增量仅约14%，远低于其他形式化验证方法2-10倍的增量。

该方法允许使用与代码相同的语言（本文为Rust）编写规范，使开发人员在扩展功能时能自主编写新规范。初期由形式化验证专家编写ShardStore规范，随着项目推进，软件工程师已逐步接管该职责，目前18%的规范由开发人员编写。

参考模型与依赖追踪

该方法的核心概念是参考模型——程序组件的简化实例，可用于跟踪不同输入条件下的程序状态。例如存储系统常用的日志结构合并树（LSMT），其状态可通过简单哈希表建模，使哈希表成为树的参考模型。实践中发现，指定参考模型平均仅需实际组件实现1%的代码量。

ShardStore使用LSMT跟踪和更新数据位置。每个存储对象被分为数据块，写入磁盘的连续存储区域（extent）。每个磁盘包含数万个extent，写入操作通过写指针跟踪下一有效写入位置。该模型使数据写入高效，但意味着无法单独删除extent中的数据块，删除操作需要转移该extent中所有其他数据块并将写指针重置到起始位置。

通过ShardStore写入单数据块所需的操作序列（更新合并树、写入数据块、递增写指针等）在连续写入操作间创建依赖关系。该方法要求跟踪跨操作依赖，通过实时构建依赖图实现。ShardStore使用依赖图决定如何最高效写入数据，同时在崩溃恢复时保持一致性。形式化验证用于检查系统是否始终正确构建这些依赖图并保持一致性。

测试流程与优化

论文描述了该方法支持的多种测试，包括并发执行测试和序列化器测试（将数据结构元素映射到内存或存储的连续位置）。为确保验证全面性，团队实施了多项优化：生成随机输入序列检测规范违反情况，发现违反时系统化精简输入序列定位具体错误输入；偏置随机输入选择器使其针对相同存储路径，最大化错误检测概率。

采用轻量级自动化推理技术验证每个ShardStore部署。任何变更进入生产环境前，通过某中心批处理服务在数亿个场景中检查其行为。为支持可扩展检查，团队开发并开源新型Rust代码模型检查器Shuttle，用于验证ShardStore的并发属性。这些方法共同为S3最关键微服务提供持续自动化正确性保障。