Concurrent

好蠢，Summary写到正面了，晕晕。抓紧时间还没忘掉总结一下。

Week1

这门课一开始的理念就把 Concurrent 和系统间通信连到了一起，并提出了 External 和 Internal 的概念，并认为内部状态外部不可见，以 $\tau$ 来表示，其他的就是正常 Transition。

主要就是把模型以 FSM 的形式表示出来。比较重要的感觉有一下几点

FSM 相关

这一块主要还是定义。

结构

$TS = (S,\to,s_0), \to\subseteq S\times Act\times S$

分别代表状态集，转移规则和起始状态。

操作的定义

$Act$： 动作集合
$Com$： 交流动作
$Int$： 内部转移

还有 $Act = Com\cup Int$

Post 操作

分为对元素和集合的操作， 2*2 共四种

$$Post(s,\alpha) = \{s'|s\mathop{\to}\limits^{\alpha} s'\}$$

$$Post(S,\alpha) = \bigcup_{s\in S}Post(s,\alpha)$$

$$Post(s,A) = \bigcup_{\alpha\in A}Post(s,\alpha)$$

$$Post(S,A) = \bigcup_{\alpha\in A}Post(S,\alpha)$$

Non-determinism

在这节课上，我们认为有两种 Non-determinism.

一种是内部的，另一种是外部的。例子如下：

stateDiagram-v2
    [*]--> Start
    Start--> End1 : a
    Start--> End2 : b

和生活结合就是一个手机，两个按钮

另一种是内部的：

stateDiagram-v2
[*]--> Start
    Start--> End1 : [a]
    Start--> End2 : [b]

和生活结合就是一个按钮，按下后是什么和内部状态相关。

还有一种是两不沾的，如：

stateDiagram-v2
    [*]--> Start
    Start--> End1 : [a]
    Start--> End2 : b

Reachability

就是定义。

$$Post^0(\{s\}) = s$$

$$Post^{n+1}(C) = Post(Post^n(C))$$

$$Reach(S) = \bigcup_{n\in\mathbb{N}}Post^n(S) \quad$$

根据定义， $s\in Reach(\{s\})$

$CSS$ 相关

$CSS_0$

这是自创的描述语言，语法如下

$S := 0| S + S | a.S \quad a\in Act$

+left associative
.right associative
prefix have higher priority

还有两个个语法扩展

$CSS_0^\omega$

这个是加上了递归语法。Reference Rule 如下：

$$\textbf{rec}\frac{P\mathop{\to}^\alpha P' \quad \Gamma(X)=P}{X\mathop{\to}\limits^{\alpha}P'}$$

$CSS$

加了一个“锁”来提供 sync。

语法是夹在了 $Act$ 上。 对于 $a\in Act$ , 我们规定 $a! , a?$ 分别为发射端和接收端。接收端接收到发射端信号才会进一步执行。图示如下：

stateDiagram-v2
    [*]--> Start
    Start--> Mid1 : a?
    Start--> Mid2 : a!
    Mid1--> End :a!
    Start-->End : τ
    Mid2--> End :a?

感觉这个实现方法有点阻塞的意思。

第一周内容大概就这么多，没写上的就是一些 Inference Rules， 准备复习的时候一起记。

Week3

等价关系

等价关系本身的定义是：把两个等价的 $P,Q$ 插到任意上下文里，出来的结果还是等价的。

从强到弱：Isomorphic bisimilar trace-equivalent

Id

完全相等，需

Isomorphic

这个最好判断，找 Mapping 就可以

Bisimilar

这个估计是考试证明的重点：

基本理念是模仿：这两个 CCS 表达能不能一步一步模仿对方？

理念是 Bisimilar 可以处理 Branching

首先，我们从玩游戏的角度来感性地证明一下：

首先，我们分为 Attacker 和 Defender。
然后每次 transit，攻防互换，看能不能这样一直走到最终状态。

如果这个游戏能玩下去，说明 bisimilar， 反之不行

形式化证明还是找 Pair。

先枚举出所有对应的 pair 的集合 $R$，再说明对于这个 $R$ 里的每一个元素，正着来反着来（写两遍）都满足 bisimilar 的定义。

将两边的点进行配对，使得所有关系里的点都满足 Bisimilar 的判定条件，同时不漏。
基本就是列举所有 mapping

Trace Equivalence

这个就是遍历所有路径，比较所有的 Trace

Week4

因为外部观测不到 $\tau$ transition，那么我们能把 $\tau$ transition 前后的状态合并吗？

当然不行，因为这样有可能把两个完全不同的东西整成 bisimilar 甚至 iso 的，而这与现实明显不符。

Weak Transition

为了描述这些情况，我们引入了 Weak Transition. 本质上就是两个状态间如果有任意多个 $\tau$ transition + 随便一个 transition $\alpha$ (可以为 $\tau$ ), 那么就称这个 transition 为 $\tau$ transition。

几个注意点

• 一个强 $\tau$ transition 也 implies 一个 Weak $\tau$ transition.
• 每个状态都有到自己的 Weak Transition
• 接上一点：如果要求 Observation Congruence 的话，那么必须要显式的 $\tau$ transition，阴式的不行。

Weak Bisimulation

定义

类似，对 Weak Transition 我们也可以定义 Bisimulation

对于左边，找 Transition 变更难了（因为得包含 $\tau$ ），但是右边变简单了。
因此，我们强化左边的条件为 Strong Transition，获得一个新的 Lemma。

这样就得到了一个更加简便的 Weak Bisimulation 判定方法。

一个🌰：

stateDiagram-v2
    Start1 --> Mid1 : a
    Mid1 --> Done1 : τ

    Start0 --> Done0 : a

    Start2 --> Mid2 : τ
    Mid2 --> Done2 : a

