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

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

在最近的ACM操作系统原理研讨会（SOSP）上，某中心云服务团队凭借使用自动化推理验证ShardStore（新型S3存储节点微服务）功能正确性的工作获得最佳论文奖。某中心简单存储服务（S3）是基础对象存储服务，具有快速、廉价和可靠的特点。ShardStore是在存储硬件上运行的服务，负责持久存储S3对象数据，是对S3最底层数据存储和访问方式的彻底重新设计。

由于ShardStore对S3可靠性至关重要，确保其无错误极为重要。形式化验证涉及对软件重要属性进行数学规范定义，并正式证明系统永不违反这些规范，即通过数学方法证明不存在错误。自动化推理是一种自动寻找这些证明的方法。

轻量级验证方法

传统形式化验证需要付出高达系统构建10倍的工作量，对于S3这样庞大的系统并不实用。针对ShardStore，团队开发了新的轻量级自动化推理方法，在获得传统形式化证明几乎全部益处的同时大幅降低开销。

该方法在ShardStore代码中发现16个错误，这些错误若通过传统测试方法发现将极为耗时费力。使用该方法时，待验证软件规范的编写仅使ShardStore代码库增加约14%，而其他形式化验证方法通常需要增加2-10倍。

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

参考模型方法

该方法的核心概念之一是参考模型，即程序组件的简化实例，可用于跟踪不同输入条件下的程序状态。

例如，存储系统常使用日志结构合并树（LSMT），这是一种复杂数据结构，设计用于在内存和不同存储层级间分配数据，其数据传输协议充分利用不同存储介质特性以最大化效率。然而LSMT的状态（数据位置和数据访问模式记录）可使用简单哈希表建模，因此哈希表可作为该树的参考模型。

在此方法中，参考模型使用可执行代码指定。代码验证即确保代码实例化的组件状态与参考模型状态在任意输入下匹配。实践中发现，指定参考模型平均仅需实际组件实现代码量的约1%。

依赖跟踪技术

ShardStore使用LSMT跟踪和更新数据位置。每个存储对象被划分为数据块，数据块被写入区段（磁盘上的连续物理存储区域）。典型磁盘包含数万个区段，每个区段内的写入操作是顺序的，由定义下一个有效写入位置的写入指针跟踪。

该模型的简单性使数据写入非常高效，但也意味着区段内的数据块无法单独删除。从区段删除数据块需要将区段内所有其他数据块转移到别处，然后将写入指针移回区段起始位置。

使用ShardStore写入单个数据块所需的过程序列（更新合并树、写入数据块、递增写入指针等）在连续写入操作间创建了依赖关系集。例如，区段内写入指针的位置取决于该区段内最后执行的写入操作。

该方法要求跟踪连续操作间的依赖关系，通过动态构建依赖图实现。ShardStore使用依赖图决定如何最高效地将数据写入磁盘，同时在崩溃恢复时保持一致性。使用形式化验证检查系统是否始终正确构建这些图，从而始终保持一致性。

测试流程优化

论文描述了该方法支持的各种测试，包括崩溃一致性测试、并发执行测试以及序列化器测试（将数据结构的单独元素映射到内存或存储中的连续位置）。

还介绍了一些确保验证彻底性的优化措施。例如，该方法生成随机输入序列以测试规范违反情况。如果检测到违反，系统会系统性地缩减输入序列以识别导致错误的具体输入。

还偏置随机输入选择器，使其选择针对相同存储路径的输入，以最大化错误检测可能性。例如，如果每个输入读取或写入不同对象，就不存在遇到数据不一致的风险。

生产环境应用

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