消息传递系统 | Codeboy's Blog

形式陈述

设进程集合为 $P$ ，有向通信图中的弧 $(p,q)$ 表示 $p$ 可向 $q$ 发送消息。每个进程 $p$ 有局部状态空间 $S_p$ ；每条信道有状态空间 $C_{pq}$ 。FIFO 信道可用消息序列表示，无序信道可用多重集表示，有界信道还要记录剩余容量。一个全局配置属于

G= \left(\prod_{p\in P}S_p\right) \times \left(\prod_{(p,q)}C_{pq}\right),

它记录所有局部状态与在途消息，是分析者构造全局状态机时使用的对象。发送事件改变发送者状态并把带身份的消息记录加入信道；交付事件从信道取出一个当前可交付记录并更新接收者；本地步骤只改变一个进程。一次 send 完成不表示对方已经执行 receive，二者之间可以隔任意多系统步骤。

一次执行由本地、发送、交付和故障事件交错而成。可容许执行必须另行规定：正确进程是否持续取步骤；发给正确接收者的消息是否最终交付；信道是否会丢失、复制、乱序或篡改；发送者身份是否认证；容量是否有界。可靠、FIFO 与 authenticated 是不同维度。所谓“恰好一次处理”通常也不是信道的免费性质：重传提供至少一次，消息 ID 与接收方持久去重才可把应用效果限制到一次。

直觉

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

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

发送者状态、FIFO 信道中的在途消息和接收者状态共同组成全局配置，发送与交付是两个事件 — 消息传递：发送、在途与交付

例子与边界

三个进程 $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 下还要求去重表比确认更早持久化，否则重启会忘记已经执行。

共享内存系统没有显式信道状态，进程通过读写对象交互。用消息服务器模拟寄存器需要请求、响应、版本与 quorum；用共享队列模拟收件箱又依赖队列原子性。偷偷加入所有节点可读的数据库或共享磁盘会改变模型，可能绕开原有故障结论。

推论与应用

可靠广播在点对点通信上增加共同交付性质，共识再要求对决定值达成一致，状态机复制把一系列决定变为共同命令日志。每层都继承底层信道假设；上层名称不会自动修复永久丢包或伪造发送者。

异步系统不提供消息延迟上界，部分同步则只在未知稳定时刻后提供界。相同的可靠信道在两种时间模型中都有最终交付，却只有后者能让超时最终成为可靠的活性工具。

Chandy–Lamport 快照展示这些通道维度会怎样进入算法证明：经典 marker 规则要求可靠 FIFO 最终交付、快照涉及进程不崩溃，并用通道顺序区分快照前后的应用消息。非 FIFO 或故障版本需要其他算法；消息传递模型本身不内嵌 marker 协议。

参考资料

Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann, 1996，Chs. 2–7。
Hagit Attiya and Jennifer Welch, Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd ed., Wiley, 2004，Chs. 2–3。

形式陈述 ​

反向链接

形式陈述