【进程代数学习笔记】4：[CSP]进程间的通道通信,管道与活锁避免

本文主要是介绍【进程代数学习笔记】4：[CSP]进程间的通道通信,管道与活锁避免，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

1 记号

1.1 通道和数据

同系统分析与验证课上学的Channel system记号类似，CSP中用序偶$c.v$（参见笔记一的2.14）表示在通道$c$上传送数据$v$。则进程$P$能够在通道$c$上通信的数据记为：
α c ( P ) = { v ∣ c . v ∈ α P } \alpha c(P) = \{v \ | \ c.v \in \alpha P \} αc(P)={v ∣ c.v∈αP}

用$channel()$和$message()$分别表示取通道名和取数据：
$$\begin{gathered} channel(c.v)=c \\ message(c.v)=v \end{gathered}$$

1.2 数据上通道

一进程将数据$v\in \alpha c(P)$发送到通道$c$上，接下来执行$P$，记为：
$$(c!v\to P)=(c.v\to P)$$

1.3 从通道取数据

一进程从通道$c$取下一个数据$x$，并根据收到的$x$的不同决定接下来的执行$P(x)$，记为：
( c ? x → P ( x ) ) = ( y : { y ∣ c h a n n e l ( y ) = c } → P ( m e s s a g e ( y ) ) ) (c?x \to P(x)) = (y: \{y \ | \ channel(y) = c \} \to P(message(y)) \ ) (c?x→P(x))=(y:{y ∣ channel(y)=c}→P(message(y)) )

式中$y$表示通道$c$上传递$message(y)$的序偶，如$c.7$。

---

例如，拷贝一比特数据的进程$COPYBIT$，可理解成从$in$通道取 v ∈ { 0 , 1 } v \in \{0,1\} v∈{0,1}，再发送到$out$通道上：
$$COPYBIT=\mu X\cdot (in?x\to (out!x\to X))$$

其中 α i n ( C O P Y B I T ) = α o u t ( C O P Y B I T ) = { 0 , 1 } \alpha in(COPYBIT) = \alpha out (COPYBIT) = \{0,1\} αin(COPYBIT)=αout(COPYBIT)={0,1}。

1.4 进程间使用通道通信

这里要注意和系统分析课使用的记号不同，这里就是用普通的并发"$||$"记号，$P||Q$当$P$发送数据到通道$c$（即$c!v$），而$Q$从通道$c$上取数据（即$c?x$）时，两进程就会发送通信。例如发送的数据是7，即是说$P$执行的动作是$c!7$，$Q$推进的动作是$c?7\to Q(7)$。

总是要求通道两侧的进程在通道上传值的字母表一致，即$\alpha c(P)=\alpha c(Q)$，不妨记为$\alpha c$。

通道通信中的字母表是关于通道名称的字母表！

2 几个例子

在CSP里的通信模型中，进程的下标表达了进程状态的互递归关系，其指示的是进程收到的通道中的值（还未传出去的那些）。

2.1 数据处理单元

这个例子用于理解在引入通道通信后，进程如何表达数据处理单元。这里是直接将数据乘以2：
$$DOUBLE=\mu X\cdot (left?x\to right!(x+x)\to X)$$

2.2 序列拆分

