合同与会话类型配对及COWS对SOC应用的规范与分析

### 合同与会话类型配对及 COWS 对 SOC 应用的规范与分析 #### 合同与会话类型的定理及讨论 在合同与会话类型的研究中，有一个重要的定理： - **定理 5**：$K[\rho] ⊣I[\sigma]$ 当且仅当 $S I[\sigma] ≤dual(C K[\rho])$。 - **证明（仅当部分）**：设 $R$ 是满足特定条件的最小关系。若 $K[\rho] ⊣I[\sigma]$ 且 $\rho$ 和 $\sigma$ 强收敛，则 $S I[\sigma] R dual(C K[\rho])$ 以及 $S nf(\sigma)_{K\{e\}} R dual(C nf(\rho)_{K\{e\}})$。要证明 $R$ 是共归纳子类型，分两种情况： - 当 $S = S I[\sigma]$，$T = dual(C K[\rho])$ 且 $K[\rho] ⊣I[\sigma]$ 时，$S = &⟨H : S nf(\sigma)_H H⊆I⟩$，$T = &⟨ K \ {e} : dual(C nf(\rho)_{K\{e\}})⟩$。由 $K \ {e} ⊆I$ 可知，$T$ 最顶层分支的标签也会出现在 $S$ 的最顶层标签中。根据 $R$ 的定义，$S nf(\sigma)_H R dual(C nf(\rho)_{K\{e\}})$ 是显然的。 - 当 $S = S nf(\sigma)_K$，$T = dual(C nf(\rho)_K)$ 且 $(K ∪{e})[\rho] ⊣I[\sigma]$ 时，设 $nf(\sigma) = \sum_{R∈A (\sigma)} \sum_{\alpha∈R} \alpha.\sigma_{\alpha}$ 和 $nf(\rho) = \sum_{R∈A (\rho)} \sum_{\alpha∈R} \alpha.\rho_{\alpha}$。则 $S = ⊕⟨ R ∩K : &⟨/0 : end; {α} : S nf(\sigma_{\alpha})_K \alpha∈R∩K⟩_{R∈A (\sigma)}⟩$，$T = ⊕⟨S : &⟨/0 : end; {α} : dual(C nf(\rho_{\alpha})_K) R∈A (\rho),\alpha∈S∩R⟩_{S⊆K,S⋊⋉A (\rho)}⟩$。设 $R ∈A (\sigma)$ 是服务的就绪集，$R ∩K = R ∩K ⊆K$。根据 ⋊⋉ 的定义，$R ∩K ⋊⋉A (\rho)$ 当且仅当对于每个 $R′ ∈A (\rho)$，要么 $e ∈R′$ 要么 $R ∩K ∩R′ ̸= /0$。因为 $R′ ⊆K$，所以 $R ∩K ∩R′ = R ∩R′$。因此，$R ∩K ⋊⋉A (\rho)$ 是假设 $(K ∪{e})[\rho] ⊣I[\sigma]$ 的直接结果。而且，从相同假设以及 $nf(\rho) \stackrel{\alpha}{=⇒}$ 和 $nf(\sigma) \stackrel{\alpha}{=⇒}$ 可以推出 $(K∪{e})[\rho_{\alpha}] ⊣I[\sigma_{\alpha}]$，根据 $R$ 的定义，可得 $S nf(\sigma_{\alpha})_K R dual(C nf(\rho_{\alpha})_K)$。 - **证明（如果部分）**：根据编码的定义，这部分是显然的，细节留给读者。 通过结合定理 5 和命题 3(3)，可以得到一个有趣的对偶结果：$dual(S I[\sigma])$ 是与 $S I[\sigma]$ 成功交互的主要客户端类型。 - **推论 1**：$K[\rho] ⊣I[\sigma]$ 当且仅当 $C K[\rho] ≤dual(S I[\sigma])$。 在会话类型到合同的编码方面，这种编码简单且几乎关于操作是同态的。唯一需要注意的操作是分支操作，需要在生成的合同中为会话类型中未提及的标签添加额外的 $\ell.\Omega$ 子项。这表明会话中的进程只能执行由伙伴进程类型明确允许的操作。也就是说，会话类型描述的通信中，在任何时候，两个交互方中恰好有一方拥有控制权，并且不会发生握手。有趣的是，将 $\Omega$ 解释为进程的灾难性状态，并考虑一种稍弱的子合同关系“安全必须”，有 $\alpha.\Omega ⪯0$，这意味着在实践中，操作 $\alpha$ 是不能保证的。 而合同到会话类型的编码会使编码后的合同呈指数级增长。这表明合同比会话类型更抽象，能够表达更复杂的同步场景。部分额外的表达能力来自于运算符 $+$ 和 $\oplus$，它们可以自由地组合任意行为。例如，$\{a,b\}[a ⊕b]$ 的编码可以明确通知客户端是只有 $a$ 可用，还是只有 $b$ 可用，或者两者都可用。但如果服务是由可能分布式的进程组成（如服务编排），可能无法向客户端提供此类信息。 合同和会话类型之间存在严格的对应关系，在双方对通信协议提供集中控制的二元交互中，它们可以互换使用。合同的优势在于，除了会话之外，它还可以描述任意进程。例如，进程 $a | b$ 可以看作是两个不相关的会话，类型分别为 $\oplus⟨a : end⟩$ 和 $\oplus⟨b : end⟩$，而整个进程可以根据以下行为之一进行类型化： - $\Omega$ - $a.\Omega + b.\Omega$ - $a.b + b.\Omega$ - $a.\Omega + b.a$ - $a.b + b.a$ 这些行为代表了对进程行为的常规且越来越精确的近似。 #### COWS 对 SOC 应用的规范与分析 近年来，随着电子商务、电子学习、电子政务等新兴模式的成功，万维网逐渐向支持自动化使用的面向服务计算（SOC）架构发展。SOC 倡导使用松散耦合的“服务”，这些服务是自主、平台独立的计算实体，可以被描述