抄訳 DEFNING LIVENESS(1985)

October 29, 2022

L.Lamportは、Proving the Correctness of Multiprocess Programsで、安全性と活性を導入し、並行プログラミングの正しさを議論した。 そこでは、安全性は、実行中に「よくないこと」が起きない性質であり、活性は「よいこと」が起きる性質である。 後に、Lamportは安全性を形式的に定義したが、活性には与えていない。 そこで、並行プログラムの実行を状態系列とみなし、活性を形式的な定義した。 プログラムの一部である任意の有限長系列\(\alpha\)について、\(\alpha\)に後続する無限長の系列を\(\beta\)とするとき、性質\(P\)をみたす連結\(\alpha\beta\)が存在し、また、そのときに限り、\(\alpha\)は\(P\)の活性がある。

\(S\)をプログラムの状態の集合、\(S^{\omega}\)を無限長、\(S^{*}\)を有限長の系列とする。 また、\(S^{\omega}\)の要素\(\sigma\)が性質\(P\)を満たすことを\(\sigma\vDash P\)とかく。 このとき活性の定義は

$$ \forall\alpha : \alpha \in S^{*}:(\exists \beta: \beta \in S^\omega : \alpha \beta \vDash P) $$ である。\(\beta\)は無限長であるため、「よいこと」が常におきるのではなく、いつか起きるという定義になっている。

なお、\(\sigma_i\)を\(\sigma\)の最初の\(i\)個の状態からなる系列とすると、以下をみたし、かつそのときのみ、\(P\)は安全性であると定義できる。

$$ \forall \sigma: \sigma \in S^\omega: \sigma \nvDash P \Rightarrow (\exists i: 0 \leq i:(\forall \beta : \beta \in S^\omega : \sigma_i \beta \nvDash P)) $$

論文へのリンク