安全变得简单 第1部分：单一所有权（并非）可选

# 安全变得简单：第1部分——单一所有权（并非）可选 来源：https://ergeysay.github.io/safe-made-easy-pt1.html - 介绍 (https://ergeysay.github.io/safe-made-easy-pt1.html#intro) - 它所承诺的和未承诺的 (https://ergeysay.github.io/safe-made-easy-pt1.html#what-it-promises-and-what-it-doesnt) - 激励示例 (https://ergeysay.github.io/safe-made-easy-pt1.html#motivating-example) - 提案 (https://ergeysay.github.io/safe-made-easy-pt1.html#the-proposal) - 线性丢弃 (https://ergeysay.github.io/safe-made-easy-pt1.html#linear-drops) - 形式化背景 (https://ergeysay.github.io/safe-made-easy-pt1.html#the-formal-background) - 迄今为止的规则 (https://ergeysay.github.io/safe-made-easy-pt1.html#the-rules-so-far) - 结论 (https://ergeysay.github.io/safe-made-easy-pt1.html#conclusion) ## 介绍 本篇文章介绍了一种内存安全方法，我认为它比现有的替代方案更加实用且更符合人体工程学。这一切的起点很早以前，并且受到我所阅读和撰写的以下内容的启发： - 尝试将线性类型叠加到 Rust 之上 (1) (https://faultlore.com/blah/linear-rust/), (2) (https://blog.yoshuawuyts.com/linearity-and-control/) - 泄漏末日 (https://faultlore.com/blah/everyone-poops/) - Verdagon 关于 Vale 设计和高阶 RAII 的文章 (https://verdagon.dev/blog/higher-raii-uses-linear-types) - 大量的 TypeScript（真的很多） 经过三年的开发，我相信我终于搞定了。提案已经完成。此外，我已经在我自己的编程语言中实现了它，并计划在近期发布。我想分享设计决策以及从“嗯，为什么不试试”到“天啊，它已经活了”的整个历程。 所以，简而言之：线性类型（即只被丢弃一次）+ 抽象解释 + 一堆技巧，使我们能够消除与 Rust 相同类别的错误（至少在非并发环境中），*加上* 内存泄漏，并且我们可以将方法扩展到也覆盖并发环境，同时*更加*符合人体工程学且限制更少。听起来有趣吗？让我们深入探讨。 ## 它所承诺的和未承诺的 - 它是**安全的**——它完全消除了整类错误，例如： - 双重释放 - 释放后使用 - 悬空指针 - 空指针解引用 - 缓冲区溢出 - 越界访问 - 迭代器失效 - 未初始化内存访问 - 内存泄漏 单一所有权实现了线性——每个值被恰好丢弃一次——并禁止所有权循环。与用于强制执行此操作的流敏感类型系统一起，这些消除了上述大多数问题。缓冲区溢出和越界访问是单独处理的，但系统的其他机制使得处理这些问题变得简单高效。 - 它是**健全的**——我将在这个系列中证明，这些主张对任意输入都成立。系统内部没有可被用来破坏所提供保证的漏洞。 - 它**不是**简单的——有相当多的基本原语协同工作，使整个系统能够维护所承诺的安全性保证。 - 它**不**关注并发——尽管“无畏并发”保证是该系统的自然扩展，但尚未以足够完整的方式实现以证明该方法的可行性。我将在未来的文章中进一步阐述这一点，一旦我将其搭建起来。 - 它**不是**声称“零成本”，但它将运行时开销保持在最低——如果编译器无法静态证明可用性，它会引入运行时检查（每次不确定访问一个分支）。 ## 激励示例 考虑以下伪代码： ```pseudo var x: T = new T; if random() > 0.5 { drop x; } print(x); ``` 这段代码所做的是*有条件地*消费一个值。在真实语言中有两种可能的情况。 C++ 并不特别在意，会愉快地编译这段代码： ```cpp #include <cstdlib> #include <cstdio> int main() { int *i = new int(42); if ((double)rand() / RAND_MAX > 0.5) { delete i; } printf("i=%d\n", *i); return 0; } ``` 然后在大约 50% 的运行中会导致未定义行为。现代 C++ 开发者会使用 `std::unique_ptr` 和 `std::optional`——它们会有所帮助，但只是部分帮助。通过智能指针的 RAII 消除了手动的 `delete`，而 `optional` 提供了一种表示“可能已移动”的方式。但 `unique_ptr` 只管理堆分配的对象，并且类型系统并*不强制*进行 optional 检查——对空 optional 使用 `operator*` 是未定义行为，即使 `value()` 也只能给出运行时异常，而不是编译时错误。记住这一点仍然是你的责任。 然而，在 Rust 中，这段代码根本无法编译： ```rust fn main() { let x = Box::new(42); if rand::random::<f64>() > 0.5 { drop(x); } println!("{}", x); // error[E0382]: borrow of moved value: `x` } ``` Rust 采用了一种截然不同的方法。编译器通过控制流跟踪移动——它发现 `x` 在 `if` 分支中*可能*已被移动，然后直接拒绝该程序。Rust 的所有权模型要求每个变量在任何程序点上的移动状态都是静态已知的——条件性移动的值违反了该要求，因此程序被拒绝。你*可以*自己将值包装在 `Option` 中并手动 `.take()`，但 Rust 不会自动为你做这件事——负担在于开发者提前重构代码。 那么，如果在这两者之间存在第三种方式呢？ ## 提案 提议的解决方案很简单： ```pseudo var x: T = new T; if rand() > 0.5f { drop x; } // <- 此时，typeof(x) 是 Option<T> ``` 现在值的类型依赖于控制流——编译器在遍历程序时对它进行评估，每次控制流分岔时*拓宽*它，以容纳*两种*可能性。然后由开发者负责在使用时*缩小*它： ```pseudo var x: T = new T; if rand() > 0.5f { drop x; } // x 被 _拓宽_ 为 Option<T> if x { // 在这个分支中 x 肯定可用，可以使用 } else { // x 肯定不可用 } // x 再次被 _拓宽_ 为 Option<T> ``` 一种看待这个的方式是考虑编译器在不同点可用的信息： - 第一个条件语句使编译器丢失了关于 `x` 可用性的信息，通过类型系统表示为将 `x` 的类型拓宽为 `Option<T>` - 第二个条件语句向编译器提供了信息——在该语句的每个分支中，`x` 都有确定的可用性 - 但在第二个条件语句之后，我们又回到了信息不可用的状态 与 C++ 方法相比，我们现在强制开发者明确考虑状态空间并避免崩溃，因为类型检查器会捕获所有尝试在应该使用 `T` 的地方使用 `Option<T>` 或使用肯定不可用的值的操作。与 Rust 方法相比，我们以运行时检查为代价获得了灵活性——在精化点处只有一个 null/标签比较。 需要注意的是，这并非一个新想法。如果要说的话，世界上最流行的语言之一 TypeScript 正是这样做的。然而，TypeScript 编译成 JavaScript——一种具有垃圾回收和共享所有权的语言，不关心生命周期、内存或资源管理问题，也不关心并发——这些都是我需要涵盖的。 这只是冰山一角，系统的非常开端。当我们涵盖更多领域——聚合体、引用、函数调用、动态分发、lambda 和闭包时——它将增长以适应新的需求。 ## 线性丢弃 我想要的另一件事是每个值都能保证被恰好丢弃一次。这被称为*线性类型*。在讨论线性类型时，保证通常表述为“恰好使用一次”，但什么构成*使用*可能有所不同。在我的例子中，使用 == 丢弃。 使用提议的方法，这变得非常简单： - 如果值是拥有类型 `T`，那么当它或它的所有者即将离开作用域时，或者手动丢弃时，它会被丢弃——这会将其类型转换为 `None` - 如果值具有不确定的可用性——即它是 `Option<T>` 类型，其中 `T` 是拥有类型——编译器在作用域结束时插入运行时检查和条件性丢弃，但这些值也可以手动丢弃 这引出了关于精化分支的问题： ```pseudo var x: T = new T; if rand() > 0.5f { drop x; } // x 被 _拓宽_ 为 Option<T> if x { // 在这个分支中 x 肯定可用且可以使用， // 但它的类型是什么？ } else { // x 是 None } // x 再次被 _拓宽_ 为 Option<T> ``` 当 `x` 在第二个条件语句中被精化为可用状态时，它到底是什么类型？如果它被精化为 `T`，那么它会在 `if` 分支作用域结束时被丢弃。那会很愚蠢——一个给定的值只能被精化一次，使用，然后在分支结束时立即丢弃。安全，但过于严苛。 相反，我们定义一个新类型——`Some<T>`——它的唯一目的是*避免*被丢弃，或者作为*可用性的证明而不拥有所有权*。这是类型检查器以特殊方式处理的多种类型之一；即： - 当它离开作用域时不会自动丢弃——这就是重点 - 除了通过精化 `Option<T>` 之外，无法构造它——从 `T` 构造它会将所有权移入，由于 `Some<T>` 不会自动丢弃，值将会泄漏 - 它*依赖于*原始的 `Option<T>`——如果解包裹的 `Option<T>` 中包含的值以某种方式被丢弃，那么该选项的精化视图应该不可用。我将在后续文章中介绍依赖关系以及它们如何帮助我们。 - 反过来，显式丢弃 `Option<T>` 会使 `Some<T>` 无效——依赖关系是双向的 - 它可以在所有与 `T` 相同的地方自由使用。开发者可以显式丢弃它——这会消耗底层值并将原始 `Option<T>` 设置为 `None` 正如我所说——绝对*不*简单。但也不是那么复杂。 ## 形式化背景 上述方法植根于编程语言理论中几个成熟的领域。 **流敏感类型**允许变量的类型随着程序的执行而变化。大多数类型系统是流*不敏感*的——声明为 `T` 的变量在其整个作用域内保持为 `T`。流敏感系统，例如 TypeScript 的控制流收窄，跟踪类型如何沿着不同的执行路径演化。我们所做的是将其应用于*所有权*——值的可用性是它类型的一部分，并且随着程序通过移动、丢弃和条件分支流动，其可用性发生变化。 **精化类型**允许通过谓词来收窄类型。当我们写 `if x { ... }` 时，我们正在将 `x` 的类型从 `Option<T>` 精化为 `Some<T>`（或者在 else 分支中为 `None`）。这是精化类型的直接应用——条件语句充当值可用的证明，类型系统反映了这个证明。 系统的几个部分在编译期间将*值*和它们的类型*连接*起来——`Some<T>` 依赖于它所精化的 `Option<T>`，并且正如我们将在后续文章中看到的，引用依赖于它们所指向的值。这在有限的意义上与**依赖类型**相关，即类型有效性依赖于特定的程序值和所有权关系。该系统并不试图实现像 Idris 或 Agda 那样的完全依赖类型，但它确实跨函数边界和控制流跟踪值到类型的依赖关系。 **抽象解释**提供了统一的框架。编译器所做的就是抽象地在*可用性域*中解释程序——不是计算实际值，而是计算每个变量是肯定可用、肯定不可用还是不确定。分支连接会拓宽状态，而条件语句会收窄它。这是一个在简单格上的标准抽象解释：`T`（可用）和 `None`（不可用）是精确状态，`Option` 是它们的连接。 值得注意的是，可用性并不是编译器解释的唯一域。后续文章将介绍额外的域——每个都有自己的格——在相同的控制流结构上进行解释。依赖跟踪、引用有效性以及聚合体的所有权都遵循相同的抽象解释方法。 ## 迄今为止的规则 在接下来的内容中，我将维护一个运行中的规则、不变量和系统行为列表。每篇文章都会添加内容。这个列表可能看起来临时且混乱，因为*没有一个单一的语法技巧可以让所有东西都自动成立*——而是有几个基本原则协同工作，生成了许多小规则。我在开始时警告过这*不*简单。但事情是这样的：你*无论如何*都需要为了安全而维护这些规则——在 C++ 中你在脑子里做，在 Rust 中你通过和借用检查器斗争来做。这里我们所做的只是机械地将责任从开发者转移到编译器。每条规则都基于成熟的理论——我们只是以一种不需要开发者思考的方式来应用它。 1. 类型被划分为*拥有类型*和*普通类型*。拥有类型需要销毁；普通类型（整数、布尔值、浮点数）则不需要。 2. 每个拥有值恰有一个所有者。 3. 每个拥有值被恰好丢弃一次——当它或它的所有者离开作用域时，当它被显式丢弃时，或者如果其可用性不确定则条件性丢弃。 4. 条件性丢弃的拥有值被拓宽为 `Option<T>`。 5. 当 `T` 是拥有类型时，`Option<T>` 本身也是一个拥有类型。 6. 可以通过条件检查将 `Option<T>` 精化为 `Some<T>` 或 `None`。 7. `Some<T>` 是非拥有的——精化不转移所有权。 8. 通过精化 `Option<T>` 获得的 `Some<T>` 与源 `Option<T>` 相*互依赖*。 9. 精化不是粘性的——它在控制流汇合时过期。 ## 结论 因此，这是开端的结束，还有更多、更多的内容需要覆盖。在下一篇文章中，我将把这个方法推广到聚合体，例如记录和数组，并引入引用以允许共享值而不转移所有权。