1 并发(concurrency)与死锁

1.1 例子

如课本P8的复杂贩卖机进程：
$$\begin{gathered} VMC=(in2p\to (large\to VMC|small\to out1p\to VMC) \\ |in1p\to (small\to VMC|in1p\to (large\to VMC|in1p\to STOP))) \end{gathered}$$
与下面这个愚蠢顾客的进程（在CSP中进程的环境可被描述成进程的形式）：
$$FOOLCUST=(in2p\to large\to FOOLCUST|in1p\to large\to FOOLCUST)$$
两者相并发，也就是具有该行为的顾客在使用该贩卖机的进程：
$$(VMC||FOOLCUST)=\mu X\cdot (in2p\to large\to X|in1p\to STOP)$$
这是因为，当$FOOLCUST$第一步选择$in2p$时，第一个$VMC$也要做此动作，两者同步执行，接下来$VMC$面临选择$large$或$small$，而$FOOLCUST$接下来要做$large$，那么两者继续向前同步执行，然后各自回到开头。

当$FOOLCUST$第一步选择$in1p$时，第一个$VMC$也要做此动作，两者同步执行，接下来$VMC$面临选择$small$或$in1p$，而$FOOLCUST$接下来要做$large$，那么两者在公共动作上存在分歧，无法继续执行，故进程进入$STOP$状态，此即发生了死锁（deadlock）。

1.2 性质

显然，并发程序的$traces$是其内所有并发程序的$traces$的交集。关于并发的更多性质在课本P50~51。仅分析其中几个最关键的性质。

假定有进程$P$和$Q$，其中$a$是$P$的私有动作，$b$是$Q$的私有动作，$c,d$是$P$和$Q$的公共动作，那么：

• L4A：$(c\to P)||(c\to Q)=c\to (P||Q)$
  这表示并发程序同步做同一动作$c$，接下来继续并发执行。

• L4B：$(c\to P)||(d\to Q)=STOPifc\ne d$
  这表示公共动作上出现分歧时，发生死锁，记为并发结束。

• L5A、L5B：$(a\to P)||(c\to Q)=a\to (P||(c\to Q)),(c\to P)||(b\to Q)=b\to ((c\to P)||Q)$
  这表示，一方要做私有动作，一方要做公共动作时，让私有动作的进程自己执行完私有动作。

• L6：$(a\to P)||(b\to Q)=(a\to (P||(b\to Q))|b\to ((a\to P)||Q))$
  这表示，双方都要做私有动作时，私有动作都要各自执行完，但任选一顺序执行。如上式右侧的选择符号$|$左边是$P$先执行私有动作$a$的情况，右边是$Q$先执行私有动作$b$的情况。

1.3 死锁解除(free from deadlock)

如在哲学家就餐问题中，如果每个哲学家拿起自己左边的筷子，那么所有哲学家都没法就餐，因为都处于要去拿右边的筷子的状态，但是该资源已经被占用了。

