分布式配置

协议进程只能读取自己的局部状态，而分析者把所有局部状态与介质状态放进同一配置。前者是算法能使用的信息，后者是证明的记账对象；数学上定义配置，并没有给进程增加读取全局状态的指令。

配置足够完整，才能检查每条边是否合法：交付事件需要消息确在信道内，恢复事件需要节点已崩溃，原子交换需要按共享对象当前值返回结果。安全性证明由此化成两步：初始配置满足不变量；每个允许事件都把满足不变量的配置送到仍满足它的配置。

两个配置若在进程 P 可观察的局部状态上相同，那么确定性 P 面对相同下一输入必须采取相同动作，即使其他节点与信道状态不同。这正是不可区分性论证的出发点。随机算法还需固定已见随机结果或比较下一步的条件分布，不能无条件断言两次运行会抽到同一随机数。

正例：两个进程打乒乓的计数协议，$p_1$ 发出"计数 3"后消息尚未到达 $p_2$。此刻配置为 $(s_1,s_2,\{\text{“3”}\})$——消息不属于任何进程的局部状态，而挂在信道分量里。比较两个局部状态完全相同、仅在途消息不同的配置：一个信道里有"3"、另一个信道为空。前者交付消息后 $p_2$ 会继续推进，后者则可能永远等待——未来行为截然不同。这说明"局部状态之积"并不足以刻画全局状态，介质分量是配置定义里不可省略的部分。

边界在于"什么必须计入配置"取决于模型的完备性要求：崩溃标志、定时器读数、预采样随机带的位置、稳定存储内容——凡是会影响后续转移的信息都得纳入，否则"当前配置决定可能的下一步"这一状态机式描述被破坏，基于配置的归纳与 Markov 式论证随之失效。随机化有两种常用记法：预先固定随机带时须记录带内容及读取位置；用概率转移核直接生成新随机结果时，不必把尚未抽取的未来硬币塞进当前配置，但必须保留影响其分布的状态。Crash-recovery 则必须区分稳定存储与易失状态，否则重启边无法表达究竟忘掉什么。

若 A 发送带编号 m 的消息后信道为 [m]，再发送同内容的新消息 n，则 FIFO 配置为 [m,n]。交换为 [n,m] 会改变下一次合法交付；无序信道可用多重集保存二者，但仍不能简化成只含 payload 的集合，否则两条合法消息会被合并。配置表示选择必须保留模型真正区分的历史。

配置是分布式算法证明的通用底座。安全性证明写成“所有从初始配置可达的配置都满足不变量”；把配置和一步事件组成标号转移系统公理库标号转移系统Labeled transition system · Labelled transition system · LTS在状态转移上标记动作，明确路径、可达性、使能动作以及终止与死锁的行为模型。后，显式状态模型检查公理库显式状态模型检查Explicit-state model checking · Explicit model checking逐个生成和存储可达状态，以图搜索检查安全性及接受环的模型检查路线。才在其有穷化图上搜索违例。前者定义语义对象，后者是探索它的算法，状态哈希或约简不能反过来省略会影响未来行为的配置分量。

终止检测公理库分布式终止检测Distributed termination detection用活动状态与在途基本消息共同定义终止，将不误报、最终检测与外部任务边界分别说明。尤其依赖完整配置：全体节点被动仍可能有一条任务在途，宣布完成必须同时排除两者。自稳定公理库自稳定系统Self-stabilization · Self-stabilizing system将任意允许初态后的收敛与合法集闭包分开证明，明确瞬时故障、调度器与恢复期间的规格范围。则改变初态量词，从任意允许配置证明最终进入合法集，并另外证明合法集的正常转移闭包；只证明好初态不变式不足以说明坏态能恢复。

FLP不可能性公理库FLP 不可能性定理FLP impossibility · Fischer–Lynch–Paterson theorem完全异步系统中即使只允许一个进程崩溃，也不存在保证所有可容许执行终止的确定性共识协议。的论证也生活在配置空间里：把配置按可能的决定值分为二价与单价，再证明对手调度能让系统永远停留在二价配置中。

一致切片公理库一致切片Consistent cut · Consistent global cut对事件因果前驱向下闭合、因而可解释为分布式全局状态的执行切片。从每个进程取一个因果向下闭合的事件前缀，由各前缀末端局部状态和跨边界在途消息组成一个全局配置。它不要求这些局部状态在同一物理时刻真实并列；Chandy–Lamport 快照公理库Chandy–Lamport 分布式快照Chandy-Lamport snapshot · Distributed snapshot algorithm在可靠 FIFO 通道上用 marker 并行记录一致进程状态与在途消息的分布式快照算法。则是在特定通道假设下构造这种配置的算法。配置也搭配分布式执行公理库分布式执行Distributed execution · Distributed run由全局配置与进程内部、发送、接收事件交替组成的系统演化路径。与可容许执行公理库可容许执行Admissible execution满足给定调度、公平性和故障模型约束的执行。使用：执行交替记录事件与配置，二者共同给出状态变化及其原因。