并发分离逻辑 | Codeboy's Blog

形式陈述

并发分离逻辑在资源上下文 $\Gamma$ 下使用 Hoare 判断。经典并行规则的核心形状是

\frac{ \Gamma\vdash\{P_1\}\ C_1\ \{Q_1\} \qquad \Gamma\vdash\{P_2\}\ C_2\ \{Q_2\} }{ \Gamma\vdash \{P_1*P_2\}\ C_1\parallel C_2\ \{Q_1*Q_2\} }.

分离合取 $P_1*P_2$ 把可组合资源拆给两个线程。每条命令只能读取或修改其断言授权的部分；普通程序变量还须满足修改集合与另一线程自由变量不冲突等侧条件。资源上下文中的共享资源只能按逻辑规定的同步规则取得。若这些条件满足，另一线程根本没有能力触碰本地拥有的堆片段，于是大批干扰自由义务由所有权语义统一解除。

该规则通常证明部分正确性与安全执行：若两边从分离资源出发且各自局部安全，那么任意合法交错不会因越权解引用而 fault，终止时资源仍可重新组合。精确结论依所选语言的 allocation、deallocation、并发读写和故障语义而定。

这里的“局部安全”不仅是最终后置正确。每个解引用前都要拥有相应 points-to 或权限，free 要拥有可释放资源，分配要取得 fresh 单元；因此一个线程不能先发生非法访问、再碰巧恢复正确终态。并行规则把这种逐步 fault avoidance 一并组合。

直觉

传统并发证明盯着每个外来动作问“它会不会改坏我的断言”。并发分离逻辑先问“它是否拥有进入这块状态的门票”。独占资源只能出现在一个线程的断言中；没有门票的代码不能合法读写它，因此局部链表更新可与另一线程的独立树更新直接并行，而不用比较每对指令。

所有权是逻辑资源，不等同于机器地址只被一个变量引用。两个指针可以都保存同一地址，但若当前线程没有相应权限，仍不能解引用。相反，权限代数可以把同一位置的只读份额分给多个线程。关键不是指针数量，而是证明状态中资源怎样拆分、转移和重组。

纯变量也会造成干扰。即使堆片段分离，线程 1 的后置若依赖普通变量 z，线程 2 又能赋值 z，单靠星号不能保护该事实；经典规则的自由变量与修改集合侧条件正用于堵住这条缝。把所有共享状态都画成“堆”而省略 store 部分，会漏掉这一层。

例子与边界

初始堆满足

p\mapsto2*q\mapsto5.

两个线程分别执行 [p]:=[p]+1 与 [q]:=[q]+1。局部规格为

\{p\mapsto2\}\ C_1\ \{p\mapsto3\}, \qquad \{q\mapsto5\}\ C_2\ \{q\mapsto6\}.

并行规则合成

\{p\mapsto2*q\mapsto5\} C_1\parallel C_2 \{p\mapsto3*q\mapsto6\}.

无论哪次写先发生，另一格都在独立资源片段中。若 $p=q$ ，前置中的两个完整 points-to 无法分离，公式本身不可满足；逻辑不会把同址双写伪装成安全并行。

两个线程只读同一格时，完全不交的堆模型又过于严格，需要分数权限或其他共享只读代数。锁保护状态则需资源不变式，在取得锁后暂时打开、释放前关闭。经典 CSL 也不自动建模弱内存重排、无锁算法的原子 ghost 更新、hazard pointer 或 epoch reclamation；直接套用堆不交规则会遗漏时间和内存回收协议。

推论与应用

并发分离逻辑使库规格保持“小脚印”：函数只声明实际触及的资源，调用者的其余堆可由 frame 原则保留，并行规则再把不同线程的小脚印拼接。资源不变式支持锁与临界区，所有权转移支持消息和线程创建，现代逻辑还加入 ghost state、原子更新与协议状态机来证明线性一致性。

安全性边界必须保持清楚。局部所有权可以排除数据竞争和非法内存访问，却不说明线程最终获得资源、操作无饥饿或算法满足 lock-free 进展。工具若自动完成 entailment，也只是在受支持的断言片段中搜索证明；逻辑规则的可靠性仍依赖并发操作语义与资源代数。

在弱内存模型中，即使权限排除了同址竞争，不同位置的写入仍可能以另一顺序被观察。若证明依赖 release/acquire 建立 happens-before，就要把原子模式和内存序纳入逻辑规则；经典顺序一致交错语义下的 CSL 证明不能自动承担这项硬件保证。

参考资料

Peter W. O’Hearn, “Resources, Concurrency and Local Reasoning,” Theoretical Computer Science 375(1–3), 2007, pp. 271–307。
Stephen Brookes, “A Semantics for Concurrent Separation Logic,” Theoretical Computer Science 375(1–3), 2007, pp. 227–270。
John C. Reynolds, “Separation Logic: A Logic for Shared Mutable Data Structures,” LICS, 2002, pp. 55–74。
Peter W. O’Hearn, “Separation Logic,” Communications of the ACM 62(2), 2019, pp. 86–95。

形式陈述 ​

反向链接

形式陈述