这三个东西事 Weak Bisimilar 的。

可以这么理解： 跟 $\tau$ 有关的都可以和到有真正 transit 前/后 最后一步。

同时 Weak 的定义也让攻击更加简单。因为你其实是可以留在一个状态的，这本身也是一个 $\tau$ Transition.
有了 Weak，在换边后就有了更多的选择。

性质

这个满足 reflexive， transitive，symmetric

但是不满足 trace preserving

因此我们引入 Weak Trace， 就是把 $\tau$ 省略掉的 Trace，这样我们就可以说

Weak bisimilar 保留了 trace， 还是 Weakly termination sensitive。

以及它不是 Congruent Relation

这就引出了下一个概念：

Observation Congruence

在 Weak Bisimilar 的基础上更进了一步，认为如果两边经过一个 trace 是 某个Weak Transition 转移后的状态 Weakly Bisimilar，那么这两个 LTS term Observation Congruence。

注意因为这里的 Trace 必须存在一个显式的 Transition。因此在 Weak 最小化的时候必须在第三部重建一些 $\tau$ 来维护 Observation Congruence。

这个东西满足了我们对等价关系的所有想象。

Weak Minimization

1. 先按正常的最小化流程，只考虑 Weak Transition （注意每个 state 有到自己的 $\tau$ transition）
2. 考察哪些 Transition 删除后还能通过 Weak Transition 重建出来。
3. 看看每个等价类里面有没有 $\tau$ transition, 如果有，那么加一个 $\tau$ 自环 （实际作用见上一部分）

$CCS_{vp}$

等价类已经定义好了，下一步就是让它变得有用

CCS without data is useless (or at most time, useless)
——Felix Freiberger

扩展语法的方式就是在 send/receive 操作后加 value.

一个🌰:

put?x, send!x, Sending[x]

几个点：

• 我们将 x 放在标点符号后面来区分操作名和数据
• 注意只有实例化的 transition 才在 $Act$ 里面。a?42 可以用 prefix， 但是 a?x 不行，得用 input。
• 同名变量我们选择 shadowing 的解释方法。 🌰：a?xb!xa?xb!x.0 - a?23 -> b!23a?xb!x.0

考察与 $CCS$ 的关系，给定 $\mathbb{V}$ finite， 那么通过给下标的方式，就可以 把 $CCS_{vp}$ 转为 $CCS$. 所以这两个东西其实本质一样，只是多了一层包装。

$CCS_{vp}^{\mathbb{Z}}$

进一步，我么给 $CCS$ 加上计算的能力。限定 $\mathbb{V} = \mathbb{Z}$，$AExp$ 为代数表达式， $BExp$ 为 Bool 表达式。

对于表达式，有 closed 的 概念。如果一个表达式所有的变量都被环境赋值了，那么它就是 Closed 的。
符号表示为：

$$e \Downarrow v$$

当 $e$ closed 为 true，反之为 false

注意 CCS term 的变量如果加括号，sematic 意义就会变，在 LTS 里面应该单建状态。

但是话又说回来，语法里定义 send 的时候规定后面跟的值只能是 Expr, 因此 a!x 和 a!(x) 是一个东西。

期中复习

这里记录的都是做题相关的信息。

Concurrent的定义

我们认为，一个分时进行的任务是 Concurrent。如果这些分时任务有重叠，那么就是 Parallel 的。感觉上 Concurrent是一个更弱的定义，包含 Parallel。

Concurrent Model 的约定

建模遵循以下原则：

1. 自动机样式 （State， Transition）。注意每个 LTS 都必须要有 starting state
2. 状态对于一个 Process 是内部的，无法被外部观测
3. Transition 是状态转移，都有一个 Action 名字
4. $Act = Int \cup Com$
5. 状态转移瞬间完成，时间只在 State 内流动。

进一步，关于时间，我们有以下 Core Assumptions:

• Concurrent processes 可以任意相对速度执行。
• 从时间角度，我们最多只考虑 Process 之间的相互顺序。

Labeled Transition System (LTS)

这个就是前面说的建模。类似自动机，定义在结构

Determinism 的定义

在 CCS 里，我们认为 state $s'$ determinism, iff $|Post(s')|\leq 1 \vee |Act(s')|\leq 1$.

注意这里和一般意义上的 determinism 的区别。

与之相关的还有 External/Internal Non-Determinism.

Internal 就是 automata 的 non-determinism 或者操作都被 [] 包装了。
External 就是 有多个操作。

这两个东西可以共存，也可以共不存。

各种 Equality 的判断

因为各种关系都 transitive，因此在大量判断时可以先两两判断，然后再找两个搭桥。

Guarded

Guarded 只保证：

1. Semantics well-defined
2. no immediate divergence

不保证整个 CCS 不 divergent。

反例：a.(X|X)

CCS 性质

整个 LTS 都是一开始就存在的。也就是说所有的状态一开始都是存在的。所以两个 Process 之间的区别其实是 initial state。

Least FP

对于 operational semantics， 我们取 Least FP，也就是最小满足 inference rule 的 relation。

Derivation Tree

只有由 CCS 生成的 LST 有 derivation tree。随便的一个 LST 不行。

哲学家吃饭

几个点：

1. CCS 里面没有编码左右结构。因此交换拿取的顺序其实并不会改变 deadlock 的结果。
2. Deadlock 在 Acquire 时发生，因此只改变 Release 也不会改变deadlock 的结果。
3. 如果允许在拿到锁以后回撤，那么 deadlock 一般都可以解决
4. 但是考虑大家都拿起放下，拿起放下，会无限循环 (Starve)
5. 进而我们得出 Deadlock free != Starvation free != fairness