分布式执行

形式陈述 ​

设 ${\mathcal{C}}_0$ 为初始配置集合，$\mathrm{enabled}(C)$ 给出配置 $C$ 中可执行的事件，$\delta (C,e)$ 给出执行事件后的配置。一次分布式执行是有限或无限路径

$$C_0\stackrel{e_1}{\to }{C}_1\stackrel{e_2}{\to }{C}_2\stackrel{e_3}{\to }\cdots ,$$

其中 $C_0\in {\mathcal{C}}_0$，每个 $e_i\in \mathrm{enabled}(C_{i-1})$，且 $C_i=\delta (C_{i-1},e_i)$。事件可以是进程内部步、消息发送或接收、共享对象访问、计时器触发和模型允许的故障。

上述序列是某个调度给出的全序交错。由同一进程的事件顺序以及每条消息的发送—接收边生成 happens-before公理库Happens-before 关系Happens-before · Causal order由进程内顺序与消息传递生成的事件因果严格偏序。 因果偏序；不同的全序执行可以是同一因果事件结构的不同线性扩展。进程投影只保留该进程的局部事件和可见输入，接口投影则可产生 并发对象历史公理库并发对象历史Concurrent object history · Invocation-response history按线程记录对象操作调用与匹配返回的有限或无限事件序列。，两种投影都会丢失部分全局信息。

直觉 ​

分布式执行把“系统如何一步步演化”固定成配置图上的路径。全序不是说系统拥有可观测的全局时钟，而是分析者选择一种合法调度来枚举原子事件；因果偏序再剥离彼此独立事件之间偶然的排列。

配置记录某一时刻会影响未来的全部状态，事件记录造成变化的原因。只保留其中一边都会丢信息：裸事件列表需要初始状态才能重放，裸配置终点则无法说明中间经历了哪些消息和故障。

例子与边界 ​

进程 $p$ 发送消息 $m$，信道状态在后继配置中加入 $m$；若稍后 $q$ 接收它，接收事件必须因果晚于发送事件。两个互不通信的进程各做一步时，调度可以把任一步排在前面，这两条全序路径却表达同一并发关系。

各机器日志按本地时间戳合并不一定得到合法执行：时钟漂移可能把接收排在发送之前，日志也可能遗漏内部或故障事件。无限执行是否属于算法承诺的范围，还要由公平性、消息可靠性和故障上界筛选；这些额外条件定义 可容许执行公理库可容许执行Admissible execution满足给定调度、公平性和故障模型约束的执行。，不属于本条的裸路径合法性。

推论与应用 ​

安全性可对所有可达执行前缀量化，活性则通常只对满足公平环境假设的无限执行量化。配置不可区分性、因果序、调度对手、模型检查与 FLP 类不可能性证明都以分布式执行为对象。将执行投影到进程或接口，可连接局部知识、trace 语义和并发对象一致性。

参考资料

• Nancy A. Lynch, Distributed Algorithms, Morgan Kaufmann, 1996, Chapters 1–3.
• Hagit Attiya and Jennifer Welch, Distributed Computing, 2nd ed., Wiley, 2004, Chapters 2–3.