消息传递系统

进程只能根据自己的局部状态与已交付消息行动。数学上的全局配置存在于证明中，协议没有读取它的指令；“所有人现在知道什么”必须通过一串消息逐步建立。

在途消息把通信拆成两个事件，也制造了认识论缺口。接收者尚未见到消息，可能因为发送者没发、信道很慢、消息丢失或发送者已崩溃。协议能排除哪些解释，完全取决于信道、时间与故障假设。

三个进程 $p,q,r$ 中，$p$ 依次发送 $m_1$ 给 $q$、发送 $m_2$ 给 $r$。即使每条点对点信道可靠 FIFO，$r$ 仍可能先交付 $m_2$，因为 FIFO 只比较同一信道上的消息。若 $p$ 再向 $q$ 发送 $m_3$，则 $q$ 必须先交付 $m_1$ 后交付 $m_3$；无序可靠信道可以反转这两次交付，但不能永远扣住任一消息。

再设 $q$ 第一次处理请求 credit(10) 后回复丢失。$p$ 超时重传，若 $q$ 不保存请求 ID，余额会增加两次；信道层的相同 payload 无法判断这是重复还是两笔合法请求。若 $q$ 持久记录 (client,id,result)，便可重发原响应而不重做效果。该协议在 crash-recovery 下不仅要求去重表比确认更早持久化，还要求去重记录与业务效果原子提交：先记去重后入账，崩溃可能使重试被忽略而钱没到账；先入账后记去重，崩溃又可能让重试再次入账。二者放进同一本地事务，才关闭这两个相反窗口。

共享内存系统公理库共享内存系统Shared-memory system进程通过读写共享对象交互的并发模型。没有显式信道状态，进程通过读写对象交互。ABD 寄存器公理库ABD 寄存器ABD register · Attiya–Bar-Noy–Dolev register用单调版本、多数确认与读后写回实现原子寄存器，并以写前查询和二元标签扩展到多写者。用请求、响应、单调版本与多数写回模拟原子寄存器；用共享队列模拟收件箱又依赖队列原子性。偷偷加入所有节点可读的数据库或共享磁盘会改变模型，可能绕开原有故障结论。

可靠广播公理库可靠广播Reliable broadcast保证有效性、一致性和完整性的广播抽象。在点对点通信上增加共同交付性质，共识公理库分布式共识Distributed consensus · Consensus problem多个进程在可能故障和通信延迟下对一个值达成一致的任务。再要求对决定值达成一致，状态机复制把一系列决定变为共同命令日志。每层都继承底层信道假设；上层名称不会自动修复永久丢包或伪造发送者。

异步系统公理库异步系统Asynchronous distributed system消息延迟和进程相对速度没有已知有限上界的系统模型。不提供消息延迟上界，部分同步则只在未知稳定时刻后提供界。相同的可靠信道在两种时间模型中都有最终交付，却只有后者能让超时最终成为可靠的活性工具。

Chandy–Lamport 快照公理库Chandy–Lamport 分布式快照Chandy-Lamport snapshot · Distributed snapshot algorithm在可靠 FIFO 通道上用 marker 并行记录一致进程状态与在途消息的分布式快照算法。展示这些通道维度会怎样进入算法证明：经典 marker 规则要求可靠 FIFO 最终交付、快照涉及进程不崩溃，并用通道顺序区分快照前后的应用消息。非 FIFO 或故障版本需要其他算法；消息传递模型本身不内嵌 marker 协议。

有损信道系统公理库有损信道系统Lossy channel system用有限控制加无界 FIFO 字串建模有损通信，以子词顺序证明兼容性，并划清丢失、可靠性与概率保证。精确区分无界 FIFO 通信中的错误语义：消息可任意删除，但不可复制、插入或重排。子词良拟序与丢失造成的迁移单调性使控制状态覆盖可判定；这不保证消息最终送达，也不把可靠信道的可判定性问题一并解决。