并发分离逻辑

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

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

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

贡献凭证不直接拥有计数器 $x$。它在锁外保留“本线程已经贡献多少”的事实；持锁后，与锁中的同名半份合并才允许改变该项贡献。其他线程即使拿到整个锁，也只有当前线程 ghost 名字的一半，不能独自改写它。这正是局部后置在他人运行期间保持有效的原因。

不相交单元与弱共享摘要 ​

初始堆满足

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

并行规则合成

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

共享写入可以通过锁资源逐步解释。设锁的不变式为 $I_0\equiv \mathrm{\exists }n.p\mapsto n$。锁空闲时，这格内存归共享资源；线程取得锁后，暂时获得 $p\mapsto n$，读写后建立 $p\mapsto n+1$，再隐藏新值以恢复 $I_0$ 并释放锁。另一线程只能在随后取得锁时接手资源，不能在持锁者更新中途打开同一不变式。

这个存在量词不变式只足以证明安全访问，不足以独自证明“两个线程结束后值恰好增加二”。后一个结论还要在规格中追踪初值和每次更新的贡献；不能把很弱的资源摘要误当成精确功能规格。

一个客户端的完整局部推导 ​

下面使用前述精确贡献不变式 $I$。用 $i\in \{1,2\}$、$j\ne i$ 统一表示客户端；$u_i$ 是其私有临时变量。带证明注解的临界区为

Ci = with r when true do
       ui := [x]
       [x] := ui + 1
       ghost gamma_i := 1

真实程序擦除最后一行。打开锁时，$T_i(0)\ast I$ 提供两个同名半份：客户端声称零，不变式声称 $b_i$；组合一致性立即给出 $b_i=0$。设另一线程贡献为 $b_j=b$，打开后的资源可重排成

读操作得到 $u_i=b$，真实写操作得到 $x\mapsto (b+1)$，full ghost 更新得到 ${\gamma }_i{\mapsto }_g^{1}1$。再拆为两个半份，保留一份作为 $T_i(1)$，另一份与未变的 ${\gamma }_j$ 半份和新堆值一起组成 $I$，见证取 $b_i=1,b_j=b$。因此临界区内部证明

通过资源不变式的开闭规则理路并发分离逻辑的资源不变式Resource invariant in concurrent separation logic · CSL resource invariant把共享资源及其不变式交由同步对象保管，规定临界区取得、使用并在释放前完整恢复资源的开闭纪律。得到

$u_i$ 只属于该线程；地址 $x$ 的值不变，其他线程不修改这个地址变量。锁保证两次真实读写之间另一客户端不能进入，因此临界区内可暂时打破 $x=b_1+b_2$，但释放前必须恢复。

并行组合、回收不变式与精确的二 ​

从 $x\mapsto 0$ 开始，在证明中分配 ${\gamma }_1{\mapsto }_g^{1}0\ast {\gamma }_2{\mapsto }_g^{1}0$，各拆成两半。把一半留给相应客户端，另一半连同 $x\mapsto 0$ 用见证 $b_1=b_2=0$ 建立 $I$。初始化资源为

两次局部推导由并行规则合成

并行命令结束意味着两个客户端都结束；再退出容纳所有使用者的局部资源作用域，按规则归还 $I$：[2, §8.3]

打开这个最终存在量词时，两份 $T_i(1)$ 分别与 $I$ 中的半份一致，迫使 $b_1=b_2=1$，于是取得

忽略证明用 ghost 堆，投影回真实程序就得到所需的部分正确性规格：从 $x\mapsto 0$ 出发，局部锁内两个客户端各增量一次，若整个命令结束，便返回 $x\mapsto 2$。没有把锁仍保管的内存同时算进客户端后置，也没有在未回收不变式时从 token 直接读出 $x$。

两种临界区先后次序可以逐行核对；表只记录每次临界区已经关闭的时刻：

等待、取得和释放可以有更多交错；互斥保证两段实际更新仍落在上述一种次序。证明已对任意 $b\in \{0,1\}$ 给出局部规则，表格不是对调度的额外假设。

凭证防止哪些错误推导 ​

第二次调用同一客户端增量规格需要 $T_i(0)$，而第一次后只剩 $T_i(1)$；重新取得锁时，一致性只能确认旧贡献是一，不能把它当零套用上述推导。若要允许重复调用，必须改成可累计的贡献协议，不能复用这个一次性接口。

不能把 $T_i(0)$ 复制成两个半份 token：它本身只有半份，复制后两个客户端再加上锁的一半总量为 $3/2$，不可组合。允许仅凭半份更新也会破坏其他持有者的值断言。若删除真实锁，两线程可能都读零再各写一；ghost 注解不能修复这条真实的丢失更新执行。

这份证明只依赖已列出的有限资源规则、互斥临界区语义与局部作用域回收；不是对任意现代 CSL 的完整可靠性证明。一般持久不变式的消除可能需要另外的取消凭证，不能套用这里的局部资源规则。

两个线程只读同一格时，完全不交的堆模型又过于严格，需要 分数权限理路分数权限Fractional permissions · Fractional ownership permissions把完整写权限可逆地拆成若干只读份额，使并发读者能够共享同一位置而写入仍要求独占。 或其他共享只读代数。经典 CSL 也不自动建模弱内存重排、无锁算法的原子 ghost 更新、hazard pointer 或 epoch reclamation；直接套用堆不交规则会遗漏时间和内存回收协议。

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

安全性边界必须保持清楚。一个线程先拿锁 $L_1$ 再等 $L_2$，另一个先拿 $L_2$ 再等 $L_1$，仍可能在任何一步都没有越权访问，却一起死锁。局部所有权因此不说明线程最终获得资源、操作无饥饿或算法满足 lock-free 进展。工具若自动完成 entailment，也只是在受支持的断言片段中搜索证明；逻辑规则的可靠性仍依赖并发操作语义与资源代数。

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