\( \def\ldef{≜} \) \( \def\globally{□} \) \( \def\eventually{◇} \) \( \def\openleftarrowplus{\overset{+}{⇾}} \) \( \def\equalv{⫤} \)

PlusCal: 証明アプローチ

2021年4月8日 TLC2 #PlusCal #TLA+

概要

このページでは PlusCal を使って記述したシステムが正しいことをどのように証明するかについて説明する。サンプルを実行するための環境セットアップは環境設定と検証の実行を参照。

概要
TLA⁺ は何を証明するのか?
Safety 特性
Liveness 特性
例: 信号機と歩行者

TLA⁺ は何を証明するのか?

一般的なプログラミング言語のアサーションが「ある時点での正しさ」のみを証明していたのに対し、TLA+ ではこれを時相論理で拡張することによって「正しい状態が継続すること」や「過去/現在/未来に正しい状態となった/なること」といった条件設定を可能にしている。つまり並行システムにおける正しさ (correctness) である Safety と Liveness の条件を制約として記述することができる。

Safety: なにか悪いことが決して起きないこと。例えば車用の信号と歩行者用の信号が同時に青になったり、銀行口座の残高がマイナスになるようなことが一瞬でも存在しないこと。
Liveness: なにか良いことがいつか起きること。例えば歩行者はいつかは横断歩道を渡れるし、送金はいつか相手の口座に振り込まれること。

TLA+ はシステムを有限状態機械とみなし、システムが取りうるすべての状態遷移を探索して Safety 特性と Liveness 特性が満たされていることを検査する。ここで、システム状態は状態変数だけではなくマルチプロセス下での各プロセスの進行状況も状態の組み合わせとして探索する。したがってレースコンディションのような問題も検出することができる。

TLA+ では Safety 特性の「決して」や Livnness 特性の「いつか」を表現するために時相論理 (temporal logic) の単項演算子 \(\globally P\) (globally; 常に \(P\) が成り立つ) と \(\eventually P\) (eventually; いつか \(P\) が成り立つ) を使用することができる。

Safety 特性

TLA+ または PlusCal では、時相論理演算子 \(\globally\) を用いた特性を定義してモデルファイルにその名前を指定し検査を実行することで Safety を検査することができる。考え方は一般的なプログラミングのアサーションを恒常的な条件に置き換えるだけであるためそれほど難しくはないだろう。

時相論理演算子 \(\globally\) を使う以外にも Invariant という制約を設置することができる。この条件も恒常的に検査されるため \(\globally\) との棲み分けが曖昧だが、個人的には TLA+ の変数は型制約がないことから、特定の変数の型制約の代用として Invariant を使用する方針をとっている。

Safety に関する制約としては一般的なテストフレームワークと同等のアサーションも使用することができる。前述の通りアサーション機能は「この時点で」を表す時相論理の一種とみなすことができる。

Liveness 特性

Liveness 特性の検査は Safety と同様に時相理論演算子 \(\eventually\) を使った特性を定義しモデルファイルで指定する。ただし、Liveness の検査のためにはスタッターリングと公平性を理解する必要がある。

スタッターリング

スタッターリング (stuttering) とは、実行可能なステップがあるにもかかわらずどのステップも進行しない動作である。有限回数のスタッターリングであれば Liveness 特性に影響することはないが、TLA+ では無限回のスタッターリングを許可している。つまり、最悪ケースとしてあるプロセスが特定のステップで無限にスタッターリングを繰り返し処理が全く進行しないケースが発生する。

有限時間内に終わるスタッターリングは、あるプロセスが大幅に遅れてシステムに復帰する Crash-Recovery 障害を再現しているとみなすことができる。ただし TLA+ ではステップの進行状況の組み合わせで既に Crash-Recovery を再現しているため、この動作は特に考慮には値しない。一方で無限に続くスタッターリングは、あるプロセスが任意の位置で応答しなくなりシステムに復帰しない Crash-Stop 障害を再現していると見なすことができる。

したがって、ラフな言い方だが TLA+ の文脈でスタッターリングするという表現は暗にそのプロセスで Crash-Stop 障害が起きることを想定しているとみなしても良い。

公平性特性

スタッターリングによって Crash-Stop を再現できるとはいえ、システムを構成するすべてのプロセスが Crash-Stop を起こすケースが存在するのであれば Liveness の検査は必ず失敗して意味をなさない。このため TLA+ では「ステップが有限時間内に進行する」という保証、つまり無限にスタッターリングしないことを保証するための公平性 (fairness) を指定することができる。

言い換えると公平性特性を付与されたプロセス (またはアルゴリズム全体や個別のステップ) はそのシステム設計において Crash-Stop 障害を想定しないことを示唆している。したがって公平性特性を付与してよいのはモデル検査で対象とするシステムを構成するプロセス、つまりプロセスの一つでも Crash-Stop したらそもそもサービスや機能を続行することができないような、システムの主旨たるプロセスに限られる。Crash-Stop 障害を想定する必要のある外部のサブシステム役となるプロセスには公平性特性を付与してはならない。

