分布式算法
模型：
- 异步共享存储
- 异步msg传递
- 同步msg传递
拓扑：无向图，节点为处理机，边喂双向信道. 算法：由每个处理器上的局部程序构成，包括本地计算和收发msg 节点 $p_i$, $p_i$ 相邻的边 $r$ 条. $p_i$ 有两个 buffer list: $outbuf_i[l]$ , $inbuf_i[l]$, $l \in [1, r]$
配置：某时刻，算法运行的全局状态。为一个向量 $(q0, \ldots, q{n-1})$, $q_i$ 是 $p_i$ 的状态.
状态
事件：两种
- $comp(i)$, 计算事件.
- $del(i,j,m)$, 传递事件，将msg $m$ 从 $p_i$ 传递到 $p_j$.
转换函数
执行: 配置和事件交错的序列。
- Safety 条件。 (用来证明算法正确性吗?) 该条件在每个有限前缀里的都成立
- Liveness 条件。 必须成立一定次数。
满足所有安全性条件的序列称为一个执行, 满足所有活跃性条件的 执行 为 容许(admissible) 的执行。
下面主要考虑异步msg传递系统。
执行片段 $\alpha$ 是一个有限或无限的序列:
$$ C_0, \Phi_1, C_1, \Phi_2, C_2, \ldots, $$ 其中 $C_k$ 是一个配置, $\Phi_k$ 是一个事件.
如果 $\alpha$ 有限, 则它必须结束于某个配置, 且需满足下述条件:
- 若 $\Phik = del(i,j,m)$, 则 $m$ 必须是 $C{k-1}$ 时 $outbuf_i[l]$ 的元素. $l$ 是 $p_i$ 信道 ${p_i, pj}$ 的标号. 从 $C{k-1}$ 到 $Ck$ 的唯一变化是将 $m$ 从 $C{k-1}$ 里的 $outbuf_i[l]$ 中 删去, 加入到 $C_k$ 的 $inbuf_i[h]$, $h$ 是 $p_j$ 的信道 ${p_j, p_i}$ 的标号.
- 若 $\Phik = comp(i)$, 则 $C{k-1}$ 到 $C_k$ 的变化是
- 改变状态: 转换函数在$pi$ 的可访问状态(在配置$C{k-1}$里)上进行操作，清空 $inbuf_i[l]$，$(1≤l≤r)$
- 发送 msg: 将转换函数制定的消息集合加入 $C_k$ 里的变量 $outbuf_i$ 上
调度 , 调度(或调度片段)总是和执行(或执行片段)联系在一起, 它是执行中的时间序列:
$$ \Phi_1, \Phi_2, \ldots$$
并不是每个事件序列都是调度. 例如, $del(1,2,m)$ 不是调度, 因为在此时间之前, $p_1$ 没有 send m.
若局部程序是确定的, 则执行(或执行片段)由 初始配置 $C_0$ 和调度(或调度片段) $\sigma$ 唯一确定, 可表示为 $exec(C_0, \sigma)$
容许执行: 满足活跃性条件的执行.
容许调度: 容许执行的调度.
同步系统, 同步模型中, 执行分为轮, 每轮里, (1)每个处理器能够发送一个 msg 到每个邻居 (2) 每个处理器一接到 msg 就进行计算.
轮 同步系统中, 每轮由一个传递时间(outbuf发送, 清空), 紧跟一个计算时间 (处理所有msg)
终止, 所有处理机均处于终止状态且没有msg 在传输.
msg复杂度
实际很少用状态转换来描述算法, 往往用伪码描述.