--LMNtalでの並行プログラムの検証--
-LMNtalでの並行プログラムの検証-
LMNtalにはプログラムの状態遷移を確認することが可能なため、
プログラムが意図しない動作をしないか検証することが可能である。
ここでは、並行プログラムをLMNtalで実装した際の検証の例を示す。
-LockOneアルゴリズムの検証-
並行プログラムの例で示したように、このプログラムはdeadlockするプログラムである。
以下に、LockOneアルゴリズムをLMNtalで実装した際の状態遷移図を示す。
この状態遷移図を見ると、無限にループする部分があり、この部分でdeadlockする可能性があるということが分かる。
-Bakeryアルゴリズムの検証-
deadlockしないプログラムの例としてBakeryアルゴリズムのプログラムの例をここに示す。
並行プログラムの例で示したLMNtalプログラムに加えて、
このプログラムが問題ないかを検証するために以下のルールを追加する。
// check
cs(0), cs(0), start :- error(0).
このルールにより、CriticalSectionに複数スレッドが入っていないかを検証できる。
以下に、BakeryアルゴリズムをLMNtalで実装した際の状態遷移図を示す。
この状態遷移図を確認することで、複数のスレッドがCriticalSectionに入ることがないということと、
全てのスレッドがCriticalSectionを実行し、終了していることが分かる。
このように、並行プログラムをLMNtalで実装することにより、プログラムの検証を行うことが出来ると分かる。