PlusCal: 並行システムと非同期処理

概要

このページでは PlusCal を使ってマルチプロセスやマルチスレッド、それらに伴う非同期処理といった並行処理を記述する方法について説明する。サンプルを実行するための環境セットアップは環境設定と検証の実行を参照。

Table of Contents

1. 概要
2. 並行システムの進行
3. プロセス間通信
   1. await 文
   2. デッドロック
   3. プロセス識別子
4. プロセス変数

並行システムの進行

単一プロセスのシステムでは begin から end algorithm の間に仕様を記述していたが、マルチプロセスでは process ブロック内に同様の記述を行うことで並行システムを記述することができる。process 内での処理記述はプロセス間通信時に await を使用する以外は単一プロセスのケースと同じである。

最初の例として複数のプロセスがどの様に進行するかを見てみよう。例 Example 1 は Hopper という 2 つのプロセスがそれぞれ 3 つのステップを実行している。そして、各プロセスが現在どのステップにいるかを状態変数 locations に保存している。つまりシステムの状態変数は \({\it locations}=(0,0)\) から始まり、すべてのプロセスが終了するときに \((3,3)\) に到達する。

---- MODULE StepProgress ----
EXTENDS Integers, TLC
(* --algorithm StepProgress
variables locations = << 0, 0 >>

process Hopper \in 1..2
begin
  Step1:
    locations[self] := 1;
    print locations;
  Step2:
    locations[self] := 2;
    print locations;
  Step3:
    locations[self] := 3;
    print locations;
end process;

end algorithm; *)
====

直感的に 2 プロセス × 3 ステップ = 6 の実行が行われると思うかもしれないが、結果の Output はもっと多い実行を示している。マルチプロセスでは (ステップが進行可能であれば) Process 1 が進行するケースと Process 2 が進行するケースのそれぞれを実行するためである。結果的にこのモデルでは \((0,0)\) から \((3,3)\) までのすべてのステップの組み合わせが実行され、Fig 2 で表される状態遷移図 (有限オートマトン) のようにすべての進行状況の組み合わせを再現する。

ステップを 1 実行単位とした CPU のタイムスライスやコルーチンのような進行を考えると良いかもしれない。

より一般的に \(n\) 個のプロセスのそれぞれが \(s\) 個の状態を持つ (つまり \(0\) から \(s-1\) までのステップのいずれかにいる) と考えると、システム全体の進行状態は \((s_1,\ldots,s_n)\) の状態ベクトルで表現できることから、システムが取りうる状態数は \(s^n\) 個となる。また、プロセス \(i\) は \(0 \le s_i \lt s-1\) のときに一つ進行することができ (1 つの矢印が発生し)、同様の進行は \(i\) 以外にも \(s^{n-1}\) 通りが可能であり、\(i\) は \(n\) 通りを取りうることから、状態の遷移数は \((s-1) \times s^{n-1} \times n\) 個となる。

Example 1 の例に適用すると \(n=2\), \(s=4\) より状態数 \(4^2=16\) (四角の数)、遷移数 \((4-1)\times 4^{2-1}\times 2=24\) (矢印の数) となる。結果の Coverage における Total 合計の 26 は遷移数 24 + 1 (init) + 1 (Terminating) と一致し、Distinct 合計の 16 は生成された一意の状態数 16 と一致していることが分かる。

この例が示すように、マルチプロセスでの個々のプロセスの進行状況は状態変数として表現することができるため、TLC モデルチェッカーによってすべての可能な進行状況の組み合わせを探索することができる (この例では明示的に locations という状態変数を用いたが、PlusCal から TLA+ にトランスパイルするときにこれと同じ目的を持つ pc (program control) という状態変数が自動的に作成される)。そしてプロセスの進行状況のすべての組み合わせを検査できるということは、レースコンディションに起因する並行処理の問題を検出できることを意味する。

プロセス間通信

PlusCal のプロセスは互いを認識することができないため、プロセス間の通信はグローバルな状態変数を共有することで行われる。そして別のプロセスによってグローバルな状態変数が期待する状態となるまで処理を待機する await を使用してプロセス間通信の同期ポイントを設置する。Example 3 の例はクライアントの送信したデータをサーバが送り返すだけの単純な Echo プロトコルのインタラクションを記述している。また Fig 4 はこの Echo プロトコルのシーケンス図を示している。

---- MODULE SimpleEcho ----
EXTENDS TLC
(* --algorithm SimpleEcho
variables
  client_to_server = "";
  server_to_client = "";

process client = "Client"
begin
  Send:
    client_to_server := "hello, world";
  Receive:
    await server_to_client /= "";
    print << "Client: ", server_to_client >>;
end process;

process server = "Server"
begin
  Receive:
    await client_to_server /= "";
    print << "Server: ", client_to_server >>;
  Send:
    server_to_client := client_to_server;
end process;

end algorithm; *)
====

Client - Server 間の通信は client_to_server と server_to_client という 2 つの状態変数を使用している。プロセスは互いを認識できないためグローバルなスコープを持つ状態変数を用いて通信する必要がある。

