'db 生命周期
Tracked 结构体和 interned 结构体都会带一个 'db 生命周期。
这个生命周期与创建它们时使用的 db: &DB 引用绑定在一起。
'db 生命周期带来了几个重要影响:
- 它保证了当某个 tracked / interned 结构体仍在被活跃使用时,
用户不能开启一个新的 Salsa 修订。
因为开启新修订需要修改 input,而这要求拿到
&mut DB, 所以在'db生命周期期间这件事不可能发生。- 而且该结构体在新修订中甚至可能根本不存在, 所以允许继续访问它本身也会让语义变得混乱。
- 它也使得这些结构体可以用指针来实现,而不是
salsa::Id, 从而让字段访问更高效(不再需要读锁)。
本节讨论的就是这种基于指针访问所用到的 unsafe 代码,以及背后的推理。 为了更具体一些,我们主要聚焦 tracked struct, 因为 interned struct 与它非常相似。
关于 UB 的说明
当本页说“用户不能做 X”时, 我们的意思是:在不触发 Undefined Behavior 的前提下,用户不能做 X。 例如通过随意 transmute 整数之类的方式并不在讨论范围内。
需要证明的义务
下面是一个 tracked struct 的典型生命周期, 以及其中那些需要我们为 unsafe 假设给出证明的用户操作:
- 某个 tracked 函数
f在修订 R0 中执行, 第一次创建了一个#[id]字段为K的 tracked struct。K会被存进 interning hashmap,并映射到一个全新的标识符id。- 标识符
id会作为StructMap的键,指向一块新分配的内存alloc : Alloc。 - 一个
ts: TS<'db>会由这个原始指针alloc构造出来,并返回给用户。
- 用户通过
ts.field(db)访问ts的字段field。- Unsafe: 这一步会访问指向
alloc的原始指针。
- Unsafe: 这一步会访问指向
- 开始一个新修订 R1。
- tracked 函数
f在 R1 中没有重新执行。 - 用户再次通过
ts.field(db)访问字段field。- Unsafe: 仍然是在访问指向
alloc的原始指针。
- Unsafe: 仍然是在访问指向
- 开始一个新修订 R2。
- tracked 函数
f在 R2 中重新执行, 并再次以键K创建了一个 tracked struct,但字段值(某些)发生了变化。ts的字段会被更新。
- 用户再次通过
ts.field(db)访问字段field。- Unsafe: 这里仍然会访问指向
alloc的原始指针。
- Unsafe: 这里仍然会访问指向
- 开始一个新修订 R3。
- 当
f这次执行时,它不会再创建一个键为K的 tracked struct。 因此 tracked structts会被放进“待删除”列表。 - 开始一个新修订 R4:
- 分配
alloc被释放。
- 分配
如上所示,用户能够触发的核心 “unsafe” 操作,
就是访问 tracked struct 的字段。
tracked struct 内部保存的是一个指向 alloc 的原始指针,
这块内存由 ingredient 持有,并包含字段数据。
而访问字段时会返回一个指向 alloc 内字段的 & 引用,
这意味着我们必须保证 Rust 的两个核心约束在这个引用的生命周期内始终成立:
alloc这块分配不会被释放(也就是不会 drop)。- 字段内容不会被修改。
而从上面的序列可以看出,我们需要在多种场景下证明这两件事:
- 新创建出来的 tracked struct。
- 在旧修订中创建、并在当前修订中被重新验证过的 tracked struct。
- 在当前修订中字段被更新过的 tracked struct。
- 在当前修订里并未被创建的 tracked struct。
定义
对于任意 tracked struct ts,
我们称它有一个定义查询(defining query)f(..)。
这指的是 tracked 函数 f 的某一次具体调用,
其中参数集合 .. 也是特定的。
在单个修订内,这个定义查询是唯一的,
也就是说,对同一组参数,f 最多只会执行一次。
我们说一个查询在修订 R 中执行过, 是指它的函数体在该修订里真的被执行了。 一旦发生这种情况, 该查询定义(创建)的所有 tracked struct, 都会与这个查询结果一起被记录下来。
我们说一个查询在修订 R 中被验证过, 是指 Salsa 系统判定它的输入没有变化, 因此跳过了函数体执行。 这同样会导致该查询定义的 tracked struct 被视为已验证 (更具体地说,我们会在它们身上执行一个函数,更新一些内部字段,稍后会解释)。
当我们谈到 ts 时,我们指的是……
定理:在新修订开始时,所有对 ts 的引用都位于 Salsa 数据库内部
在 ts 被删除之后,
仍然可能存在一些 memoized 值继续引用 ts,
但它们必须有某个 red input query。
即使用户函数是非确定性的,这件事还成立吗?
直觉上的论证是:成立。
因为基于“不可伪造性”,
那些 memoized 值本身其实无法被用户拿到并继续访问。
那么这些 memoized 值最初是如何得到 TS<'db> 的呢?
它只能来自某个函数参数(XX:那 thread-local state 呢)。
所以如果要再次访问这个值,
用户必须重新提供那些函数参数。
但这些参数本身又是怎么来的?
潜在漏洞包括:
- 某些 thread-local API 可以把
'db值“隐式地”往下传, 从而让你在返回值里带出它们,而它们并没有显式出现在参数里。 例如一个 tracked 函数() -> S<'db>, 它实际上是从 thread-local state 里取到值的。- 我们也许可以通过定义一组 trait, 去静态检查返回值里的生命周期标记内容“理论上都可能来自某个参数”, 但我并不觉得这能彻底证明一切。 所以我们要么告诉用户“别这么做”, 要么就需要某种动态检查机制,例如带版本号的指针。 需要注意,这件事目前确实会涉及 unsafe, 但更多是因为现有 API 的能力边界。
- 另一种思路是把删除对象的清理工作做得更彻底。 这个方向是可行的。
- 还有那些很奇怪的
Eq实现之类的问题呢? 我们是不是也得把它们视作 unsafe?
定理:在修订 R 中访问 tracked struct ts,其定义查询 f(..) 必须已经在 R 中执行过或被验证过
这是后续大部分推理的核心。
基本想法是:用户不能“伪造”一个 tracked struct 实例 ts。
他们只能通过 Salsa 的内部机制拿到它。
这点非常关键,
因为 Salsa 会把指向字段内部的 & 引用交给用户,
而这些引用在一个修订内必须保持有效。
但在新修订开始时,Salsa 可能会修改这些字段,甚至释放对应分配。
之所以这仍然安全,
就是因为用户不可能在新修订开始时还持有对 ts 的可用引用。
引理
我们会沿着前面那条生命周期序列,按修订顺序推进证明 (也可以把它看作一种归纳证明)。
在 R0 第一次创建 ts 之前
用户最初拿到 ts: TS<'db>,
必然是通过调用 TS::new(&db, ...)。
原因是,创建 TS 实例需要提供一个 NonNull<salsa::tracked_struct::ValueStruct> 指针,
而这是某个 unsafe 函数的参数,
其契约要求这个指针必须有效。
FIXME: 严格来说这句话现在还不完全正确。 我觉得构造函数目前可能只是个私有 tuple ctor, 我们应该把这点修正掉。
在 R0 期间
归纳情形:考虑某个修订 R
我们先展示一些不可能发生的情况:
- 访问一个从未被创建过的 tracked struct
ts的字段。 - 在
ts已经被释放后继续访问它的字段。
引理(不可伪造):用户无法伪造 tracked struct
第一个观察是:用户无法“伪造”一个 tracked struct ts 实例。
他们必须拿到一个指向 Alloc 的指针。
这意味着每个 tracked struct ts 的来源都只能是 ingredient。
而像 input struct 就不是这样,
因为 input struct 只是用整数 id 构造出来的,用户完全可以自己随便编一个。
引理(单修订内):用户无法跨修订持有 tracked struct ts
tracked struct ts: TS<'db> 的生命周期 'db 是由一个 db: &'db dyn Db 句柄生成出来的。
而开启一个新修订需要拿到 &mut 引用。
因此,只要用户还在活跃地使用 ts,数据库就不可能开始新修订。
检查点: 如果用户手里有两个数据库并调用了一些内部方法,会不会绕过这个约束? 也许会,我们可能需要再补一些断言。
定理:在修订 R0 中拿到 tracked struct ts,创建它的 tracked 函数 f 必须先执行过或被验证过
上面两个点结合起来,就能推出……
创建新值
每个新值都会通过 StructMap::insert 被存放进一个 salsa::alloc::Alloc 中。
Alloc 可以看作标准 Rust Box 的一种变体,
但它不携带唯一性语义。
这意味着每个 tracked struct 都有自己单独的一块分配。
这块分配由 tracked struct ingredient 持有,
因此只要 tracked struct ingredient 还活着,
或者它尚未被移除,
这块内存就会保持有效
(至于移除时如何保证安全,稍后还会继续讨论)。
用户可见类型内部使用的是原始指针
#[salsa::tracked] 宏会生成一个暴露给用户的结构体,
大致形如下:
#![allow(unused)] fn main() { // 这个结构体包装了实际字段, // 额外附带一些修订元数据。 // 你可以把它理解为 tracked struct 字段的一层 newtype 包装。 use salsa::tracked_struct::ValueStruct; struct MyTrackedStruct<'db> { value: *const ValueStruct<..>, phantom: PhantomData<&'db ValueStruct<...>> } }
这里有两个关键点:
- 运行时实际保存的并不是指向
ValueStruct的 Rust 引用,而是原始指针。 这是为了符合 stacked borrows 规则。 PhantomData被用来维持'db生命周期信息。
我们之所以在结构体里存原始指针,
是因为这个结构体实例本身会活得比某次具体的 'db 引用更久。
看下面这个例子:
#![allow(unused)] fn main() { let mut db = MyDatabase::default(); let input = MyInput::new(&db, ...); // Revision 1: let result1 = tracked_fn(&db, input); // Revision 2: input.set_field(&mut db).to(...); let result2 = tracked_fn(&db, input); }
tracked_fn 在 Revision 1 创建的 tracked struct,
可能会在 Revision 2 中被复用,
但创建它们时使用的那个原始 &db 引用已经过期了。
如果我们把它存成真正的 Rust 引用,
那就会违反 stacked borrows 规则。
因此我们选择保存原始指针; 当用户调用某个字段访问器时, 我们再临时创建一个新的引用:
#![allow(unused)] fn main() { impl<'db> MyTrackedStruct<'db> { fn field(self, db: &'db dyn DB) -> &'db FieldType { ... } } }
这个引用与 db 绑定,
并且只要……
“静止状态”下的 'db 生命周期
跨修订更新 tracked struct 字段
XX
安全性引理
这些引理用于支撑整个系统的安全性论证。
在某个修订 R 中使用 MyTracked<'db>,总是发生在一次 MyTracked::new 调用之后
当某个 tracked struct 实例 TS<'db> 第一次在修订 R1 中被创建时,
其结果对应的是一块全新的分配,
因此此前不可能已经存在它的别名。
此时 TS<'db> 也会被存入 Salsa 数据库。
而在后续修订里,我们断言……
&'db T 引用永远不会被存进数据库
我们维护一个不变量:在后续任意修订 R2 中,……
然而在某个更晚的修订 R2 中,又是如何……