第二章 同步网络模型
2.1 同步网络系统
同步网络系统是由一组位于有向网络图节点位置的计算元素组成，计算元素可看为处理器或者进程。
首先为了形式化定义在同步网络系统中的节点，定义了以下几个部分：
有向图G=(V，E)，distance(i,j)表示在G中从i到j的最短有向路径的长度，i表示任意节点
states[i]，一组状态的集合（不一定是有限集合，计数器是无界数据结构），称为状态集
start[i]，states[i]的子集，称为开始状态集
msgs[i]，一个消息生成函数，从给定状态开始到进程i向指定的邻接节点发出的消息
trans[i]，一个状态迁移函数，每个状态和所有来自入向邻接节点的消息集合，进程i需要迁移到的状态
链路，G中的每一条边（i,j）存在一条通道
整个系统的运行以所有进程处于任意开始状态和所有通道都为空开始。所有的进程在每个时间重复执行以下步骤：
- 对当前状态消息生成函数，生成所有向出向邻接节点发送的消息。把这些消息放在相应的通道上。
- 对当前状态的入向消息状态迁移函数，获得新的状态。并删除通道上所有的消息。
需要考虑的几个问题：
- 停止，如何分辨出那些状态是进程的停止
- 变量开始时间，考虑同步系统中进程可能从不同的轮次开始执行。我们在网络图中添加一个特殊的环境节点，该节点与所有的普通节点相连。环境节点的环境进程的工作是向其他所有普通节点发送特殊的唤醒消息。其中每个进程的所有初始状态需是休眠的，并且只有当它从环境节点收到唤醒消息或者从其他普通节点收到非空消息，它才迁移到新的状态
- 无向图，考虑网络图是无向图的情况
2.2 故障
同步系统的各种故障，包括进程故障和链路（通道）故障，Byzantine故障。
- 进程故障，比如在上一节的第一步或者第二步发生故障。在第一步发生故障可能只把预期的消息子集放入消息通道中，并且任意子集不一定是顺序的产生的消息子集，可能是消息集的中间段
- Byzantine故障，随意的方式产生下一个消息和下一个状态，而不遵循它的消息产生和状态迁移函数所指定的规则
- 链路故障，丢失消息，比如一个链路没有承载此消息
2.3 输入和输出
定义输入输出，一个进程可以有多个开始状态，并且输入放在开始状态中指定的输入变量中。当一个进程可以有多个开始状态，那么系统需要适应不同的可能输入。输出指的输出变量只记录所执行的第一个写操作，也就是一次写入变量。然而输出变量可被读任意多次。
2.4 运行
定义运行，形式化的描述：
- 状态赋值（state assignment）被定义为对该系统的每个进程赋值一个状态
- 消息赋值（message assignment）是对每个通道赋值一条消息（可以是空消息）
- 系统的运行定义为一个无限的序列，C[0],M[1],N[1],C[1],M[2],N[2],C[2],.............，其中C[r]是状态赋值，M[r]和N[r]为消息赋值（分别是发送和接受消息），C[r]代表r轮后系统状态，C[r]某个时刻r的状态赋值，r是指执行r轮之后的时间点
- 假设A和B是一个系统的两次运行。如果A和B两次运行中，进程i有相同的状态序列、输入和输出消息序列，则称A和B对于进程i是不可区分的
2.5 证明方法
如何证明，使用不变式断言的证明。一个不变式断言是指系统状态（所有进程的状态）的一个属性，该属性在每一轮之后的每次运行都成立。并且可以在断言中有完成轮数，这样就可以证明每次r轮之后的状态。
还有一种方法证明是模拟。为了证明同步算法A，又实现了另外一个同步算法B，即两者产生相同的输入/输出行为。当两个算法在相同的轮数出现相同的故障时，A和B之间的对应关系用与A和B状态相关的断言来描述。这样断言是模拟关系，它一般是通过对已完成的轮数来证明。
2.6 复杂度度量
同步的分布式算法，考虑时间复杂度和通信复杂度。
时间复杂度的度量是根据所有输出都生成或者进程全部停止时已运行的轮数。如果系统允许可变的开始时间，则时间复杂度是任一进程被唤醒的第一轮开始度量。
通信复杂度是按照已发送的非空消息的个数来度量。
一般来说时间复杂度更重要，只有当阻塞到使处理进程缓慢才变得重要。比如在许多分布式算法同时运行，共享同一网络带宽。任一单个算法在加入链路的消息负载都会增加该链路总的消息负载。
2.7 随机化
我们不要求进程是确定性的，有时候，允许它们基于某一给一定的概率分布进行随机选择。，在基本的同步系统模型中不允许这一点。我们在消息产生和状态迁移两个函数的同时，添加一个随机函数来表示随机选择的步骤，用形式化描述就是在每一阶段i的自动机描述中增加一个rand部分；对于每个状态s，rand(s）是states的某个子集上的一个概率分布。现在，在每轮运行中，首先用随机函数rand选出新的状态，然后按常规应用msgs和trans函数。系统运行的无界序列为，C[0],D[1],M[1],N[1],C[1],D[2],M[2],N[2],C[2],............，其中D[r]是新添加的状态赋值。
对随机系统计算内容的声明通常是概率化的，断言某些结果至少有一定的出现概率。当作出这样的声明时，一般认为它对所有输入和所有的故障模式都成立。为了对输入和故障模式建模，通常假设有一个称为“对手”的假想实体控制着输入的选择和故障的发生，那么，概率性声明断言系统在与任意合法“对手”的竞争中表现良好。