基于定时器的通信协议解析

### 基于定时器的通信协议解析 #### 1. 引言 在通信协议的设计与验证中，定时器起着至关重要的作用。本文将深入分析一种基于定时器的通信协议，该协议不仅提供了数据传输机制，还能实现连接的打开与关闭，并且对消息的丢失、重复和乱序具有一定的容错能力。 #### 2. 协议基础与假设 ##### 2.1 滑动窗口协议相关 在一些协议中，如滑动窗口协议，存在一些关键的参数和性质。对于数据包集合中的元素，其序号有一定的范围限制。例如，若 $(pack, w, i) \in Q_p$，根据相关条件和引理可知，$i < S_q + l_q$ 且 $i < s_p + L$，同时 $i \geq O_p - l_p$ 且 $i \geq s_p - L$，对于 $Q_q$ 中的数据包也有类似结论。基于此引理，以模 $k$（$k \geq 2L$）的方式发送数据包即可，因为已知 $s_p$ 和 $i \bmod k$ 就能计算出 $i$。 协议中常量 $l_p$ 和 $l_q$ 的取值对协议效率有重要影响，其对协议吞吐量的影响可通过概率分析得出，而最优值取决于多个系统相关参数： - **通信时间**：即进程两次连续操作之间的时间。 - **往返延迟**：数据包从 $p$ 发送到 $q$ 并收到 $q$ 的回复所需的平均时间。 - **错误概率**：特定数据包丢失的概率。 当 $L = 1$，即 $l_p = 1$ 且 $l_q = 0$（或反之）时，可得到滑动窗口协议的一个特殊情况——交替位协议。此时，变量 $O_p$ 和 $a_q$ 初始化为 $-l_p$ 和 $-l_q$，且始终有 $O_p + l_q = s_p$ 和 $a_q + l_p = S_q$ 成立，因此协议中只需存储 $O_p$ 和 $s_p$（以及 $a_q$ 和 $S_q$）中的一个。若进一步限制定时器的使用，确保站点轮流发送消息，就能得到著名的交替位协议。 ##### 2.2 定时器协议假设 本文所研究的协议是 Fletcher 和 Watson 提出的用于端到端消息通信的 $\tau$-协议的简化形式。为了聚焦于协议的连接管理机制和定时器的作用，对协议进行了如下简化： 1. **单向传输**：数据仅从 $p$（发送者）传输到 $q$（接收者），但协议使用反向的确认消息（从 $q$ 到 $p$）。若要实现双向传输，可额外执行一个角色互换的协议，并引入包含数据和确认信息的组合消息。 2. **单字接收窗口**：接收者仅考虑并立即交付下一个预期的数据包，不存储序号高于预期的数据包。更复杂的版本会存储提前到达的高序号数据包，并在低序号数据包全部到达并交付后再进行交付。 3. **简化的定时假设**：协议使用最少数量的定时器。假设只要接收者端的连接处于打开状态，接收进程可随时发送确认消息。同时，省略了触发数据重传的定时器机制，仅保留保证协议安全性的必要机制。 4. **单字数据包**：发送者每个数据包只能包含一个单字，若数据包能包含连续的字块，协议效率会更高。 此外，关于系统中的时间和定时器有以下假设： - **全局时间**：系统中所有进程有一个全局的时间度量，每个事件发生在特定时间，且事件本身持续时间为 0，进程无法观察到事件发生的时间。 - **有限的数据包生命周期**：数据包的生命周期受常量 $\mu$（最大数据包生命周期）限制。若数据包在时间 $\sigma$ 发送，在时间 $\tau$ 接收，则 $\sigma < \tau < \sigma + \mu$。若数据包在信道中被复制，每个副本必须在原数据包发送后的 $\mu$ 时间内被接收，否则丢失。 - **定时器**：进程无法观察其操作的绝对时间，但可使用定时器。定时器是进程的实值变量，其值随时间连续递减（除非显式赋值）。具体而言，若 $X_t$ 是定时器，其在时间 $t$ 的值记为 $X_t(t)$，若在 $t_1$ 到 $t_2$ 期间未被重新赋值，则 $X_t(t_1) - X_t(t_2) = t_2 - t_1$。 发送者的输入字用无限数组 $inp$ 建模，$p$ 只能访问其一部分，当 $p$ 从生成字的进程获取下一个字时，可访问的 $inp$ 部分会在高端扩展，此操作称为发送者接受一个字。接收者交付字的建模方式与之前不同，接收者通过“交付字”操作将字传递给消费进程。理想情况下，$inp$ 中的每个字应仅被交付一次且按正确顺序交付，但由于协议只能在有限时间内处理每个字，无法保证字在有限时间内一定被接收，因此协议允许报告丢失，即发送协议生成错误报告表明字可能丢失。协议需满足以下两个性质： - **无丢失**：$inp$ 中的每个字在 $p$ 接受该字后的有限时间内，要么由 $q$ 交付，要么由 $p$ 报告为“可能丢失”。 - **有序性**：$q$ 交付的字在 $inp$ 中按严格递增顺序排列。 #### 3. 协议呈现 ##### 3.1 连接管理 在该协议中，当之前没有连接存在，且发送者接受下一个字或接收者收到可交付的数据包时，连接将被打开。因此，在发送数据包之前无需交换控制消息，这使得该协议对于每次连接仅传输少量字的应用（小批量通信）较为高效。用谓词 $cs$（发送者）和 $cr$（接收者）表示连接是否打开，通常这不是显式的布尔变量，而是通过连接记录的存在来定义。进程通过搜索其打开连接列表中是否存在连接记录来测试连接是否打开。 发送者打开新连接时，从 0 开始对接受的字进行编号。$High$ 表示当前连接中已接受的字的数量，$Low$ 表示已收到确认的字的数量。理论上，发送者可发送序号范围从 $Low$ 到 $High - 1$ 的数据包，但有一个限制：发送者只能在接受字后的长度为 $U$ 的时间间隔内发送该字，为此为每个字 $inp[i]$ 关联一个定时器 $Ut[i]$，在接受字时将其设置为 $U$，只有当定时器值为正时才能传输该字。因此，发送者的发送窗口由 $Low$ 到 $High - 1$ 范围内且关联定时器为正的字组成。 协议发送的数据数据包包含一个位（序列起始位）、一个序号和一个字，为便于分析，每个数据包还携带一个剩余数据包生命周期字段，该字段在发送时始终为 $\mu$。确认数据包仅包含 $q$ 期望的下一个序号，同样为分析目的携带剩余数据包生命周期。 协议的变量定义如下： | 类型 | 变量 | 含义 | | ---- | ---- | ---- | | 网络常量 | $\mu$ | 最大数据包生命周期 | | 协议常量 | $U$ | 发送间隔长度 | | 协议常量 | $R$ | 接收者超时值（$R \geq U + \mu$） | | 协议常量 | $S$ | 发送者超时值（$S \geq R + 2\mu$） | | 发送者连接记录 | $Low$ | 当前连接中已确认的字 | | 发送者连接记录 | $High$ | 当前连接中已接受的字 | | 发送者连接记录 | $St$ | 连接定时器 | | 接收者连接记录 | $Exp$ | 下一个期望的序号 | | 接收者连接记录 | $Rt$ | 连接定时器 | | 通信子系统 | $M_q$ | 发往 $q$ 的数据数据包通道 | | 通信子系统 | $M_p$ | 发往 $p$ 的确认数据包通道 | | 辅助变量 | $B$ | 先前连接中的字的数量 | | 辅助变量 | $cr$ | 接收者端连接是否存在 | | 辅助变量 | $cs$ | 发送者端连接是否存在 | 发送者协议的具体算法如下： ```plaintext Ap: (* 接受下一个字 *) begin if not cs then begin (* 首先打开连接 *) create (St, High, Low); (* cs := true *) Low := High := 0; St := S Ut[B + High] := U; High := High + 1 end end Sp: (* 发送当前连接中的第 i 个字 *) { cs && Low <= i < High && Ut[B + i] > 0 } begin send ( data, (i = Low), i, inp[B + i], μ ); St := S end Rp: (* 接收确认消息 *) { cs && ( ack, i, p ) in Mp } begin receive ( ack, i, p ); Low := max (Low, i) end Ep: (* 生成可能丢失字的错误报告 *) { cs && Ut[B + Low] <= -2μ - R } begin error[B + Low] := true; Low := Low + 1 end Cp: (* 关闭连接 *) { cs && St < 0 && Low = High } begin B := B + High; delete (St, High, Low) (* cs := false *) end ``` 接收者协议的具体算法如下： ```plaintext Rq: (* 接收数据数据包 *) { ( data, s, i, w, p ) in Mq } begin receive ( data, s, i, w, p ); if cr then if i = Exp then begin Rt := R; Exp := i + 1; deliver w end else if s = true then begin create (Rt, Exp); (* cr := true *) Rt := R; Exp := i + 1; deliver w end end Sq: (* 发送确认消息 *) { cr } begin send ( ack, Exp, μ ) end (* 若 Rt 超时则关闭连接，见 Time 操作 *) ``` ##### 3.2 连接关闭 连接的关闭由定时器控制，发送者使用定时器 $St$，接收者使用定时器 $Rt$。由于每个字的发送间隔和数据包的有限生命周期，每个字在信道中存在的时间区间长度为 $\mu + U$（从接受字的时刻开始）。因此，接收者在收到字 $\mu + U$ 时间单位后可丢弃该字的相关信息，因为此后不会有重复数据包到达，从而避免重复交付。每次交付字时，将 $Rt$ 设置为 $R$（$R \geq U + \mu$），若在 $R$ 时间内交付下一个字，则刷新 $Rt$，否则关闭连接。发送者的定时器值 $S$ 满足 $S \geq R + 2\mu$，以确保在连接关闭时不会收到确认消息。每次发送数据包时，将 $St$ 设置为 $S$，只有当 $St < 0$ 且 $Low = High$ 时才能关闭连接。若此时还有未确认的字，必须先报告这些字，然后才能关闭连接。 起始位用于接收者在关闭连接时收到数据包的情况，以决定是否打开连接并交付数据包。发送者在所有先前的字都已确认或报告为可能丢失时，将该位设置为 true。当 $q$ 在已打开的连接中收到数据包时，只有当数据包的序号等于下一个期望的序号（存储在 $Exp$ 中）时，才会交付该字。 变量 $B$ 是辅助变量，仅用于协议的正确性证明。发送者在每个连接中从 0 开始对字编号，但为了区分不同连接中的字，在协议分析中对所有字进行连续递增编号。发送者索引为 $i$ 的字的“绝对”编号为 $B + i$，其中 $B$ 是 $p$ 在先前连接中接受的数据包总数。在协议实现中，$B$ 不被存储，发送者会“忘记”$inp[0 .. B - 1]$ 中的所有字。 通信子系统由两个多集表示：$M_p$ 用于存储发往 $p$ 的数据包，$M_q$ 用于存储发往 $q$ 的数据包。除了发送者和接收者的协议，系统还有额外的转换，代表信道故障和时间的推进： ```plaintext Loss: { m in M } (* M 可以是 Mp 或 Mq *) begin remove m from M end Dupl: { m in M } (* M 可以是 Mp 或 Mq *) begin insert m in M end Time: (* δ > 0 *) begin forall i do Ut[i] := Ut[i] - δ; St := St - δ; Rt := Rt - δ; if Rt <= 0 then delete (Rt, Exp); (* cr := false *) forall ( .. , p) in Mp, Mq do begin p := p - δ; if p <= 0 then remove packet end end ``` #### 4. 协议正确性证明 ###