从$left$通道一次性读入长度为80的数据，从$right$通道一次输出一个（队头）：
α l e f t = { s ∣ s ∈ α r i g h t ∗ ∧ # x = 80 } U N P A C K = P ⟨ ⟩ P ⟨ ⟩ = l e f t ? s → P s P ⟨ x ⟩ = r i g h t ! x → P ⟨ ⟩ P ⟨ x ⟩ ⌢ s = r i g h t ! x → P s \begin{aligned} \alpha left &= \{s \ | \ s\in \alpha right^* \wedge \#x = 80 \} \\ UNPACK &= P_{\langle \rangle} \\ \\ P_{\langle \rangle} & = left?s \to P_s \\ P_{\langle x \rangle} & = right!x \to P_{\langle \rangle} \\ P_{\langle x \rangle^\smallfrown s} & = right!x \to P_s \end{aligned} αleftUNPACKP⟨⟩​P⟨x⟩​P⟨x⟩⌢s​​={s ∣ s∈αright∗∧#x=80}=P⟨⟩​=left?s→Ps​=right!x→P⟨⟩​=right!x→Ps​​

2.3 序列合并

从$left$通道每次读入一个数据，到125个时从$right$通道一次性输出：
α r i g h t = { s ∣ s ∈ α l e f t ∗ ∧ # s = 125 } P A C K = P ⟨ ⟩ P s = r i g h t ! s → P ⟨ ⟩ i f # s = 125 P s = l e f t ? x → P s ⌢ ⟨ x ⟩ i f # s < 125 \begin{aligned} \alpha right & = \{s \ | \ s \in \alpha left^* \wedge \#s = 125 \} \\ PACK & = P_{\langle \rangle} \\ \\ P_s & = right!s \to P_{\langle \rangle} & if \ \#s=125 \\ P_s & = left?x \to P_{s^\smallfrown \langle x \rangle} & if \ \#s<125 \end{aligned} αrightPACKPs​Ps​​={s ∣ s∈αleft∗∧#s=125}=P⟨⟩​=right!s→P⟨⟩​=left?x→Ps⌢⟨x⟩​​if #s=125if #s<125​

2.4 子串替换

这个例子有点编译器的味道，就是把"$\ast \ast$“输出成”$\uparrow$"，其它都不变，显然要在输入了一个"$\ast$"时检查下一个输入：
α l e f t = α r i g h t − { " ↑ " } S Q U A S H = μ X ⋅ l e f t ? x → i f x ≠ " ∗ " t h e n ( r i g h t ! x → X ) e l s e l e f t ? y → i f y = " ∗ " t h e n ( r i g h t ! " ↑ " → X ) e l s e ( r i g h t ! " ∗ " → r i g h t ! y → X ) ) \begin{aligned} \alpha left & = \alpha right - \{"\uparrow"\} \\ SQUASH & = \mu X \cdot left?x \to \\ if \ x & \neq "*" \ then \ (right!x \to X) \\ else \ &left?y \to \\ & if \ y="*" \ then \ (right!"\uparrow" \to X) \\ & else \ (right!"*" \to right!y \to X)) \end{aligned} αleftSQUASHif xelse ​=αright−{"↑"}=μX⋅left?x→​="∗" then (right!x→X)left?y→if y="∗" then (right!"↑"→X)else (right!"∗"→right!y→X))​

2.4 可选输入

一个双输入管道，但每次只选其一，然后就原样输出的进程：
$$\begin{array}{rl}\alpha left1=& \alpha left2=\alpha right\\ MERGE=& (left1?x\to right!x\to MERGE\\ & |left2?x\to right!x\to MERGE)\end{array}$$

显然，输出可以是两个输入序列的任一Interleaving。

2.5 一位寄存器

总是可以读入一个数据将当前数据覆盖掉，或者输出寄存的数据而不会因输出导致丢失数据：
$$\begin{array}{rl}\alpha left& =\alpha right\\ VAR& =left?x\to VA{R}_x\\ VA{R}_x& =(left?y\to VA{R}_y|right!x\to VA{R}_x)\end{array}$$

2.6 多参数计算单元

从$up$通道读入prod，从$left$通道读入sum，计算$sum+v\times prod$的进程：
$$NODE(v)=\mu X\cdot (up?sum\to left?prod\to down!(sum+v\times prod)\to X)$$

2.7 无限容量的队列

注意2.7和2.8模拟栈和队列都是在用进程模拟，而不是在用通道模拟。通道本身就是一个队列，在CSP里忽视通道的容量。

读入元素放到队尾，出队时去除队头元素：
$$\begin{array}{rl}BUFFER& =P_{⟨⟩}\\ & \\ P_{⟨⟩}& =left?x\to P_{⟨x⟩}\\ P_{⟨x{⟩}^{⌢}s}& =(left?y\to P_{⟨x{⟩}^{⌢}{s}^{⌢}⟨y⟩}|right!x\to P_x)\end{array}$$

2.8 无限容量的栈

读入元素放到栈顶，出栈时去除栈顶元素：
$$\begin{array}{rl}STACK& =P_{⟨⟩}\\ & \\ P_{⟨⟩}& =left?x\to P_{⟨x⟩}\\ P_{⟨x{⟩}^{⌢}s}& =(left?y\to P_{⟨y{⟩}^{⌢}⟨x{⟩}^{⌢}s}|right!x\to P_x)\end{array}$$