ステップが進行可能な条件が継続して続くのであればいつか進行する公平性を弱い公平性 (weak fairness)、進行可能と進行不可能が断続的に繰り返されたとしてもいつか進行する公平性を強い公平性 (strong fairness) と呼ぶ。例えばセマフォのように一時的に進行可能となったとしても先に別のプロセスが進行してしまい再び進行不可能になることを繰り返す状況では、弱い公平性では進行可能な状況をすべてスタッターリングで見逃してしまう可能性があるため進行できない経路が存在する。

公平性を指定する fair (弱い公平性) または fair+ (強い公平性) キーワードは algorithm の前か process の前に付与することができる。また Step:+ のように個別のステップのラベルのあとに + または - を付加してそのステップのみ公平性を変更することもできる。

キーワード	公平性	効果
(指定なし)	unfairness	制御対象のステップが進行可能だったとしても、永遠にスタッターリングを繰り返して進行しない可能性がある (任意の位置で Crash-Stop する)。
`fair`	weak fairness	制御対象のステップが実行可能であり続ける限り、いつかはそのステップが実行される。
`fair+`	strong fairness	制御対象のステップが断続的に実行可能であれば、いつかはそのステップが実行される。断続的とは、実行可能となったあとに実行可能でなくなり再び実行可能になることを繰り返すこと。

終了の検査

アルゴリズムが終了するかの検査は Liveness 特性の一種である。一般には Crash-Stop を想定しないすべてのプロセスが "いつかは" 最終的なステップまたは状態に到達することを検査すれば良い。

