Proving the Correctness of Multiprocess Programs (1977)

March 25, 2023

マルチプロセスプログラムの正しさを証明するための公理を提案する。正しさの条件は、プログラムが安全性と活性を満たすことである。安全はプログラムが特定の状態になりえないことを、活性はプログラムが特定の状態に必ず到達することを意味する。たとえば、キューにメッセージを配信するproducerとキューから取り出すconsumerがあるとする。このとき、容量以上のメッセージがキューに蓄積しない性質が安全性に、キューが満杯時にconsumerがメッセージを消費する性質が活性になりえる。プログラム、安全性、活性を形式化し、安全性と活性を証明することで、プログラムの正しさを示す。

形式化したプログラムのプロセスはフローチャートで表現できる。グラフのノードは、下の図のAssignment NodeとDecision Nodeの2種類に分かれる。 Assignment Nodeは変数の更新、Decision Nodeは分岐に対応する。 Assignment Nodeの出力先のノードはつねに1つ、Decision Nodeの出力先は2つである。 $x$をプログラム中の変数集合、$X$は$x$がとりえる値の集合とすると$f$は$X$から$X$への写像である。 $p$の始域は$X$, 終域は$\{\textit{true},\textit{false}\} $である。 flowchart

プロセスが実行中の矢印を示すための印をトークンといい、Asseriton（表明）は、トークンと$x$をもとに真偽値を返す関数である。プログラムが実行中、つねに表明が真であれば、表明はinvariant（不変）である。より形式的には、$N$個のプロセスがあり、プロセス$\prod_k$の矢印の集合を$\Gamma_k$, $\Gamma\equiv\Gamma_1\times \cdots\times\Gamma_N$とすると、表明$A$は始域が$X\times\Gamma$で、終域が真偽値の関数である。表明は、$\forall(x,\gamma)\in X \times \Gamma: A(x,\gamma)=\textit{true}$がなりたつので、定理とみなすことができる。定理$A$が証明可能であることを$\vdash [A]$, $A$が不変であることを$\models[A]$と書く。

Interpretation（解釈）は各矢印に表明の適用することである。表明が真になる位置にトークンがある状態をlegitimateといい、プログラムが常にlegitimateであれば、解釈は不変である。 legitimateな状態で任意のステップを実行してもlegitimateな状態に移行するとき、interpretationはconsistent（一貫）であるという。

表明$\pi_k=\alpha$は、解釈が真になる必要十分条件がプロセス$\prod_k$の矢印$\alpha$にトークンがあることを意味する。 $\prod_k$-assertion $A_k$は、$\prod_k$のトークンの位置に結果が依存しないassertionである。 $I_k^\alpha$は、$\prod_k$-assertionを、$\prod_k$のトークンが$\alpha$にある状態に適用する解釈である。

安全性は表明についての帰納法で証明できる。以上の定義をもとに、以下の2つを公理として定義する。

任意の表明 A, Bについて $$ \begin{align} &\text{if} \vdash [A]\text{, then}\models[A].\\ &\text{if} \models [A]\text{ and}\models[A \supset B]\text{, then}\models [B]. \end{align} $$ である。

また、解釈$I$が不変であれば、任意の$k$と$\alpha\in\Gamma_k$について $$ \models[(\pi_k=\alpha)\supset I^{\alpha}_{k}] $$ である。

$I_k$がgeneralized interpretationであるとは、$\vdash[_oI^\alpha_k\supset_iI^\alpha_k]$である入力の表明$\textit{input} \prod_k\textit{-assertion}\ _iI_{k}^{\alpha}$と出力の表明$\textit{output} \prod_k\textit{-assertion}\ _oI^\alpha_k$を各$a\in\Gamma_k$に適用することを意味する。

legitimateな実行系列によって表明$A$が真である状態に到達したら後に$B$が成立する関係を$A\leadsto B$と書く。表明$A$と$B$があり、$I$をgeneralized interpretation $I_k$からなる解釈とする。

このとき活性の証明のための2つのうち公理1は、

$\models [\sim B]$と仮定すると $$ \begin{align} &\models [A \supset \wedge\{(\pi=\alpha)\supset _iI^\alpha_k: \text{all } k, \text{and all }\alpha\in\Gamma_k\}]\\ &I \text{ is consistent} \end{align} $$ を証明でき、$\{\alpha: _oI^\alpha_k\equiv \textit{false}\}$がinevitable setであれば、$A\leadsto B$である。

また、公理2は、$\leadsto$は推移的閉包であり、$\mathcal{D}$が表明の有限集合で、$A\in \mathcal{D}$であれば$\vee\mathcal{D}\leadsto B$が成立することである。

論文のリンク

雑記

非形式的に、安全性と活性は、特定の状態にならない、特定の状態にいずれ到達すると説明されている。しかし、安全性と活性の形式的な定義は論文中にない。安全性は、Distributed Systemsで、活性はDEFINING LIVENESSで後に形式的な定義が提案された。 DEFINING LIVENESSにも安全性の定義があるが、Distributed Systemsの定義とことなる。また、なぜ安全性と活性を満たせばプログラムが正しいと言えるのか議論されていない。以上の理由と、プログラムの性質は安全性と活性だけではないことから、状態を仮定した帰納法でプログラムの性質を証明する形式的な手法を提案した論文とみなすのがよい。