并发系统的建模

迁移系统(Transition System, TS)
一个迁移系统是一个六元组\[TS=(S, Act, \rightarrow, I, AP, L),\]其中
S是一个状态集合；
Act是由动作组成的集合；
\(\rightarrow \subseteq S\times Act\times S\)是迁移关系，如果\((s,a,s')\in \rightarrow\), 我们简记为\(s\overset{a}{\rightarrow}s'.\)
\(I\subseteq\)是初始状态集合；
\(AP\)是原子命题构成的集合；
\(L:S\to 2^{AP}\)是标记函数。直观上看，\(L(s)(s\in S)\)表示恰好被状态s满足的那些原子命题。
如果\(S,ACT,AP\)都有限，则称TS是有限的。

我们用Post(s)和Pre(s)表示状态s的后继和前驱。迁移系统的终止状态定义为\(Post(s)=\emptyset\)的那些状态。
用迁移系统对软硬件系统建模的关键是未定性，通过交错为独立活动的并行执行建模。交错意味着未定地选择并行进程动作的执行顺序。但是，我们也常考虑一些确定性的迁移系统.
(1) 如果\(|I|\le 1, \forall s, a ,|Post(s,a)\le 1|.\) 称此TS是动作确定的。
(2) 如果\(|I|\le 1, \forall s, A\in 2^{AP}\)都有\(Post(s) \cap \{s'|L(s')=A\}|\le 1\), 称此TS是AP确定的。

迁移系统TS的一个执行片段\(\rho\)是指有限或无限序列\[\rho = s_0 a_1 s_1 a_2 s_2\cdots.\] 无限执行片段或以终止状态结束的片段称为极大执行片段。若\(s_0\in I,\)称为起始执行片段。TS的一个执行定义为起始执行极大片段。若存在一个执行包括状态s，称s是TS可达的状态，可达状态集记作Reach(TS).

程序图
有型变量集合Var上的程序图(Program Graph, PG)是六元组\[(Loc, Act, Effect, \hookrightarrow,Loc_0, g_0),\]其中
Loc是位置的集合，
Act是动作的集合，
Effect: \(Act\times Eval(Var)\to Eval(Var)\)是效果函数，
\(\hookrightarrow\subseteq Loc\times Cond(Var)\times Act\times Loc\) 是条件迁移关系，
\(Loc_0\subseteq Loc\)是初始位置，
\(g_0\in Cond(Var)\)是初始条件。

条件迁移关系\(l\overset{g:a}{\hookrightarrow}l'\)是\((l,g,a,l')\)的简写。g称为"守卫条件"(guard)，可以看做这一迁移触发的条件。当g=True时可以忽略不写。
位置\(l\in Loc\)处的行为取决于变量赋值\(\eta\). 对于\(\eta\vDash g\)的条件g，以及对应存在的条件迁移关系，l在其中做出未定选择。如果没有可行的迁移，则系统结束。
当一个迁移动作发生时，效果函数Effect调整各变量的赋值。

程序图可以解释为迁移系统，此时每个状态s视为\(\langle l,\eta\rangle\). 迁移关系将如下定义：\[\frac{l\overset{g:a}{\hookrightarrow}l'\land \eta\vDash g}{\langle l,\eta\rangle\overset{a} {\to} \langle l', Effect(a,\eta)\rangle}.\]

迁移系统的交错
设\(TS_i, TS_2\)是两个迁移系统。迁移系统\(TS_1||| TS_2\)定义为\[(S_1\times S_2, Act_1\cup Act_2, \rightarrow, I_1\times I_2, AP_1\cup AP_2, L)\]其中迁移关系包括两部分，第一部分由\[\frac{(s_1,a,s'_1)\in\rightarrow_1}{(\langle s_1,s_2\rangle, a, \langle s'_1, s_2\rangle)\in \rightarrow}\]生成，第二部分类似。而标记函数定义为\(L(\langle s_1, s_2\rangle) = L_1(s_1)\cup L_2(s_2)\).
迁移系统的交错可为异步并发建模，但不能解决共享变量等问题。

类似于迁移系统，我们可以定义程序图的交错。程序图\(PG_1|||PG_2\)的全局变量（共享变量）是\(Var_1\cap Var_2\). 在程序图的交错中，进程可以通过共享变量实现通信。
以Peterson互斥算法为例，两个进程可以通过访问或修改某个共享变量\(x\)实现通信，来确保两个进程不会同时进入关键节段中。

同步消息传递（握手）
在同步消息传递中，参与互动定的进程只能以同步的方式进行(握手). 也就是说，只有进程都同时参与互动时，进程才可以互动。
设有迁移系统\(TS_1,TS_2\)。握手动作的集合\(H\subseteq Act_1\cap Act_2\). 定义\(TS_1||_H TS_2\)的迁移关系如下：
(1) H中的动作必须同步执行, 即\[\frac{a\in H\land s_1\rightarrow^a_1 s'_1 \land s_2\rightarrow^a_2 s'_2}{(s_1,s_2)\to^a (s'_1,s'_2)}.\]
(2) 不在H中的动作按照交错定义。
Note：当\(H = Act_1\cap Act_2\)时，可以简写为\(TS_1||TS_2\); 当H为空集时，与交错\(TS_1|||TS_2\)相同。
算子\(||_H\)是可交换的。如果固定H，则算子\(||_H\)是结合的。
对于多个进程\(TS_1,TS_2,\cdots,TS_n\), 一般是两两之间通信，此时我们可以定义\(H_{ij}\subseteq Act_i\cap Act_j,\) 并且假定\(H_{ij}\cap Act_k=\emptyset.\)

通道系统
通道是一个先进先出的、可传递信息的缓冲区。通道系统广泛用于描述通信协议。
直观上，通道系统由n个进程\(P_1\sim P_n\)组成，每个\(P_i\)用通信动作扩展的程序图来描述。程序图的迁移要么是通常的条件迁移，要么是以下动作之一：
(1) \(c!v\) 沿通道c发送消息v
(2) \(c?x\) 从通道c接受消息，并将其值赋给变量x.
每个通道都有一个容量cap(c)（非负整数数或无穷）和定义域dom(c)。容量决定了缓冲区的最大数据量，当cap(c)=0时，通道相当于握手。

形式化地描述，设\(Chan\)是由通道组成的有限集合，令\[Comm = \{c!v, c?x|c\in Chan, v\in dom(c), x\in Var, dom(c)\subseteq dom(x)\}\]表示(通道)动作的集合。我们先扩展(Var, Chan)上的程序图PG的定义，与通常的流程图不同的是\[\hookrightarrow \subseteq Loc \times Cond(Var) \times (Act\cup Comm)\times Loc.\]然后，我们可以定义(Var, Chan)上的通道系统CS由\((Var_i,Chan)\)上的程序图\(PG_i\)组成，\(Var = \bigcup Var_i\), 通道系统\[CS = [PG_1 |PG_2|\cdots |PG_n].\]
迁移关系有两种，第一种是通常的条件迁移，另一种是通道条件迁移，条件guard满足时，若c非空可以执行\(c?x\)，若c未满可以执行\(c!x\).

    所属分类：Formal Methods     发表于2022-02-07