分数权限 | Codeboy's Blog

形式陈述

在简化的有理份额模型中，断言 $\ell\mapsto^{\pi}v$ 表示以份额 $0<\pi\le1$ 拥有位置 $\ell$ ，并知道其值为 $v$ 。兼容份额满足

(\ell\mapsto^{\pi}v)* (\ell\mapsto^{\rho}v) \equiv \ell\mapsto^{\pi+\rho}v, \qquad \pi+\rho\le1.

同一位置的碎片必须同意当前值；份额总和不能超过 $1$ 。任意正份额通常允许读，写入和释放则要求完整份额 $1$ 。因此分离合取不再强制地址域完全不交，而是要求底层权限资源可组合。

读写规则把这一区别写进前置条件。读操作可以保持任意正份额：

\{\ell\mapsto^{\pi}v\}\ r:=[\ell]\ \{\ell\mapsto^{\pi}v\land r=v\}, \qquad \pi>0.

写操作则消费并恢复完整权限：

\{\ell\mapsto^{1}v\}\ [\ell]:=w\ \{\ell\mapsto^{1}w\}.

只要资源账本始终可组合，就不存在一个合法写者与另一个合法读者同时访问同一位置。

有理数加法只是教学模型。更一般的 share algebra 可以使用树形份额、嵌套权限或其他非数值表示，并把组合定义为部分交换运算；存在二元拆分规则并不意味着允许任意无穷份额求和。无论表示如何，可靠性的关键都是：两个可同时存在的非完整份额不能各自授权冲突写，而所有碎片重新汇合后可以恢复独占能力。

直觉

完整权限像原件，能读、改和销毁；把它撕成两张可验证的半份凭证后，两位持有人都能确认内容，却没有任何一人能单独改动原件。只有把所有凭证收回，写权限才恢复。这里的分数不是“这个线程大概拥有一半内存”，而是可精确守恒的逻辑能力。

这种设计填补了纯堆不交模型的空隙。只读查表、并行遍历和共享不可变配置不需要强迫只有一个线程持有地址；同时，写者必须等待所有读份额归还，因而不会与读者并发修改同一位置。

例子与边界

初始资源为 $\ell\mapsto^{1}42$ 。利用拆分等式可得到

\ell\mapsto^{1/2}42* \ell\mapsto^{1/2}42,

把两份分别交给线程 A、B。二者都能读取并验证结果为 $42$ ，却都无法满足写规则所需的份额 $1$ 。线程结束后重新组合两份，恢复 $\ell\mapsto^{1}42$ ，此时才可执行写入并得到 $\ell\mapsto^{1}43$ 。

若只收回 A 的一半，持有者总份额仍是 $1/2$ ，写入义务失败；把“没人正在读”当作逻辑事实不能补出丢失的份额。若两份分别声称值 $42$ 与 $43$ ，它们也不可组合，因为同一实际位置不能同时具有两个当前值。

拆分不必只有两份。例如三个工作线程可各得 $1/3$ ，分别扫描同一只读表；join 后用结合律合成 $1/3+1/3+1/3=1$ ，再进入更新阶段。若某个异常分支没有归还自己的 $1/3$ ，其余两份最多合成 $2/3$ ，逻辑会在写入点暴露资源泄漏，而不是根据线程已经退出便自动补齐。

允许任意正份额写会立刻破坏规则：A、B 各拿 $1/2$ 后可以并发写不同值，资源账面没有超额，实际却产生数据竞争。零份额通常等同没有访问权，不能用来读取。权限也不自动解决对象生命周期：线程可能保有读份额时，完整份额就不可能被合法回收；何时收齐所有份额仍需协议或作用域证明。

推论与应用

分数权限支持读写锁的规格：读锁取得一个非零份额，多个读者的份额可共存；写锁必须取得完整份额，因而排除所有读者与其他写者。fork/join 并行循环可在 fork 时拆分数组元素的读权限，在 join 时重新合并，再进入写阶段。

份额记录的是访问权，不是程序中有多少指针别名，也不保证持有者最终归还。带借用、线程取消或异步回调的语言需要说明份额怎样跨作用域移动；自动权限推断若返回 unknown，也不能把缺少证明当成没有竞争。

份额还可附在递归数据结构的不同层次：遍历者拥有每个节点的读份额，维护线程只有在回收整条路径的全部份额后才能旋转或释放节点。这里的算术守恒是安全证书，不是运行时引用计数；实现可以完全擦除这些分数，只要类型或逻辑证明确保相同访问纪律。

同样的份额代数可用于证明用ghost单元，但须单独规定新鲜分配、full更新和擦除规则。精确共享计数器让锁与客户端各持一个贡献位的半份；持锁时合成完整权限修改，释放前重新拆开。另一线程即使取得锁，也无法独自更新缺少客户端半份的贡献。这利用的是同名份额的值一致性，半份不会自行授权写入。

参考资料

John Boyland, “Checking Interference with Fractional Permissions,” Static Analysis Symposium, LNCS 2694, 2003, pp. 55–72。
Richard Bornat, Cristiano Calcagno, Peter O’Hearn, and Matthew Parkinson, “Permission Accounting in Separation Logic,” POPL, 2005, pp. 259–270。
John Boyland, “Semantics of Fractional Permissions with Nesting,” ACM TOPLAS 32(3), 2010, Article 6。