PlasCal には終了検査の簡易的な方法として -termination オプションがあり、それを使用すると Termination という特性が有効化される。\[ {\it Termination} \ldef \left\{ \begin{array}{ll} \forall {\it self} \in {\it ProcSet}: \eventually {\it pc}[{\it self}] = {\tt "Done"} & \ \ \mbox{for multiprocess} \\ \eventually {\it pc} = {\tt "Done"} & \ \ \mbox{for uniprocess} \end{array} \right. \] ただし、この方法はすべてのプロセスが "Done" ステップに到達する必要があるため、すべてのプロセスが fair であることを前提としている。抽象化された並行システム設計においては必ずしもこのように終了を定義する必要はない。

以下の例は -termination オプションを使用して livelock (無限ループ) による非終了を検出している。アルゴリズムに 2 つ以上のステップが存在しないと内部的な状態変数 pc が作成されず Termination 定義が見つからないというエラーとなることに注意。

PlusCal options (-termination)
---- MODULE Termination ----
(*--fair algorithm Termination
variables state = TRUE;
begin
  Loop:
    while TRUE do
      state := ~state;
    end while;
  Finish:
    skip;
end algorithm; *)
====

SPECIFICATION Spec
PROPERTY Termination
\* Add statements after this line.

例: 信号機と歩行者

Safety 特性と Liveness 特性を実装するために、Fig 1 に示すような歩行者、歩行者用信号、自動車用信号の 3 つのプロセスで構成されるシステムを考えよう。

歩行者 (Pedestrian) は歩行者用信号 (PedestriansSignal) が青のときにしか道路を渡ることができない。
歩行者用信号は自動車用信号 (DriversSignal) によって制御されているが、それぞれは独立したサブシステムである。
Safety 特性: 歩行者用信号と自動車用信号が同時に青になることはない。
Liveness 特性: 歩行者はいつか道路を渡ることができる。

この Mutex に似たシステムは PlusCal で以下のようなモデルとして表すことができる。

Fig 1. 歩行者、歩行者用信号、自動車用信号の 3 プロセスで構成されるシステム。

---- MODULE Crosswalk ----
EXTENDS Integers, TLC
(* --algorithm Crosswalk
variables
  pedestrians_signal \in { "red", "green" };
  drivers_signal = IF pedestrians_signal = "red" THEN "green" ELSE "red";
  went_through = FALSE;
  request_for_pedestrians_signal = "";

define
  BothSignalsDontTurnGreenAtTheSameTime ==
    [](~(drivers_signal = "green" /\ pedestrians_signal = "green"))
  APedestrianCrossesTheIntersection == <>went_through
end define;

fair+ process Pedestrian = "Pedestrian"
begin
  Wait:
    await pedestrians_signal = "green";
  Passed:
    went_through := TRUE;
end process;

fair process DriversSignal = "DriversSignal"
begin
  Switch:
    while TRUE do
      await request_for_pedestrians_signal = "";
      if drivers_signal = "green" then
        assert pedestrians_signal = "red";
        drivers_signal := "red";
        request_for_pedestrians_signal := "green";
      elsif pedestrians_signal = "green" then
        assert drivers_signal = "red";
        request_for_pedestrians_signal := "red";
      else
        assert drivers_signal = "red" /\ pedestrians_signal = "red";
        drivers_signal := "green";
      end if;
    end while;
end process;

fair process PedestriansSignal = "PedestriansSignal"
begin
  WaitRequest:
    while TRUE do
      Flip:
        await request_for_pedestrians_signal /= "";
        pedestrians_signal := request_for_pedestrians_signal;
        request_for_pedestrians_signal := "";
    end while;
end process;

end algorithm; *)
====

SPECIFICATION Spec
\* Add statements after this line.
PROPERTIES
  BothSignalsDontTurnGreenAtTheSameTime
  APedestrianCrossesTheIntersection

歩行者、歩行者用信号、自動車用信号のいずれか 1 つでも Crash-Stop すればシステムの Liveness 特性が損なわれることは自明であり必ず失敗して検査の意味をなさないことから、この検査では 3 つすべてのプロセスが Crash-Stop しないことを前提とする (つまり 3 つのプロセスに公平性特性 fair を付与する)。

歩行者

Pedestrian プロセスは歩行者用信号 pedestrians_signal が "green" となっているときに進行し went_through フラグを立てて終了する。歩行者用信号は青と赤を繰り返すため、信号待ちの await でスタッターリングしないためには強い公平性 fair+ が必要である。

歩行者用信号

PedestriansSignal プロセスはプロセス間通信用の変数 request_for_pedestrians_signal に設定されている色を点灯する。歩行者用信号は終了しなくても良い。

自動車用信号

DriversSignal プロセスは自動車用信号と歩行者用信号が同時に青にならないように注意深く制御を行っているため少し複雑である。歩行者用信号への要求キュー request_for_pedestrians_signal が空のときに制御を有効化し、以下のような挙動を行う:

自動車用信号が青であれば、自動車用信号を赤に設定して歩行者用信号を青にするように要求する。
自動車用信号が赤で歩行者用信号が青であれば、歩行者用信号を赤にするように要求する。
自動車用信号と歩行者用信号が共に赤であれば、自動車用信号を青にする。

ここでは想定している点灯を保証するためのアサーションも設置している。自動車用信号は終了しなくても良い。

Safety および Liveness 特性の検査はそれぞれ define の BothSignalsDontTurnGreenAtTheSameTime と APedestrianCrossesTheIntersection で時相論理演算子付きで定義し、モデルファイル中の PROPERETIES に指定している。

このモデルは Fig 2 のように正常終了する。この例にいくつかの "間違った" 修正を行って Safety や Liveness 特性がどのように違反するかを確認しよう。

歩行者用信号の故障

信号プロセスに公平性が欠落すると何が起きるだろうか? 歩行者用信号から fair を除去して実行してみよう。

\* process PedestriansSignal = "PedestriansSignal"
process PedestriansSignal = "PedestriansSignal"

TLA+ において公平性特性を持たないプロセスは任意のステップでスタッターリング (故障停止) を起こすようになる。歩行者用信号が赤を点灯している状態で故障停止すると歩行者は永遠に道路を渡れなくなり Liveness 特性に違反することが予想される。またこの例では自動車用信号も要求キューが空になってから次の動作を行うため、自動車用信号を含むシステム全体が進行しなくなることになる (ただし Safety 特性が満たされた状態で停止するはずである)。

実際 PedestriansSignal から fair 属性を削除して検査を行うと Fig 3 のようにスタッターリングによる時相特性違反のエラーが報告される。

歩行者の青信号見逃し

歩行者に付与している強い公平性を弱い公平性に替えると何が起きるかについて考えてみよう。

\* fair+ process Pedestrian = "Pedestrian"
fair process Pedestrian = "Pedestrian"

TLA+ の強い公平性はステップが有効化/無効化 (つまり進行可能/不可能) を繰り返していたとしても有限時間内の進行を保証する。一方で弱い公平性はステップが継続して有効化されているときのみ進行を保証する。この例では歩行者用信号は青と赤を繰り返していることから Wait ステップは await によって有効化/無効化を繰り返している。したがって歩行者プロセスを進行させるためには強い公平性 fair+ が必要である。

歩行者プロセスを弱い公平性に変更すると、最悪ケースとして青信号を無限に繰り返して見逃してしまうことで永遠に道路を渡ることができない ─ つまり Liveness 特性に違反することが予想される (ただし Safety 特性は継続して満たしているはずである)。

Pedestrian プロセスを弱い公平性 fair に変更して検査を行うと Fig 4 のように時相特性違反のエラーが報告される。

歩行者用と自動車用の信号を青にする

この例では独立して動作する歩行者用信号と自動車用信号のサブシステムが同時に青にならないように実装しているが、非同期を考慮しない間違った修正を加えてみよう。

if drivers_signal = "green" then
  drivers_signal := "red";
  request_for_pedestrians_signal := "green";
else
  request_for_pedestrians_signal := "red";
  drivers_signal := "green";
end if;

DriversSignal の条件分岐を上記のように書き換えると Fig 5 に表すエラーが発生する。これは request_for_pedestrians_signal に設定した赤点灯要求は歩行者用信号にはすぐには反映されず、結果的に歩行者用信号と自動車用信号が同時に青に点灯するケースが発生しまっているためである。したがってモデルチェッカーはシステムの Safety 特性として設定した BothSignalsDontTurnGreenAtTheSameTime 違反のエラーを報告する。