分布式配置

分布式系统的定义性约束是"没有进程看得见全局"，而分析者恰恰要跳出这个限制：把所有局部状态与在途消息拼成一个假想的全局节点，系统的一切可能演化就变成一张图上的可达性问题。这是标准的"上帝视角"手法——它不违反模型，因为配置只服务于证明，不供协议读取。有了配置图，串行程序验证的全套武器立即可用：不变量归纳（每步转移保持某性质）、可达集分析、按图搜索反例。同样重要的是配置给"进程的无知"提供了精确语言：若两个配置在进程 $p$ 的局部状态（及其可见事件）上一致，$p$ 就无法区分它们，必须做出相同动作——不可区分性论证是几乎所有不可能性证明的杠杆。

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

边界在于"什么必须计入配置"取决于模型的完备性要求：崩溃标志、定时器读数、尚未使用的随机币、稳定存储内容——凡是会影响后续转移的信息都得纳入，否则"当前配置决定可能的下一步"这一状态机式描述被破坏，基于配置的归纳与 Markov 式论证随之失效。典型错误是在带随机化的协议里漏掉硬币状态，或在 crash-recovery 模型里漏掉稳定存储，得到的"状态空间"无法重现真实执行集合。

配置是分布式算法证明的通用底座。安全性证明写成“所有从初始配置可达的配置都满足不变量”；把配置和一步事件组成标号转移系统公理库标号转移系统Labeled transition system · Labelled transition system · LTS在状态转移上标记动作，明确路径、可达性、使能动作以及终止与死锁的行为模型。后，显式状态模型检查公理库显式状态模型检查Explicit-state model checking · Explicit model checking逐个生成和存储可达状态，以图搜索检查安全性及接受环的模型检查路线。才在其有穷化图上搜索违例。前者定义语义对象，后者是探索它的算法，状态哈希或约简不能反过来省略会影响未来行为的配置分量。自稳定理论则把“任意配置出发最终回到合法配置集”作为定义本身。最著名的应用是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满足给定调度、公平性和故障模型约束的执行。使用：执行交替记录事件与配置，二者共同给出状态变化及其原因。