类型a：单一原创研究
研究作者与发表信息
本研究的作者包括来自Mozilla和MPI-SWS（马克斯·普朗克软件系统研究所）的Ralf Jung，来自MPI-SWS的Hoang-Hai Dang，来自KAIST（韩国科学技术院）的Jeehoon Kang，以及同样来自MPI-SWS的Derek Dreyer。该论文发表于《Proceedings of the ACM on Programming Languages》第4卷POPL（Principles of Programming Languages）会议论文集，文章编号41，于2020年1月正式发表。论文标题为“Stacked Borrows: An Aliasing Model for Rust”（堆叠借用：Rust的别名模型）。
学术背景与研究动机
本研究属于编程语言理论与程序分析领域，具体聚焦于操作语义（operational semantics）与别名分析（alias analysis）。Rust语言的核心优势之一在于其类型系统对指针别名施加了严格的纪律约束：可变引用（&mut T）在作用域内是唯一的，不能与其他指针别名；共享引用（&T）允许别名但禁止通过其进行可变修改。这一静态别名信息使编译器能够进行程序优化，例如在不了解函数内部实现的情况下，安全地重排内存访问顺序、消除冗余读写等。然而，Rust同时支持不安全代码（unsafe code），程序员可以通过将引用转换为裸指针（raw pointer）等方式绕过类型系统的检查，制造别名并破坏上述优化假设。这一矛盾构成了Rust编译器优化的核心困难。
本研究要解决的核心问题是：如何在允许编译器利用别名信息进行激进优化的同时，为不安全代码作者提供一套清晰的规则，使其能够确信只要遵循这些规则，编译器的优化就不会改变程序的可观察行为。为此，作者提出了Stacked Borrows（堆叠借用）这一操作语义模型，它定义了一种动态的别名纪律，违反该纪律的程序将被判定为未定义行为（undefined behavior）。该模型的目标是既为编译器提供足够的优化空间，又不至于过多地排斥真实世界中合法使用的不安全代码。
详细工作流程与研究设计
本研究的工作流程可以划分为四个主要阶段，以逐步构建并验证Stacked Borrows模型。
第一阶段：为简化语言建立基础模型。 作者首先考虑仅包含可变引用和裸指针的Rust语言片段。核心思想是将借用检查器（borrow checker）的静态规则动态化，但避免使用生命周期（lifetime）。具体来说，每个内存位置（location）维护一个借用栈（borrow stack），栈中存放标记（tag）对应的项目（item）。当创建新的可变引用时，为其分配一个全新的唯一标记，并将该标记推入借用栈顶部。当使用某个指针进行读写时，要求对应该指针标记的项目必须存在于栈中，并且使用过程中需要将位于其上方的项目弹出（pop），从而使该标记项目到达栈顶。如果标记不在栈中，则程序被判定为未定义行为。这一机制强制实现了引用的嵌套使用模式，违反了这种嵌套（如xyxy模式）的程序会被拒绝。对于裸指针，模型引入一个特殊标记⊥表示未标记（untagged），并在借用栈中使用sharedrw项目来表示该位置可被所有裸指针自由读写。当从可变引用创建裸指针时，新的sharedrw被推入栈顶。这保证了裸指针之间的任意交错访问是被允许的，然而只要其中涉及可变引用，栈纪律的违反仍会导致未定义行为。
第二阶段：引入重标记（retagging）与保护器（protectors）。 由于不安全代码可以通过transmute_copy等方式复制可变引用，造成相同标记的引用出现，从而使标记的唯一性假设失效。为解决此问题，模型引入了retag操作。在函数入口处，所有引用类型的参数都会被自动retag（retag x等价于x = &mut *x），使进入函数的引用获得全新的唯一标记。这使编译器可以在函数内部安全地基于该引用的独特性进行优化。此外，为了支持将内存访问向下移动（即跨越未知函数调用延迟读写），作者引入了保护器（protector）机制。在函数入口的retag[fn]操作中，新推入栈的项目会被赋予当前函数调用标识（call id）作为保护器。如果某个受保护的项目在所属函数调用尚未返回时被弹出，则程序为未定义行为。这一机制反映了Rust中“引用必须超出函数调用”的生命周期约束，从而排除了那些在函数调用期间通过别名指针修改被引用内存的对抗性程序。
第三阶段：扩展至共享引用与内部可变性。 对共享引用，模型引入了sharedro(t)项目，表示带标记t的共享引用仅可读不可写。读取操作read-1的行为与写入不同：读取时不要求目标项目最终位于栈顶，只要求目标项目上方没有非sharedro项目。这样多个共享引用可以交错读取而不会互相弹出。若通过transmute等方式将共享引用转为裸指针并尝试写入，则因栈中没有对应的unique或sharedrw项目而触发未定义行为。然而，Rust的UnsafeCell类型提供了内部可变性（interior mutability），允许通过共享引用进行受控的可变操作。例如&Cell<i32>或&RefCell<i32>可在别名情况下安全地修改数据。为此，模型规定：创建共享引用时，对于引用所覆盖的内存中位于UnsafeCell内部的那些位置，推入sharedrw(t)项目而非sharedro(t)，从而允许这些位置的可变别名访问。同时，创建指向UnsafeCell内部的共享引用或从引用创建裸指针时不视为一次访问操作，而是将新项目插入到栈中对应标记项目的正上方，以维持可变引用唯一标记仍然位于栈顶的不变量。
第四阶段：形式化定义与实验评估。 作者在Coq证明助手中形式化了完整的Stacked Borrows操作语义，将其定义为一个带标签的状态转换系统。状态包括内存位置到借用栈的映射、当前活动调用列表、下一个指针标记和下一个调用标识。在验证方面，作者进行了双向评估：一方面，将Stacked Borrows实现于Miri（Rust的解释器）中，并使用该解释器运行Rust标准库中与操作系统无关的测试套件（包括libcore、liballoc和hashmap模块的测试），以检验模型是否足够宽松以容忍真实世界的不安全代码。测试结果发现少数违反该模型的代码，其中绝大多数被Rust开发者确认为标准库中的缺陷并随后修复，其余大部分测试无需修改即可通过。另一方面，作者给出了若干代表性编译器变换的证明草图（由Coq中的机械化证明支持），包括example1中跨未知代码移动读操作、example2中在共享引用上移动读操作、以及example3_down中跨函数调用移动写操作等变换的合法性证明，证明这些优化在Stacked Borrows语义下是可靠且正确的。
主要结果与逻辑分析
实验的第一项关键结果来自于形式化证明的成功完成。通过对example1（可变引用）的证明，作者展示了经过retag之后，引用x的标记位于借用栈顶部；在x的两次使用之间，任何其他指针若访问同一位置，其标记必然位于x标记的下方，而访问操作会弹出位于其上方的所有项目（包括x的标记），从而使后续对x的使用失败且被判为未定义行为。由此证明了在遵守Stacked Borrows的前提下，程序不可能在x的写操作与之后的读操作之间通过其他别名修改该位置的值，于是优化器可以安全地将读取替换为常量42或在时间上重排。类似地，对example2（共享引用）的证明表明，共享引用经过retag后其sharedro(t)位于栈顶，在函数调用期间如有任何写操作将弹出所有sharedro并导致违反，因此可以安全地将读操作跨越函数调用向下移动。对于example3_down（写操作向下移动）的证明则显示了保护器的关键作用：带有活动保护器的项目不能被弹出，因此未知函数无法在原始程序位置观察到旧值，优化器可以推迟写操作而不改变可观察行为。
实验的第二项结果来自于Miri解释器上的标准库测试。测试套件覆盖了Rust标准库中大量使用不安全代码的核心数据结构，如Vec、HashMap等。大规模测试通过表明Stacked Borrows模型的设计与Rust生态系统中实际惯用的不安全代码模式高度兼容。少数暴露出的标准库违规实例不仅未否定模型，反而印证了该模型能够有效捕获真实的别名纪律缺陷，对改善Rust标准库的实现质量产生了实际影响。这些结果共同支撑起论文的核心结论：Stacked Borrows成功地在支持编译器优化与容纳真实不安全代码之间取得了平衡。
结论与学术应用价值
本研究的结论是：Stacked Borrows操作语义为Rust语言提供了一套可形式化验证的别名模型，既为编译器提供了足够的别名信息以进行激进但安全的程序变换，又为不安全代码作者提供了清晰且稳定的行为规则。其科学价值在于：它首次为像Rust这样的系统编程语言建立了一个可机器验证的、与借用检查器静态规则相呼应的动态别名模型，解决了该领域长期存在的优化安全性与不安全代码灵活性之间的张力。从应用价值看，该模型已在Miri解释器中被实现并验证了大量标准库测试，它不仅有助于发现标准库中的实际缺陷，还为Rust编译器的优化策略提供了可靠的形式化基础。更重要的是，Stacked Borrows不依赖生命周期推理的具体细节，使不安全代码的正确性不再随编译器生命期推断算法的变化而漂移，为未来Rust别名模型的演进提供了稳定的基石。
研究亮点
本研究的首要亮点是将Rust借用检查器的静态栈式纪律转化为动态借用栈模型，并通过retag与protector机制使该模型在不依赖生命周期信息的前提下支撑多种程序变换的重排证明。第二个亮点是模型对裸指针与UnsafeCell内部可变性的精细处理，尤其是sharedrw项目的引入与“不在栈顶、而在标记正上方插入”的非栈式操作，为解决内部可变性与别名优化的冲突提供了巧妙且实用的方案。第三个亮点是read-2规则中“禁用（disabled）”项目的引入，它允许在读取时禁用上方唯一的唯一项目而不弹出其间的sharedrw项目，从而在保持优化能力的同时避免了无辜的裸指针失效。最后，模型在Coq中完成了完整的形式化，并以实际标准库测试为实证基础，体现了理论深度与工程实用性的高度统一。