并发分离逻辑的资源不变式

资源不变式不是“每条机器指令后都公开成立”的普通断言。锁空闲时，资源和不变式一起由锁保管；线程取得锁后可以暂时拆开不变式、更新内部状态，只要释放前恢复。其他线程在此期间无法取得同一资源，所以看不到这段逻辑上的开放窗口。

条件临界区中的 guard $B$ 也必须在取得资源、看到受保护状态后判断。若线程先在锁外读取 $B$，再等待锁，另一线程可能在等待期间改变受保护变量；把旧判断带进规则会错误使用 $(P\ast R)\wedge B$。原子取得与 guard 检查的语义正是规则成立的一部分。

这是一笔借还账：acquire 把共享堆片段转到线程局部上下文，release 要求原数归还满足新状态的片段。若线程把资源留在自己的后置中又同时关闭 invariant，就等于复制所有权；若只归还一部分，下一个取得者便拿不到声明的资源。

令锁 $r$ 保护地址 $x$，资源不变式为

线程取得 $r$ 后得到某个见证 $n$ 和完整单元 $x\mapsto n$，执行 [x]:=n+1，随后以见证 $n+1$ 建立 $x\mapsto (n+1)$ 并关闭 $R$。非负性保持，且任何时刻只有持锁线程能写该格。两个线程从 $x=0$ 各进入一次临界区，具体执行最终得到 $x=2$。

但仅凭 $R$ 的存在量词，逻辑后置只能推出最终值仍为某个非负数，不能推出恰好为 $2$。两个客户端的精确贡献证明理路并发分离逻辑Concurrent separation logic以可分资源组织并发推理，并用每线程贡献token、锁不变式与作用域回收证明两个客户端精确计数2。把每个ghost位的半份留给锁、半份留给对应线程；锁中以堆值等于两位之和作不变式。线程打开锁时由同名半份一致性确认旧贡献，合成full权限更新，再归还一半。两线程结束并退出局部锁作用域、取回不变式后，两个完成token迫使两位都是一，从而得到堆值二。把具体运行直觉冒充不变式蕴含，会掩盖证明缺口。

若线程释放锁时仍在局部后置中保留 $x\mapsto n$，或关闭后继续写 $x$，便出现重复所有权。另一个边界是原子性：经典临界区规则依赖同步原语保证互斥；把不可靠自旋标志当锁使用，需要先证明它确实实现 acquire/release 语义。现代逻辑常只允许在原子步骤附近打开某些 invariant，并用 mask 管理嵌套，这与本页的命名临界区规则相关但不是同一条无条件规则。

资源不变式把共享数据结构的表示条件封装在锁规格中。客户端不必永久携带整棵共享树或队列，只在持锁区域内取得表示资源；退出时恢复结构不变式。多把锁可各自保护不相交资源，减少一个巨大全局不变式带来的证明耦合。

同一开闭思想也出现在信号量、监视器和现代原子协议中，但同步对象必须说明何时转移资源、失败的 acquire 是否取得任何份额、异常退出怎样归还。资源不变式主要支持安全和局部推理；锁最终可得、临界区有界等待和死锁自由仍需进展或锁序证明。

局部资源作用域可在全部使用者结束后归还不变式资源，正是精确计数证明的最后一步；它不是对任意全局或持久不变式的无条件拆除许可。

多资源程序还要规定嵌套取得次序。每个局部 invariant 都可能被正确恢复，线程仍可能以相反顺序取得两把锁而死锁；反之，为避免死锁建立全局锁序，并不会自动证明每份堆资源在 release 时已归还。资源安全与进展条件应在接口中分别列出。