TLA+ on VSCodeで再帰ロックアルゴリズムを検証してみた
TLA+を使って『並行プログラミング入門』4.4章にある再帰ロックのアルゴリズムを検証してみました。TLA+は公式のGUIアプリも用意されているのですが、今回はVSCodeを利用してみました。公式のGUIアプリはエディタが微妙なのですが、VSCodeを使うとサクサク書けます。そのかわり、各種設定を設定ファイルに書く必要があります。
検証内容は「デッドロックしない」と「クリティカルセクションを実行中のプロセスは高々1つ」です。
TLA+と再帰ロックのアルゴリズムは以下を参照してください。
アルゴリズムの実装
次に、reclock.tlaを作成します。reclock.tlaにはPlusCalでアルゴリズムを記述します。具体的には、reclock.tlaというファイルを以下のように作成します。
------------------------------ MODULE reclock ------------------------------
EXTENDS Integers, TLC, Sequences, FiniteSets
CONSTANTS MAX_REC, PIDS
(*--algorithm lock
variables
locking = {}, \* ロック中のプロセス集合。検証用の変数
\* アルゴリズム用の変数
lock = FALSE,
id = 0,
cnt = 0;
\* ロック獲得
procedure acquire()
begin
Acquire:
if lock /\ id = self then
A0: cnt := cnt + 1;
else
TAS:
await lock = FALSE;
lock := TRUE;
locking := locking \union {self};
A1: id := self;
A2: cnt := cnt + 1;
end if;
A3: return
end procedure;
\* ロック開放
procedure release()
begin
Release:
cnt := cnt - 1;
R0:
if cnt = 0 then
R1: id := 0;
R2: lock := FALSE;
locking := locking \ {self};
end if;
R3: return;
end procedure;
\* 再帰ロック
procedure recursive_lock()
begin
RecLock:
either
Rec:
if cnt < MAX_REC then \* 最大MAX_REC回まで再帰ロック
RL0:
call lock_unlock() \* 再帰ロック
end if;
or
NotRec:
skip;
end either;
RL1: return;
end procedure;
procedure lock_unlock()
begin
Lock:
call acquire(); \* ロック獲得
L0: call recursive_lock(); \* 再帰ロック
L1: call release(); \* ロック開放
L2: return;
end procedure;
fair process pid \in PIDS
begin
T1:
call lock_unlock()
end process;
end algorithm;*)
TypeInvariant ==
/\ MAX_REC \in Int
/\ PIDS \subseteq Int
AtMostOne == Cardinality(locking) <= 1
=============================================================================つづいて、F1からTLA+: Parse Moduleを選択すると、TLA+の論理式がreclock.tlaに追記され、設定ファイルのreclock.cfgが出力されます。reclock.cfgに必要な設定を追加してきます。
reclock.cfgには、以下のように定数や検証する不変条件を追記します。「\* Add statements after this line.」という行より下が、今回追加した行です。定数と不変条件を設定します。
SPECIFICATION Spec
\* Add statements after this line.
CONSTANTS
PIDS = {1, 2, 3}
MAX_REC = 5
INVARIANTS
AtMostOne
TypeInvariant
検査
次に、再びF1からTLA+: Check model with TLCを選択して検査します。
検査に成功すると、以下のように出力されます。検査に失敗した場合は反例が表示されます。
以上簡単ですね。色々なものが検証できそうです。