await 文

ラベル付けされたステップ中に await 文が含まれているとき、TLC はその条件式が true となるまでそのステップを実行対象から除外する (await の位置で停止するわけではない点に注意)。これは別のプロセスが条件式を true とするような作用を起こすことを暗に期待しており、プロセス間の同期ポイントと考えることができる。

await 文はステップ中のどこでも配置することができるが、そのステップに入る前に条件式が false であった場合、同一ステップ内で await より前に配置されている別の処理を実行しないまま停止する。この直観的ではない挙動がしばしば混乱を引き起こすため、可能な限りラベルの直後に await 文を配置することを推奨する。

例えば Example 3 のラベルを以下のように書き換えたとしよう。状態変数の初期化が終わった時点で server_to_client = "" であるため 12 行目の await により TLC は Client プロセスの Echo ステップを開始することができない。同時に client_to_server = "" であるため Server プロセスの Receive ステップも開始できない。結果的に TLC は実行可能なステップを見つけることができずデッドロックが発生していると判断する。

すべて表示

  Echo:
    client_to_server := "hello, world";
    await server_to_client /= "";
    print << "Client: ", server_to_client >>;

デッドロック

デッドロック (deadlock) はどのプロセスもステップを進行することができなくなったときに TLC により Deadlock reached というメッセージで報告されるエラーである。PlusCal のマルチプロセス環境では await で待機しているプロセスがいるにもかかわらず他にステップを進めることのできるプロセスが存在しなくなったときに発生する。また TLA+ を使っているケースでは単一プロセスの場合であっても Next で次に実行可能なステップが存在しなかったときに発生する。

デッドロックをシステムの正常停止と定義するようなシステムを検証する場合は、モデルファイルに CHECK_DEADLOCK FALSE を追加することで TLC がデッドロックをエラーとして扱わないようになる。

プロセス識別子

プロセスは識別子ごとにインスタンスを持つ。例えば例 Example 1 では process Hopper \in 1..2 のように Hopper プロセスを 2 インスタンス構築したし、例 Example 3 では process client = "Client" のように 1 インスタンスを構築している。プロセスに割り当てられている識別子はプロセス内から self で参照することができる。

TLA+ に変換されたコードを調べるとすべてのプロセス識別子が ProcSet に定義されていることが分かる。このため、プロセス定義が異なるとしても同じモジュール内で重複するプロセス識別子を使用することはできず、またすべてのプロセス識別子は同じ型でなければならない。

ProcSet == {"Client"} \cup {"Server"}

プロセス変数

process 内の variables に変数を宣言することで個々のプロセス固有の状態変数を持つことができる。ただし、変数自体はグローバルなスコープを持つため、他のプロセスの変数名と重複することはできない。これは、プロセス変数であっても TLA+ の観点からは VARIABLES で宣言される状態変数の 1 つに過ぎず、プロセス識別子 self を使って擬似的に固有領域を作り出してるためである。

この動きをもう少し具体的に調べてみよう。Example 5 に示すようにプロセス変数を使うと Alice, Bob, Carol がそれぞれ自分の自己紹介メッセージを message 変数に持つことができる。

---- MODULE ProcVar1 ----
EXTENDS Sequences, TLC
(* --algorithm ProcVar1
process Student \in {"Alice", "Bob", "Carol"}
variable message;
begin
  SelfIntroduction:
    message := "Hi, I'm " \o self \o ".";
    print message;
end process;
end algorithm; *)
====

TLA+ 変換後の定義を見ると、このプロセス変数 message の実体はグローバルなスコープを持つ関数 (一般の言語で言うところのマップ) であり、変数にアクセスするときに暗黙的にプロセス識別子 self が付与されるように変換されている。

VARIABLES message, ...
Init == message = [self \in {"Alice", "Bob", "Carol"} |-> defaultInitValue] /\ ...
SelfIntroduction(self) == message' = [message EXCEPT ![self] = "Hi, I'm " \o self \o "."]
                       /\ PrintT(message'[self]) /\ ...

VARIABLES で宣言されたプロセス変数そのものはグローバルなスコープを持つため他のプロセスから参照することができる。ただしそのときに暗に自身の識別子が付与されることから自分以外のプロセスの変数値にアクセスすることができない。例えば Example 6 では Teacher プロセスから secret["Alice"] を参照しようとしているが、実質的には secret["Teacher"]["Alice"] を参照していて意図した値は取得できない。

---- MODULE ProcVar2 ----
EXTENDS Sequences, TLC
(* --algorithm SecretOfAlice
process Student \in {"Alice", "Bob", "Carol"}
variable secret;  \* => VARIABLES secret
begin
  A: secret := self \o "'s secret";
    \* => secret' = [secret EXCEPT ![self] = self \o "'s secret"]
end process;

process Teacher = "Teacher"
begin
  B: print secret["Alice"]
    \* => PrintT(secret["Teacher"]["Alice"])
end process;
end algorithm; *)
====