并发分离逻辑

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

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

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

初始堆满足

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

并行规则合成

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

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

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

两个线程只读同一格时，完全不交的堆模型又过于严格，需要 分数权限公理库分数权限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 证明不能自动承担这项硬件保证。