3 通道满足规范(specification)

3.1 简述

定义迹$tr$中在有关通道$c$的所有动作的值$v$组成的迹：
$$tr\downarrow c=messag{e}^{\ast }(tr\upharpoonright \alpha c)$$

输入通道和输出通道的迹之间往往可以存在序关系（一方是另一方的前缀）：
$$tr\downarrow right\le tr\downarrow left$$

简写成$right\le left$。所以：
$$s{\le }^{n}t=(s\le t\wedge \#t\le \#s+n)$$
这表示，通道$s$（的trace）是通道$t$（的trace）的前缀，并且$t$（的trace）最多比$s$（的trace）长n。这可导出如下性质：

• $s{\le }^{0}t\equiv (s=t)$
  最多长0说明一样长，又是前缀说明它们的trace就是一样的。
• $s{\le }^{n}t\wedge t{\le }^{m}u\Rightarrow s{\le }^{n+m}u$
  这是由前缀的传递性和不等式的合并。
• $s\le t\equiv \exists n\cdot s{\le }^{n}t$
  前缀关系总是会有长度关系的界。

3.2 例子

在1.3中的$COPYBIT$满足：
$$COPYBITsatright{\le }^{1}left$$

右边总是左边的前缀，且左边比右边最多长1，仅当刚输入还没开始输出时取等号。

---

在2.1中的$DOUBLE$满足：
$$DOUBLEsatright{\le }^{1}doubl{e}^{\ast }(left)$$

这在本质上和上一个是一样的，式中"$doubl{e}^{\ast }()$"仅仅是一个将传入的trace中每个数字乘2的符号变换而已。

---

在2.2中的$UNPACK$满足：
$$UNPACKsatright{\le }^{80}⌢/left$$

其中$⌢/$后接一个序列，作用是将其中的所有元素连接成一个合乎规格的普通trace：
$$⌢/⟨s_0,s_1,...,s_{n-1}⟩=s_0^{⌢}{s}_1^{⌢}..{.}^{⌢}{s}_{n-1}$$

上面是课本中的写法，意思就是trace里包含trace，实际上在这个例子和下一个例子里都只包含一个$s_0$，这里$\#s_0=80$，下个例子里$\#s_0=125$。

---

在2.3中的$PACK$满足：
P A C K s a t ( ( ⌢ / r i g h t ≤ 125 l e f t ) ∧ ( # ∗ r i g h t ∈ { 125 } ∗ ) ) PACK \ sat \ (( \smallfrown / right \leq^{125} left) \wedge ( \#^* right \in \{125\}^*)) PACK sat ((⌢/right≤125left)∧(#∗right∈{125}∗))

4 通信(Communication)

4.1 简述

进程间可以依靠通道上发送和接受值来实现通信：

如上图中若$v=7$，则进程$Q$也就收到$x=7$，然后执行$Q(7)$。

• L1：$(c!v\to P)||(c?x\to Q(x))=c!v\to (P||Q(v))$
  传递的信息$v$决定后续动作。

• L2：$((c!v\to P)||(c?x\to Q(x)))\backslash C=(P||Q(v))\backslash C$
  这是将通道上的通讯动作屏蔽掉，其中通道动作集合 C = { c . v ∣ v ∈ α c } C = \{c.v \ | \ v\in \alpha c\} C={c.v ∣ v∈αc}。

4.2 例子

$$\begin{array}{rl}P& =(left?x\to mid!(x\times x)\to P)\\ Q& =(mid?y\to right!(173\times y)\to Q)\end{array}$$

其中，$P$和$Q$各自满足的规格：
$$\begin{array}{rl}P& sat(mid{\le }^{1}squar{e}^{\ast }(left))\\ Q& sat(right{\le }^{1}173\times mid)\end{array}$$

两进程并发，所有满足的规格要取合取：
$$(P||Q)sat(right{\le }^{1}173\times mid)\wedge (mid{\le }^{1}squar{e}^{\ast }(left))$$

从而：
$$right\le 173\times squar{e}^{\ast }(left)$$

5 管道(Pipes)

5.1 简述

管道是一系列进程的顺序组合，这些进程之间通信的通道被屏蔽掉，即外部无法看到管道内部的具体通信过程，如将4.1中两进程间的通信过程隐藏：

记为$P>>Q$，管道的字母表：
$$\begin{array}{rl}\alpha (P>>Q)& =\alpha left(P)\cup \alpha right(P)\end{array}$$

5.2 例子

通过组合不同的进程，可以构造出具有各式各样功能的管道。

• X1：$QUADRUPLE=DOUBLE>>DOUBLE$
  将输入数据放大四倍的管道。

• X2：$UNPACK>>PACK$
  80到125的序列长度转换器。

• X3：$UNPACK>>SQUASH>>PACK$
  类似于X2，只是还要在转换过程中将"$\ast \ast$“过滤为”$\uparrow$"。

• X4：$UNPACK>>BUFFER>>PACK$
  类似于X2，相当于加了一个缓冲区，使得管道的输入和输出可以异步工作。

• X5：$COPY>>UNPACK>>PACK>>COPY$
  注意，这里$COPY$是拷贝任意一个数据，不必是一个二进制位。这个管道类似于X4，相当于在左右添加一个容量为1的缓冲区，使得输入输出可以异步工作。

• X6：$COPY>>COPY$
  容量为2的缓冲区，最多在输出前预接受2个数据。

5.3 管道的操作规则

• L1：$P>>(Q>>R)=(P>>Q)>>R$
  管道满足结合律（因为最终总是要把内部全屏蔽完），但不满足交换律。

• L2：$(right!v\to P)>>(left?y\to Q(y))=P>>Q(y)$
  从$P$出和从$Q$进的动作在$P>>Q$中对外屏蔽，但这一动作会影响$Q$使其接下来执行$Q(v)$。

• L3：$(right!v\to P)>>(right!w\to Q)=right!w\to ((right!v\to P)>>Q)$
  从$P$出和从$Q$出的动作，其中前者（从$P$出）是管道内部的动作，要在内部执行。

• L4：$(left?x\to P(x))>>(left?y\to Q(y))=left?x\to (P(x)>>(left?y\to Q(y)))$
  从$P$进和从$Q$进的动作，其中后者（从$Q$进）是管道内部的动作，要在内部执行。

5.4 管道的活锁(Livelock)现象

活锁是比递归程序出现$STOP$更坏的情况，其根本原因是管道屏蔽了内部动作，如：
$$\begin{array}{rl}P& =(right!1\to P)\\ Q& =(left?x\to Q)\end{array}$$
进程$P$不断输出1，而进程$Q$不断接受输入，两者连成管道$(P>>Q)$后，从外部看来整个管道是静止的，其实内部在不停消耗计算资源。

这是一个最纯粹的活锁例子，这样的活锁现象会抢占正常工作的动作，如：
$$\begin{array}{rl}P& =(right!1\to P|left?x\to P1(x))\\ Q& =(left?x\to Q|right!1\to Q1)\end{array}$$

它们组成的管道$(P>>Q)$会出现$P$发送$Q$接收的白白消耗计算资源的情况，则正常工作的部分（$P$接收、$Q$发送）就被抢占了。

5.5 避免活锁(free of livelock)

如果进程$P$不能无限的输出（而不受输入限制），那么就称$P$是left-guarded的。其数学表达是：
$$\exists f\cdot Psat(\#right\le f(left))$$

其中，$\#right$是指到任何时刻为止输出的数据长度。而$f$是指一个函数，将到该时刻为止的输入映射到自然数集中。这是在要求任何时刻输出的数据长度都有一个上界，而这个上界取决于输入数据。例如"输入1个数据，随后输出10个该数据"这样的进程就是left-guarded，例如可以取到这样一个$f$：
$$f(left)=11\times \#left$$

从而总有$\#right\le f(left)$即$10t\le 11t$是成立的（$t$是经历的时刻）。

同理可以定义right-guarded，略。

• L1：如果任何用到$P$的递归进程在$P$左边都有guarded的输入，那么$P$是left-guared的。
• L2：如果$P$是left-guarded的，那么$(P>>Q)$不会发生活锁。
• L3：如果$Q$是right-guarded的，那么$(P>>Q)$不会发生活锁。

这篇关于【进程代数学习笔记】4：[CSP]进程间的通道通信,管道与活锁避免的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！

---