并发分离逻辑中的所有权转移

发送裸指针像告诉别人仓库地址；所有权转移还要把钥匙交出去，并从自己的钥匙串上取下。接收者得到钥匙后可以按权限读写或释放，发送者即使仍记得地址，也不能再合法开门。逻辑通过前后条件中的资源消失和出现记录这笔交接。

转移比永久共享更容易保持局部性：任一时刻资源只有一个完整所有者，不需要每次访问都重新分析竞争。若只转移一个分数份额，双方可以共享读取，但任何一方都没有写或释放的完整权力；资源谓词精确说明交出去的是多少能力。

发送线程分配一个单元并得到 $\ell \mapsto 42$，定义

调用 send(c,ℓ) 前，它拥有 $P\ast (\ell \mapsto 42)$；调用后只剩 $P$，因此随后执行 [ℓ]:=0 无法满足写前置。接收线程执行 p:=recv(c) 后取得 $p\mapsto 42$，可以读出 $42$，再以完整所有权执行 free(p)。从分配到释放，资源依次由发送者、通道、接收者拥有，账本中从未同时出现两份完整 points-to。

若通道可能重复投递，同一个 $M(v)$ 会被两个接收者取得，规则不再可靠；若消息丢失，资源可能永久留在通道中，影响泄漏和终止性质。广播需要可复制的纯事实或预先拆分的只读份额，不能广播线性写权限。超时与取消还要规定尚未交付的资源退还发送者、留在队列还是转入清理线程。

地址序列化到另一进程也不自动搬运本地堆所有权；跨地址空间消息通常传数据副本、共享内存句柄或协议 token，各有不同资源模型。内存回收中的 ABA、hazard pointer 和 epoch 同时依赖时间与读者存活信息，不能只用一次 send/receive 转移概括。

异步缓冲区还区分“send 已返回”与“receiver 已取得”。两事件之间资源属于通道内部队列，因此队列表示不变式必须把每个待收消息的 $M(v)$ 一并保存。只在发送者和接收者端各写一个三元组、却让缓冲区摘要遗漏资源，会在这段时间造成逻辑资源凭空消失；接收方后来也就不能有根据地取得所有权。

所有权转移为流水线、actor 邮箱、工作窃取队列和生产者—消费者协议提供模块化规格。每个阶段只验证自己持有对象期间的局部操作，消息谓词则承担阶段之间的数据结构表示关系。通道实现若被证明满足消息资源协议，客户端无需展开其锁和缓冲区。

同一思想还能表达 API 生命周期：打开文件返回句柄 token，close 消耗 token；线程 spawn 消耗子任务前置，join 产生其后置。资源守恒能排除 double free 和 use-after-transfer，但不保证消息最终到达或接收者最终释放，后两者属于可靠传输与活性规格。

对于带选择接收或超时的 API，最清楚的规格往往给每个返回分支不同资源后置：收到值时产生 $M(v)$，超时时保持原有 $Q$，取消成功时说明缓冲中的资源由谁回收。把所有分支写成同一个模糊后置，会丢失所有权究竟停在哪里的关键信息。