死锁解除可以通过在原来的进程上并发一些约束进程来实现。如在哲学家就餐问题中，只要引入$FOOT$进程，可以理解成引导哲学家进餐的侍者（footman），其动作就是让哲学家坐下/起身。这两个动作是每个哲学家自己就有的，所以将这个进程并发上去，也就变成了“当有哲学家希望坐下/起身，需要侍者允许它这样做时才行”，也就是两个进程在公共事件上要同步推进。
⋃i=04{i.sits down, i.gets up}U=⋃i=04{i.gets up}D=⋃i=04{i.sits down} \bigcup_{i=0}^4 \{i.sits \ down, \ i.gets \ up\} \\ U = \bigcup_{i=0}^4 \{i.gets \ up\} \\ D = \bigcup_{i=0}^4 \{i.sits \ down\} i=0⋃4​{i.sits down, i.gets up}U=i=0⋃4​{i.gets up}D=i=0⋃4​{i.sits down}
为了避免出现死锁，最多只允许桌上有4个哲学家即可，可以定义0~5一共5个相关的进程，来表示当前桌上有几个哲学家（将约束转换成进程的技巧）。所以$FOOT$进程的互递归定义如下：
FOOT0=(x:D→FOOT1)FOOTj=(x:D→FOOTj+1 ∣ y:U→FOOTj−1)     for j∈{1,2,3}FOOT4=(y:U→FOOT3) FOOT_0 = (x:D \to FOOT_1) \\ FOOT_j = (x:D \to FOOT_{j+1} \ | \ y:U \to FOOT_{j-1}) \ \ \ \ \ for \ j \in \{1,2,3\} \\ FOOT_4 = (y:U \to FOOT_3) FOOT0​=(x:D→FOOT1​)FOOTj​=(x:D→FOOTj+1​ ∣ y:U→FOOTj−1​)     for j∈{1,2,3}FOOT4​=(y:U→FOOT3​)
将其和原进程并发，即得到了解除死锁后的进程：
$$NEWCOLLEGE=(COLLEGE||FOO{T}_0)$$
无死锁的进程可以这样表达，在执行过任何trace中的动作后都无法进入$STOP$状态：
$$(NEWCOLLEGE/s)\ne STOPforalls\in traces(NEWCOLLEGE)$$

2 相关操作

2.1 并发进程的符号变换(change of symbol)

$f$是从原字母表$\alpha P$到新字母表$A$的映射：
$$f:\alpha P\to A$$
该映射作用于进程$P$时，即将其中所有字母映射到新的字母表上去：
$$\alpha f(P)=f(\alpha P)$$
对变换后的进程取迹集合，相当于对原进程的所有迹求上节2.9的迹上符号变换：
traces(f(P))={f∗(s) ∣ s∈traces(P)}traces(f(P))=\{f^*(s) \ | \ s \in traces(P)\}traces(f(P))={f∗(s) ∣ s∈traces(P)}

进程的符号变换可用于模型修改，如需要修改贩卖机的商品价格，就可以用符号变换：
$$\begin{gathered} f(in2p)=in10p \\ f(in1p)=in5p \\ ... \end{gathered}$$

进程的符号变换可用于模型结合，如要连接两个in-out的$COPYBIT$进程，使其能够按序工作，即从第一个$COPYBIT$输入，传给第二个$COPYBIT$最后再输出，可用符号变换将前者的输出和后者的输入连接起来：
$$\begin{gathered} f(out.0)=g(in.0)=mid.0 \\ f(out.1)=g(in.1)=mid.1 \\ ... \end{gathered}$$
最后，将两者并发就可得到新模型：
$$CHAIN2=f(COPYBIT)||g(COPYBIT)$$

2.2 并发进程打标签(process labelling)

进程打标签用于区分多个行为一致的进程，如两台$VMS$一左一右一起提供服务，即：
$$(left:VMS||right:VMS)$$
如果不对其打标签，那么两个行为一致的进程，其所有动作都是共同动作，即：
$$VMS||VMS=VMS$$
这是没有意义的。

进程打标签$l:P=f_l(P)$，是对其中的所有动作打标签：
$$f_l(x)=l.xforallxin\alpha P$$

2.3 并发进程满足规范(specification)

这里的规范可见上节2.16迹与产品规格的定义，使用符号$sat$连接进程和规范。并发进程满足规范主要有以下两个性质：

• L1：$PsatS(tr)\wedge QsatT(tr)=>(P||Q)sat(S(tr\upharpoonright \alpha P)\wedge T(tr\upharpoonright \alpha Q))$
  注意，其中$=>$左侧的$tr$是$P$和$Q$各自的trace，而右侧的$tr$是$(P||Q)$的trace。

• L2：如果$P$和$Q$都不会终止并且至多有一个公共事件，那么$(P||Q)$不会终止。
  试想如果有两个以上的公共事件，那么$P$和$Q$各自拿出不同的公共事件要求并发时，就会死锁。而只有一个公共事件时便不会有这种情况。