Rust中分布式程序的精炼方法论

《Proceedings of the ACM on Programming Languages》：A Refinement Methodology for Distributed Programs in Rust

本文提出一种新型底向上细化方法，结合 guarded transition systems 和 locally inductive invariants 实现抽象模型与具体代码的灵活关联，突破传统耦合不变式限制，支持多种程序结构和证明方法，并通过Rust类型系统管理守卫所有权，成功应用于并发Memcached等实际案例。

　　

摘要

精细化（Refinement）是将一个抽象的系统模型转化为一个具体的、可执行的程序，使得为抽象模型定义的属性能够直接应用于具体实现中。这种方法在开发经过验证的大型系统中取得了成功。然而，现有的精细化技术存在一些局限性，这些局限性限制了它们的实际应用价值。自顶向下的精细化技术虽然能够自动生成可执行代码，但生成的实现通常性能不佳；而自底向上的精细化技术虽然可以对现有的高效实现进行推理，但对代码结构、精细化证明的结构以及所使用的验证逻辑和工具有着严格的要求。

在本文中，我们提出了一种新的自底向上精细化方法，旨在克服这些局限性。该方法利用了“受保护转换系统”（guarded transition systems）这一熟悉的概念来表达抽象模型，并将“保护机制”（guards）与“局部归纳不变量”（locally inductive invariants）这一创新概念相结合，从而将抽象模型“局部”地映射到具体状态上。与传统的耦合不变量（coupling invariants）相比，这种方法具有更高的灵活性，能够支持多种程序结构、数据表示形式和证明结构。我们将该方法集成到了Rust编程语言中，并利用Rust的类型系统来处理保护机制的所有权问题。这种集成使得我们的方法可以与现有的Rust验证工具一起使用，同时也便于实际应用。我们通过多个案例研究验证了该方法的有效性，其中包括一个并发实现的Memcached系统。