(57)【要約】  【課題】  メモリーコンシステンシーモデルを考慮し、プログラムの検証を行うプログラム検証プログラム、プログラム検証装置、プログラム検証方法を提供する。  【解決手段】  検証対象プログラムの検証を行うプログラム検証方法をコンピュータに実行させるプログラム検証プログラムであって、検証対象プログラムの処理手順を記述した処理手順モデルを生成する処理手順モデル生成ステップと、メモリーコンシステンシーモデルに基づいて、処理手順モデルに処理手順を追加する処理手順モデル変更ステップと、処理手順モデルの検証を行う処理手順モデル検証ステップとをコンピュータに実行させる。  【選択図】  図２
2006277580.tif 000002
【特許請求の範囲】
【請求項１】
検証対象プログラムの検証を行うプログラム検証方法をコンピュータに実行させるプログラム検証プログラムであって、
前記検証対象プログラムの処理手順を記述した処理手順モデルを生成する処理手順モデル生成ステップと、
メモリーコンシステンシーモデルに基づいて、前記処理手順モデルに処理手順を追加する処理手順モデル変更ステップと、
前記処理手順モデルの検証を行う処理手順モデル検証ステップと、
をコンピュータに実行させるプログラム検証プログラム。
【請求項２】
請求項１に記載のプログラム検証プログラムにおいて、
前記処理手順モデル変更ステップは、前記処理手順モデルにおいて前記メモリーコンシステンシーモデルにより非決定的となる部分を検出し、該部分に別の発生し得る前記処理手順を追加することを特徴とするプログラム検証プログラム。
【請求項３】
請求項１または請求項２に記載のプログラム検証プログラムにおいて、
前記非決定的となる部分は、前記メモリーコンシステンシーモデルにより順序の変更が許可された命令列の部分であり、前記別の処理手順は、前記命令列の順序を変更した処理手順であることを特徴とするプログラム検証プログラム。
【請求項４】
検証対象プログラム検証を行うプログラム検証装置であって、
前記検証対象プログラムの処理手順を記述した処理手順モデルを生成する処理手順モデル生成部と、
メモリーコンシステンシーモデルに基づいて、前記処理手順モデルに処理手順を追加する処理手順モデル変更部と、
前記処理手順モデルの検証を行う処理手順モデル検証部と、
を備えてなるプログラム検証装置。
【請求項５】
検証対象プログラムの検証を行うプログラム検証方法であって、
前記検証対象プログラムの処理手順を記述した処理手順モデルを生成する処理手順モデル生成ステップと、
メモリーコンシステンシーモデルに基づいて、前記処理手順モデルに処理手順を追加する処理手順モデル変更ステップと、
前記処理手順モデルの検証を行う処理手順モデル検証ステップと、
を実行するプログラム検証方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プログラムの検証を行うプログラム検証プログラム、プログラム検証装置、プログラム検証方法に関するものである。
【背景技術】
【０００２】
複数のプロセッサを持つ並列計算機の一種に、共有メモリ型並列計算機がある。共有メモリ型並列計算機は、各プロセッサが主記憶装置を共有するアーキテクチャであり、代表的な例としては、ＳＭＰ（Symmetric Multi Processor）がある。また、共有メモリ型並列計算機は、プログラムを記述する際に各タスク間のデータの受け渡しが容易であるという特徴があることから、よく利用されている。
【０００３】
共有メモリ型並列計算機においては、性能向上等のために、主記憶装置への読み書きの順序が、プログラムに記述された順序と異なる場合がある。このような場合のために、主記憶装置に対する命令の順序の保証範囲を示すものが、メモリーコンシステンシーモデル（Memory Consistency Model）である。メモリーコンシステンシーモデルには、ＴＳＯ（Total Store Ordering）、ＰＳＯ（Partial Store Ordering）等がある。
【０００４】
ここで、メモリーコンシステンシーモデルの例として、ＴＳＯについて説明する。ＴＳＯは、次の順序制約を持つ。ここで、ロード（load）命令は、主記憶装置からデータを読み出す命令であり、ストア（store）命令は、主記憶装置にデータを書き込む命令である。
【０００５】
１．ストア命令は、ロード命令、ストア命令を追い越せない。
２．ロード命令は、ストア命令を追い越せる。
３．ロード命令は、ロード命令を追い越せない。
【０００６】
また、並列プログラムの検証には、モデル検査ツールが用いられている。この手法は、検証対象である並列プログラムをＦＳＭ（有限状態機械：Finite State Machine）として捉え、初期状態から全ての状態遷移を辿ることにより、並列プログラムが仕様を満たしているか否かを調べるものである。例えば、デッドロックやデータ競合が発生するか否か、等を調べる。
【０００７】
なお、本発明の関連ある従来技術として、例えば、下記に示す特許文献１が知られている。これは、プログラム言語により電子回路を設計する装置であり、回路動作を記述したプログラムの中で順次動作する部分を、ステートマシンとして動作するように変換し、変換後のプログラムを得るものである。
【特許文献１】特開平１０−１４９３８２号公報
【発明の開示】
【発明が解決しようとする課題】
【０００８】
ここで、ＴＳＯに従う動作の例について説明する。図１４は、プログラムの記述における命令列の順序の一例を示す図である。ＴＳＯに従う並列計算機上で、このプログラムを実行すると、実際の主記憶装置への読み書きにおいて、“ｌｏａｄ  ｃ”命令が“ｓｔｏｒｅ  ｂ”命令を追い越す可能性がある。図１５は、プログラムの処理における命令列の順序の一例を示す図である。このように、プログラムで記述における順序とプログラムの処理における順序が異なる場合、正しく動作するプログラムを記述することが難しいという問題がある。
【０００９】
また、従来、並列プログラムの検証を行う場合に、メモリーコンシステンシーモデルを考慮することは不可能であった。
【００１０】
本発明は上述した問題点を解決するためになされたものであり、メモリーコンシステンシーモデルを考慮し、プログラムの検証を行うプログラム検証プログラム、プログラム検証装置、プログラム検証方法を提供することを目的とする。
【課題を解決するための手段】
【００１１】
上述した課題を解決するため、本発明は、検証対象プログラムの検証を行うプログラム検証方法をコンピュータに実行させるプログラム検証プログラムであって、前記検証対象プログラムの処理手順を記述した処理手順モデルを生成する処理手順モデル生成ステップと、メモリーコンシステンシーモデルに基づいて、前記処理手順モデルに処理手順を追加する処理手順モデル変更ステップと、前記処理手順モデルの検証を行う処理手順モデル検証ステップとをコンピュータに実行させるものである。
【００１２】
また、本発明に係るプログラム検証プログラムにおいて、前記処理手順モデル変更ステップは、前記処理手順モデルにおいて前記メモリーコンシステンシーモデルにより非決定的となる部分を検出し、該部分に別の発生し得る前記処理手順を追加することを特徴とするものである。
【００１３】
また、本発明に係るプログラム検証プログラムにおいて、前記非決定的となる部分は、前記メモリーコンシステンシーモデルにより順序の変更が許可された命令列の部分であり、前記別の処理手順は、前記命令列の順序を変更した処理手順であることを特徴とするものである。
【００１４】
また、本発明に係るプログラム検証プログラムにおいて、前記処理手順モデルは、状態機械であることを特徴とするものである。
【００１５】
また、本発明に係るプログラム検証プログラムにおいて、前記検証対象プログラムは、並列プログラムまたは並行プログラムであることを特徴とするものである。
【００１６】
また、本発明に係るプログラム検証プログラムにおいて、前記処理手順モデル変更ステップは、予めメモリーコンシステンシーモデルの候補を記憶しておき、ユーザの指示に従って候補の中から１つを選択することにより前記メモリーコンシステンシーモデルを設定することを特徴とするものである。
【００１７】
また、本発明に係るプログラム検証プログラムにおいて、前記メモリーコンシステンシーモデルの候補は、ＴＳＯ、ＰＳＯのいずれかを含むことを特徴とするものである。
【００１８】
また、本発明に係るプログラム検証プログラムにおいて、前記処理手順モデル変更ステップは、ユーザの指示に従って、ロード命令、ストア命令、同期命令の順序制約を定義することにより前記メモリーコンシステンシーモデルを設定することを特徴とするものである。
【００１９】
また、本発明は、検証対象プログラム検証を行うプログラム検証装置であって、前記検証対象プログラムの処理手順を記述した処理手順モデルを生成する処理手順モデル生成部と、メモリーコンシステンシーモデルに基づいて、前記処理手順モデルに処理手順を追加する処理手順モデル変更部と、前記処理手順モデルの検証を行う処理手順モデル検証部とを備えたものである。
【００２０】
また、本発明に係るプログラム検証装置において、前記処理手順モデル変更部は、前記処理手順モデルにおいて前記メモリーコンシステンシーモデルにより非決定的となる部分を検出し、該部分に別の発生し得る前記処理手順を追加することを特徴とするものである。
【００２１】
また、本発明に係るプログラム検証装置において、前記非決定的となる部分は、前記メモリーコンシステンシーモデルにより順序の変更が許可された命令列の部分であり、前記別の処理手順は、前記命令列の順序を変更した処理手順であることを特徴とするものである。
【００２２】
また、本発明に係るプログラム検証装置において、前記処理手順モデルは、状態機械であることを特徴とするものである。
【００２３】
また、本発明に係るプログラム検証装置において、前記検証対象プログラムは、並列プログラムまたは並行プログラムであることを特徴とするものである。
【００２４】
また、本発明に係るプログラム検証装置において、前記処理手順モデル変更部は、予めメモリーコンシステンシーモデルの候補を記憶しておき、ユーザの指示に従って候補の中から１つを選択することにより前記メモリーコンシステンシーモデルを設定することを特徴とするものである。
【００２５】
また、本発明に係るプログラム検証装置において、前記メモリーコンシステンシーモデルの候補は、ＴＳＯ、ＰＳＯのいずれかを含むことを特徴とするものである。
【００２６】
また、本発明に係るプログラム検証装置において、前記処理手順モデル変更部は、ユーザの指示に従って、ロード命令、ストア命令、同期命令の順序制約を定義することにより前記メモリーコンシステンシーモデルを設定することを特徴とするものである。
【００２７】
また、本発明は、検証対象プログラムの検証を行うプログラム検証方法であって、前記検証対象プログラムの処理手順を記述した処理手順モデルを生成する処理手順モデル生成ステップと、メモリーコンシステンシーモデルに基づいて、前記処理手順モデルに処理手順を追加する処理手順モデル変更ステップと、前記処理手順モデルの検証を行う処理手順モデル検証ステップとを実行するものである。
【発明の効果】
【００２８】
本発明によれば、メモリーコンシステンシーモデルに従う非決定的な状態遷移を含めたＦＳＭを作成することができる。更に、このＦＳＭのモデル検査を行うことにより、メモリーコンシステンシーモデルを考慮した検証が可能となり、並列プログラムや並行プログラムの開発において検証の信頼性を向上させることができる。
【発明を実施するための最良の形態】
【００２９】
以下、本発明の実施の形態について図面を参照しつつ説明する。
【００３０】
本実施の形態に係るプログラム検証装置は、検証対象プログラムの処理手順を記述した処理手順モデルを生成し、メモリーコンシステンシーモデルに基づいて処理手順モデルに処理手順を追加し、処理手順モデルのモデル検査を行うものである。ここで、処理手順モデルは、特にメモリにアクセスする処理手順に着目する。また、本実施の形態においては、代表的な処理手順モデルとしてＦＳＭを用いる。
【００３１】
まず、本発明に係るプログラム検証装置の構成について説明する。
【００３２】
図１は、本発明に係るプログラム検証装置の構成の一例を示すブロック図である。このプログラム検証装置は、検証対象プログラム取得部２１、状態機械作成部２２、メモリーコンシステンシーモデル設定部２３、状態機械変更部２４、検証項目設定部１４、モデル検査部１５、検証結果表示部１６を備える。
【００３３】
次に、本発明に係るプログラム検証装置の動作について説明する。
【００３４】
まず、検証前の動作について説明する。検証対象プログラム取得部２１は、検証の対象となる検証対象プログラムを取得する。また、メモリーコンシステンシーモデル設定部２３は、ユーザの指示に従ってメモリーコンシステンシーモデルを設定する。メモリーコンシステンシーモデルの設定方法としては、予めＴＳＯ、ＰＳＯ等のメモリーコンシステンシーモデルの候補がメモリーコンシステンシーモデル設定部２３に予め記憶されており、ユーザが候補の中から選択する簡単な設定方法と、ユーザがロード命令、ストア命令、同期命令の順序制約を定義する詳細な設定方法があり、いずれを用いても良い。また、検証項目設定部１４は、ユーザの指示に従って検証項目を設定する。検証項目の設定方法としては、予めデッドロック、データ競合等のパターンが用意されており、ユーザがパターンを選択する方法がある。
【００３５】
次に、検証の動作について説明する。図２は、本発明に係るプログラム検証装置の動作の一例を示すフローチャートである。まず、状態機械作成部２２は、検証対象プログラム取得部２１が出力する検証対象プログラムをモデル化し、ＦＳＭに変換する（Ｓ１２）。次に、状態機械変更部２４は、メモリーコンシステンシーモデル設定部２３におけるメモリーコンシステンシーモデルに基づいて、状態機械作成部２２により出力されたＦＳＭの変更を行う（Ｓ１３）。ここでは、ＦＳＭにおいてメモリーコンシステンシーモデルにより非決定的となる部分を検出し、この部分に別の発生し得る状態遷移を追加する。次に、モデル検査部１５は、検証項目設定部１４が出力する検証項目について、状態機械変更部２４により出力されたＦＳＭのモデル検査を行う（Ｓ１４）。次に、検証結果表示部１６は、モデル検査部１５により出力された検証結果の表示を行い（Ｓ１５）、このフローを終了する。ここで、状態機械作成部２２は、既存の状態機械作成手法を用いる。また、モデル検査部１５は、既存のモデル検査手法を用いる。
【００３６】
次に、状態機械変更部２４によるＦＳＭの変更の動作について説明する。
【００３７】
本実施の形態では、状態機械作成部２２が、命令発行と状態が対応するように検証対象プログラムをモデル化し、ムーア型ＦＳＭに変換する。なお、ミーリー型ＦＳＭでも同様の動作を行うことができる。図３は、本発明に係る状態機械変更部の動作の一例を示すフローチャートである。まず、状態機械変更部２４は、ＦＳＭの全ての状態集合から状態を１つを選択してｐとする（Ｓ３１）。次に、ｐが初期状態であるか否かの判断を行う（Ｓ３２）。ｐが初期状態であれば（Ｓ３２，Ｙ）、処理Ｓ３９へ移行する。一方、ｐが初期状態でなければ（Ｓ３２，Ｎ）、状態機械変更部２４は、ｐより前の状態から１つを選択してｑとする（Ｓ３３）。次に、状態機械変更部２４は、メモリーコンシステンシーモデル設定部２３におけるメモリーコンシステンシーモデルを参照し、ｐがｑを追い越せるか否かの判断を行う（Ｓ３４）。
【００３８】
ｐがｑを追い越せない場合（Ｓ３４，Ｎ）、処理Ｓ３８へ移行する。一方、ｐがｑを追い越せる場合（Ｓ３４，Ｙ）、状態機械変更部２４は、ｑの１つ前の状態から１つを選択してｒとする（Ｓ３５）。次に、状態機械変更部２４は、ｒ→ｐ→ｑの命令列が発生するように、ＦＳＭに状態遷移を追加する（Ｓ３６）。
【００３９】
次に、状態機械変更部２４は、ｑの１つ前の状態であるｒの候補に残りがあるか否かの判断を行う（Ｓ３７）。ｒの候補に残りがある場合（Ｓ３７，Ｙ）、処理Ｓ３５へ戻る。一方、ｒの候補に残りがない場合（Ｓ３７，Ｎ）、状態機械変更部２４は、ｐより前の状態であるｑの候補に残りがあるか否かの判断を行う（Ｓ３８）。ｑの候補に残りがある場合（Ｓ３８，Ｙ）、処理Ｓ３３へ戻る。一方、ｑの候補に残りがない場合（Ｓ３８，Ｎ）、状態機械変更部２４は、全ての状態集合であるｐの候補に残りがあるか否かの判断を行う（Ｓ３９）。ｐの候補に残りがある場合（Ｓ３９，Ｙ）、処理Ｓ３１へ戻る。一方、ｐの候補に残りがない場合（Ｓ３９，Ｎ）、このフローを終了する。
【００４０】
処理Ｓ３６の詳細について、ｑがｐの１つ前の状態である場合と、ｑがｐの２つ以上前の状態である場合に分けて説明する。
【００４１】
まず、ｑがｐの１つ前の状態である場合について説明する。まず、状態機械変更部２４は、ｐ、ｑの命令を持つ新しい状態ｐ’、ｑ’を生成する。次に、状態機械変更部２４は、状態遷移（ｒ、ｐ’）、（ｐ’、ｑ’）をＦＳＭに追加する。状態遷移（ｒ、ｐ’）の表記は、状態ｒから状態ｐ’への遷移を表す。ここで、ｐの１つ後の状態をｎｅｘｔ（ｐ）とする。次に、状態機械変更部２４は、全てのｎｅｘｔ（ｐ）について状態遷移（ｑ’、ｎｅｘｔ（ｐ））をＦＳＭに追加する。
【００４２】
まず、ｑがｐの２つ以上前の状態である場合について説明する。まず、状態機械変更部２４は、新しい状態ｐ’、ｑ’に加えて、ｑとｐの間にある状態ｓ１，ｓ２，…ｓｎの命令を持つ新しい状態ｓ１’，ｓ２’，…ｓｎ’を生成し、ｓ１，ｓ２，…ｓｎの間の状態遷移（ｓｘ，ｓｙ）に対応してｓ１’，ｓ２’，…ｓｎ’間の状態遷移（ｓｘ’，ｓｙ’）をＦＳＭに追加する。次に、状態機械変更部２４は、状態遷移（ｒ、ｐ’）、（ｐ’、ｑ’）をＦＳＭに追加する。ここで、状態ｓ１，ｓ２，…ｓｎの中でｐの１つ前の状態をｐｒｅｖ（ｐ）とし、ｐｒｅｖ（ｐ）の命令を持つ新しい状態として生成された状態をｐｒｅｖ’（ｐ）とする。次に、状態機械変更部２４は、全てのｎｅｘｔ（ｐ）について状態遷移（ｐｒｅｖ’（ｐ）、ｎｅｘｔ（ｐ））をＦＳＭに追加する。
【００４３】
次に、本発明に係るプログラム検証装置の動作について、具体例を用いて説明する。
【００４４】
まず、検証対象プログラムの具体例について説明する。ここでは、生産者−消費者問題として知られるアルゴリズムを実装した並列プログラムを、検証対象プログラムとする。図４は、本発明に係る検証対象プログラムの構成の一例を示すブロック図である。このアルゴリズムは、２つのタスクであるＰｒｏｄｕｃｅｒ３１とＣｏｎｓｕｍｅｒ３３の間において、バッファ（Ｂｕｆｆｅｒ）３２を介してデータを送受信する機構である。
【００４５】
次に、検証対象プログラムのソースコードの具体例について説明する。ここでは、Ｃ言語で記述されたソースコードを用いる。図５は、参考文献：docs.sun.com：マルチスレッドのプログラミング（http：//docs.sun.com/app/docs/doc/816−3976？l＝ja）の例９−５で紹介されている、本発明に係る検証対象プログラムの一例を示すソースコードである。検証対象プログラムは、共有変数の定義、関数ｐｒｏｄｕｃｅｒ、関数ｃｏｎｓｕｍｅｒの３つのソースコードを持つ。ここで、変数ｂｕｆｆｅｒはバッファ３２の内容であり、定数ＢＳＩＺＥはバッファ３２のサイズであり、変数ｉｎは書き込みポインタであり、変数ｏｕｔは読み出しポインタである。また、関数ｐｒｏｄｕｃｅｒはＰｒｏｄｕｃｅｒ３１の動作を表す関数であり、バッファ３２へデータを書き込む度に呼び出される関数である。また、関数ｃｏｎｓｕｍｅｒはＣｏｎｓｕｍｅｒ３３の動作を表す関数であり、バッファ３２からデータを読み出す度に呼び出される関数である。また、関数ｐｒｏｄｕｃｅｒにおける変数ｉｔｅｍはバッファ３２へ書き込むデータであり、関数ｃｏｎｓｕｍｅｒにおける変数ｉｔｅｍはバッファ３２から読み込んだデータである。
【００４６】
この検証対象プログラムは、メモリーコンシステンシーモデルがＴＳＯである時に正しく動作するものである。図６は、メモリーコンシステンシーモデルがＴＳＯである場合の順序制約の一例を示す表である。この表は、プログラムの記述における現在の命令と前の命令の組み合わせについて表しており、○が記されているとき、現在の命令は前の命令を追い越すことが可能であることを表す。上述したように、ＴＳＯにおいては、現在の命令がロード命令である場合、前のストア命令を追い越すことができる。
【００４７】
次に、プログラム検証装置における設定の具体例について説明する。検証対象プログラム取得部２１が取得する検証対象プログラムは、図５の並列プログラムとする。説明を簡単にするため、検証対象プログラムにおいてＢＳＩＺＥ＝１とする。また、メモリーコンシステンシーモデル設定部２３に設定されるメモリーコンシステンシーモデルは、ＰＳＯとする。図７は、メモリーコンシステンシーモデルがＰＳＯである場合の順序制約の一例を示す表である。ＰＳＯにおいては、現在の命令がロード命令またはストア命令である場合、前のストア命令を追い越すことができる。メモリーコンシステンシーモデル設定部２３には、図７のようなメモリーコンシステンシーモデルが設定される。また、検証項目設定部１４に設定される検証項目は、「データ競合が発生しない」こととする。
【００４８】
次に、状態機械作成部２２の動作の具体例について説明する。状態機械作成部２２は、Ｐｒｏｄｕｃｅｒ３１とＣｏｎｓｕｍｅｒ３３から、共有変数であるｂｕｆｆｅｒ，ｉｎ，ｏｕｔへの読み書きを抽出し、ＦＳＭを作成する。ここで、ｉｎ％ＢＳＩＺＥ，ｏｕｔ％ＢＳＩＺＥをそれぞれｉｎ，ｏｕｔと表記し、ｉｎを読み出す処理をＲ（ｉｎ）と表記し、ｂｕｆｆｅｒ［ｉｎ］に書き込む処理をＷ（ｂｕｆｆｅｒ［ｉｎ］）と表記し、ｉｎに１を書き込む処理をＷ（ｉｎ，１）と表記する。
【００４９】
図８は、本発明に係る状態機械作成部により抽出されたＰｒｏｄｕｃｅｒの処理の一例を示す表である。図に示すように、関数ｐｒｏｄｕｃｅｒから共有変数の読み書き処理Ｐ１，Ｐ２，Ｐ３が抽出される。図９は、本発明に係る状態機械作成部により抽出されたＣｏｎｓｕｍｅｒの処理の一例を示す表である。図に示すように、関数ｃｏｎｓｕｍｅｒから共有変数の読み書き処理Ｃ１，Ｃ２，Ｃ３が抽出される。
【００５０】
次に、Ｐｒｏｄｕｃｅｒ３１とＣｏｎｓｕｍｅｒ３３のＦＳＭが作成される。ここで、変数ｉｎの値はＰｒｏｄｕｃｅｒ３１の状態に用いられ、変数ｏｕｔの値はＣｏｎｓｕｍｅｒ３３の状態に用いられる。また、ＢＳＩＺＥ＝１であることから、ｉｎ＝０，１、ｏｕｔ＝０，１の値を取る。
【００５１】
図１０は、本発明に係る状態機械作成部により作成されたＰｒｏｄｕｃｅｒのＦＳＭの一例を示す状態遷移図である。状態として、Ｐ０１（Ｓ２０１），Ｐ０２（Ｓ２０２），Ｐ０３（Ｓ２０３）、Ｐ１１（Ｓ２１１），Ｐ１２（Ｓ２１２），Ｐ１３（Ｓ２１３）が生成される。状態Ｐ０１，Ｐ１１は、処理Ｐ１に対応し、状態Ｐ０２，Ｐ１２は、処理Ｐ２に対応し、状態Ｐ０３，Ｐ１３は、処理Ｐ３に対応する。また、状態Ｐ０１，Ｐ０２，Ｐ０３はｉｎ＝０の状態であり、状態Ｐ１１，Ｐ１２，Ｐ１３はｉｎ＝１の状態である。また、状態遷移（Ｐ０１，Ｐ０２）はガード条件ｏｕｔ＝＝０が成立した場合に遷移し、状態遷移（Ｐ１１，Ｐ１２）はガード条件ｏｕｔ＝＝１が成立した場合に遷移する。
【００５２】
図１１は、本発明に係る状態機械作成部により作成されたＣｏｎｓｕｍｅｒのＦＳＭの一例を示す状態遷移図である。状態として、Ｃ０１（Ｓ３０１），Ｃ０２（Ｓ３０２），Ｃ０３（Ｓ３０３）、Ｃ１１（Ｓ３１１），Ｃ１２（Ｓ３１２），Ｃ１３（Ｓ３１３）が生成される。状態Ｃ０１，Ｃ１１は、処理Ｃ１に対応し、状態Ｃ０２，Ｃ１２は、処理Ｃ２に対応し、状態Ｃ０３，Ｃ１３は、処理Ｃ３に対応する。また、状態Ｃ０１，Ｃ０２，Ｃ０３はｏｕｔ＝０の状態であり、状態Ｃ１１，Ｃ１２，Ｃ１３はｏｕｔ＝１の状態である。また、状態遷移（Ｃ０１，Ｃ０２）はガード条件ｉｎ＝＝１が成立した場合に遷移し、状態遷移（Ｃ１１，Ｃ１２）はガード条件ｉｎ＝＝０が成立した場合に遷移する。また、状態Ｃ０１，Ｃ０２を含む部分Ｓ３００は、後述するＦＳＭの合成の説明に用いる部分である。
【００５３】
次に、状態機械変更部２４の動作の具体例について説明する。状態機械変更部２４は、図７のメモリーコンシステンシーモデルを参照する。メモリーコンシステンシーモデルの設定がＰＳＯであることから、書き込み処理（ストア命令）の順序が保証されない。従って、検証対象プログラムにおいては、Ｃｏｎｓｕｍｅｒ３３から見ると、Ｐｒｏｄｕｃｅｒ３１における処理Ｐ２と処理Ｐ３の順序が非決定的となり、上述したＦＳＭの変更のフローにより、Ｐｒｏｄｕｃｅｒ３１のＦＳＭは、別の発生し得る状態遷移が追加される。一方、Ｃｏｎｓｕｍｅｒ３３のＦＳＭは変更されない。
【００５４】
図１２は、本発明に係る状態機械変更部により変更されたＰｒｏｄｕｃｅｒのＦＳＭの一例を示す状態遷移図である。図１２において、図１０と同一符号は図１０に示された対象と同一又は相当物を示しており、ここでの説明を省略する。図１０のＦＳＭと比較すると図１２のＦＳＭには新たに、状態Ｐ０３（Ｓ２２２），Ｐ０２（Ｓ２２３）が追加される。これは、状態Ｐ０２（Ｓ２０２），Ｐ０３（Ｓ２０３）の順序が逆になった場合を表す。更に、ＦＳＭには新たに、状態Ｐ１３（Ｓ２３２），Ｐ１２（Ｓ２３３）が追加される。これは、状態Ｐ１２（Ｓ２１２），Ｐ１３（Ｓ２１３）の順序が逆になった場合を表す。また、状態Ｐ０１（Ｓ２０１），Ｐ０２（Ｓ２０２），Ｐ０３（Ｓ２０３），Ｐ０３（Ｓ２２２），Ｐ０２（Ｓ２２３）を含む部分Ｓ４００は、後述するＦＳＭの合成の説明に用いる部分である。
【００５５】
次に、状態機械変更部２４は、Ｐｒｏｄｕｃｅｒ３１のＦＳＭとＣｏｎｓｕｍｅｒ３３のＦＳＭを、１つのＦＳＭに合成すると共に、存在しない状態遷移を削除する。図１３は、本発明に係る状態機械変更部により合成されたＦＳＭの一例を示す状態遷移図である。状態機械変更部２４により合成されたＦＳＭの部分Ｓ４００は、上述したＰｒｏｄｕｃｅｒ３１のＦＳＭの部分Ｓ４００とＣｏｎｓｕｍｅｒ３３のＦＳＭの部分Ｓ３００を、合成したＦＳＭである。また、ガードは省略している。
【００５６】
状態Ｐ０１Ｃ０１（Ｓ４０１）は、Ｐｒｏｄｕｃｅｒ３１のＦＳＭにおける状態Ｐ０１（Ｓ２０１）とＣｏｎｓｕｍｅｒ３３のＦＳＭにおける状態Ｃ０１（Ｓ３０１）を合成したものである。同様に、状態Ｐ０２Ｃ０１（Ｓ４０２）は、状態Ｐ０２（Ｓ２０２）と状態Ｃ０１（Ｓ３０１）を合成したものであり、状態Ｐ０３Ｃ０１（Ｓ４０３）は、状態Ｐ０３（Ｓ２０３）と状態Ｃ０１（Ｓ３０１）を合成したものであり、状態Ｐ０３Ｃ０１（Ｓ４１２）は、状態Ｐ０３（Ｓ２２２）と状態Ｃ０１（Ｓ３０１）を合成したものであり、状態Ｐ０２Ｃ０１（Ｓ４１３）は、状態Ｐ０２（Ｓ２２３）と状態Ｃ０１（Ｓ３０１）を合成したものであり、状態Ｐ０３Ｃ０２（Ｓ４２３）は、状態Ｐ０３（Ｓ２２２）と状態Ｃ０２（Ｓ３０２）を合成したものである。
【００５７】
次に、モデル検査部１５の動作の具体例について説明する。検証項目設定部１４に設定された検証項目「データ競合が発生しない」について、具体的に表すと次の２点となる。第１に「Ｐｒｏｄｕｃｅｒ３１がバッファ３２に書き込んだデータを、Ｃｏｎｓｕｍｅｒ３３が読む前に、上書きすることはない。」ことであり、第２に「Ｐｒｏｄｕｃｅｒ３１がバッファ３２にデータを書き込む前に、Ｃｏｎｓｕｍｅｒ３３がバッファ３２を読むことはない。」ことである。
【００５８】
上述した２点の検証項目を合わせ、処理のパターンとして表すと、バッファ３２に対する書き込み処理Ｗと読み出し処理Ｒについて、「ＷＲの処理のペアが繰り返される。」ことになる。ここで、Ｗは処理Ｗ（ｂｕｆｆｅｒ［ｉ］）を表し、Ｒは処理Ｒ（ｂｕｆｆｅｒ［ｉ］）を表し、ｉは、０≦ｉ≦ＢＳＩＺＥの整数を表す。検証項目を満たす処理としては例えば、ＷＲＷＲＷＲＷＲＷＲの処理である。一方、検証項目を満たさない処理としては例えば、ＷＷの処理や、ＲＷＲＷの処理である。
【００５９】
モデル検査部１５は、検証項目についてＦＳＭ上の状態遷移を調べる。注目する状態は、Ｗ（ｂｕｆｆｅｒ［０］）が発生する状態Ｐ０２、Ｗ（ｂｕｆｆｅｒ［１］）が発生する状態Ｐ１２、Ｒ（ｂｕｆｆｅｒ［０］）が発生する状態Ｃ０２、Ｒ（ｂｕｆｆｅｒ［１］）が発生する状態Ｃ１２である。従って、ＦＳＭ上の検証項目は次のようになる。「状態Ｐ０２に到達した後、状態Ｃ０２を経由せずに再び状態Ｐ０２に到達することはない。」こと、「初期状態または状態Ｃ０２の後に、状態Ｐ０２を経由せずに状態Ｃ０２に到達することはない。」こと、「状態Ｐ１２に到達した後、状態Ｃ１２を経由せずに再び状態Ｐ１２に到達することはない。」こと、「初期状態または状態Ｃ１２の後に、状態Ｐ１２を経由せずに状態Ｃ１２に到達することはない。」ことである。
【００６０】
実際に、図１３のＦＳＭについてモデル検査部１５によるモデル検査を行うと、検証項目を満たさないことになる。これは、状態Ｐ０１Ｃ０１（Ｓ４０１）→状態Ｐ０３Ｃ０１（Ｓ４１２）→状態Ｐ０３Ｃ０２（Ｓ４２３）という状態遷移が検証項目に違反するからである。つまり、状態Ｃ０２でＲ（ｂｕｆｆｅｒ［０］）が発生するのに、それよりも前に状態Ｐ０２を経由していないことから、Ｐｒｏｄｕｃｅｒ３１がバッファ３２にデータを書き込む前に、Ｃｏｎｓｕｍｅｒ３３がバッファ３２を読んでしまうことになるからである。
【００６１】
上述したように、状態機械変更部２４により出力されるＦＳＭは、メモリーコンシステンシーモデルに従う非決定的な状態遷移を含めたＦＳＭとなる。モデル検査部１５がこのＦＳＭのモデル検査を行うことにより、メモリーコンシステンシーモデルを考慮した検証が可能となる。
【００６２】
なお、本実施の形態においては、並列プログラムの検証について述べたが、同様にして本発明を並行プログラムの検証に適用することも可能である。
【００６３】
また、本実施の形態においては、プログラム検証装置に検証対象プログラム取得部２１と状態機械作成部２２を含めたが、プログラム検証装置１３からこれらを省き、外部の検証対象プログラム取得部と状態機械作成部により作成されたＦＳＭをプログラム検証装置に入力し、ＦＳＭの変更を行う構成としても良い。また、本実施の形態においては、プログラム検証装置に検証項目設定部１４とモデル検査部１５と検証結果表示部１６を含めたが、プログラム検証装置１３からこれらを省き、状態機械変更部２４が出力するＦＳＭを外部のモデル検査部に渡し、モデル検査を行う構成としても良い。
【００６４】
また、本実施の形態においては、ＦＳＭを用いてモデル検査を行うこととしたが、他の手段を排除するものではない。例えば、ソースプログラム中のメモリアクセスを行う命令を抽出した命令列を生成し、メモリーコンシステンシーモデルに従って命令の発行の順が非決定的となる命令の並びを入れ替えた命令列を生成し、抽出した命令列及び生成した全ての命令列に対して検証を行うことは、本発明の技術的範囲に属するものである。
【００６５】
更に、プログラム検証装置を構成するコンピュータにおいて上述した各ステップを実行させるプログラムを、プログラム検証プログラムとして提供することができる。上述したプログラムは、コンピュータにより読取り可能な記録媒体に記憶させることによって、プログラム検証装置を構成するコンピュータに実行させることが可能となる。ここで、上記コンピュータにより読取り可能な記録媒体としては、ＲＯＭやＲＡＭ等のコンピュータに内部実装される内部記憶装置、ＣＤ−ＲＯＭやフレキシブルディスク、ＤＶＤディスク、光磁気ディスク、ＩＣカード等の可搬型記憶媒体や、コンピュータプログラムを保持するデータベース、或いは、他のコンピュータ並びにそのデータベースや、更に回線上の伝送媒体をも含むものである。
【００６６】
なお、処理手順モデル生成部とは、実施の形態における検証対象プログラム取得部２１、状態機械作成部２２に対応する。また、処理手順モデル変更部とは、実施の形態におけるにメモリーコンシステンシーモデル設定部２３、状態機械編変更部２４に対応する。また、処理手順モデル検証部とは、実施の形態における検証項目設定部１４、モデル検査部１５に対応する。また、処理手順モデル生成ステップは、実施の形態における処理Ｓ１２に対応する。また、処理手順モデル変更ステップは、実施の形態における処理Ｓ１３に対応する。また、処理手順モデル検証ステップは、実施の形態における処理Ｓ１４に対応する。
【００６７】
（付記１）  検証対象プログラムの検証を行うプログラム検証方法をコンピュータに実行させるプログラム検証プログラムであって、
前記検証対象プログラムの処理手順を記述した処理手順モデルを生成する処理手順モデル生成ステップと、
メモリーコンシステンシーモデルに基づいて、前記処理手順モデルに処理手順を追加する処理手順モデル変更ステップと、
前記処理手順モデルの検証を行う処理手順モデル検証ステップと、
をコンピュータに実行させるプログラム検証プログラム。
（付記２）  付記１に記載のプログラム検証プログラムにおいて、
前記処理手順モデル変更ステップは、前記処理手順モデルにおいて前記メモリーコンシステンシーモデルにより非決定的となる部分を検出し、該部分に別の発生し得る前記処理手順を追加することを特徴とするプログラム検証プログラム。
（付記３）  付記１または付記２に記載のプログラム検証プログラムにおいて、
前記非決定的となる部分は、前記メモリーコンシステンシーモデルにより順序の変更が許可された命令列の部分であり、前記別の処理手順は、前記命令列の順序を変更した処理手順であることを特徴とするプログラム検証プログラム。
（付記４）  付記１乃至付記３のいずれかに記載のプログラム検証プログラムにおいて、
前記処理手順モデルは、状態機械であることを特徴とするプログラム検証プログラム。
（付記５）  付記１乃至付記４のいずれかに記載のプログラム検証プログラムにおいて、
前記検証対象プログラムは、並列プログラムまたは並行プログラムであることを特徴とするプログラム検証プログラム。
（付記６）  付記１乃至付記５のいずれかに記載のプログラム検証プログラムにおいて、
前記処理手順モデル変更ステップは、予めメモリーコンシステンシーモデルの候補を記憶しておき、ユーザの指示に従って候補の中から１つを選択することにより前記メモリーコンシステンシーモデルを設定することを特徴とするプログラム検証プログラム。
（付記７）  付記６に記載のプログラム検証プログラムにおいて、
前記メモリーコンシステンシーモデルの候補は、ＴＳＯ、ＰＳＯのいずれかを含むことを特徴とするプログラム検証プログラム。
（付記８）  付記１乃至付記７のいずれかに記載のプログラム検証プログラムにおいて、
前記処理手順モデル変更ステップは、ユーザの指示に従って、ロード命令、ストア命令、同期命令の順序制約を定義することにより前記メモリーコンシステンシーモデルを設定することを特徴とするプログラム検証プログラム。
（付記９）  検証対象プログラム検証を行うプログラム検証装置であって、
前記検証対象プログラムの処理手順を記述した処理手順モデルを生成する処理手順モデル生成部と、
メモリーコンシステンシーモデルに基づいて、前記処理手順モデルに処理手順を追加する処理手順モデル変更部と、
前記処理手順モデルの検証を行う処理手順モデル検証部と、
を備えてなるプログラム検証装置。
（付記１０）  付記９に記載のプログラム検証装置において、
前記処理手順モデル変更部は、前記処理手順モデルにおいて前記メモリーコンシステンシーモデルにより非決定的となる部分を検出し、該部分に別の発生し得る前記処理手順を追加することを特徴とするプログラム検証装置。
（付記１１）  付記９または付記１０に記載のプログラム検証装置において、
前記非決定的となる部分は、前記メモリーコンシステンシーモデルにより順序の変更が許可された命令列の部分であり、前記別の処理手順は、前記命令列の順序を変更した処理手順であることを特徴とするプログラム検証装置。
（付記１２）  付記９乃至付記１１のいずれかに記載のプログラム検証装置において、
前記処理手順モデルは、状態機械であることを特徴とするプログラム検証装置。
（付記１３）  付記９乃至付記１２のいずれかに記載のプログラム検証装置において、
前記検証対象プログラムは、並列プログラムまたは並行プログラムであることを特徴とするプログラム検証装置。
（付記１４）  付記９乃至付記１３のいずれかに記載のプログラム検証装置において、
前記処理手順モデル変更部は、予めメモリーコンシステンシーモデルの候補を記憶しておき、ユーザの指示に従って候補の中から１つを選択することにより前記メモリーコンシステンシーモデルを設定することを特徴とするプログラム検証装置。
（付記１５）  付記１４に記載のプログラム検証装置において、
前記メモリーコンシステンシーモデルの候補は、ＴＳＯ、ＰＳＯのいずれかを含むことを特徴とするプログラム検証装置。
（付記１６）  付記９乃至付記１５のいずれかに記載のプログラム検証装置において、
前記処理手順モデル変更部は、ユーザの指示に従って、ロード命令、ストア命令、同期命令の順序制約を定義することにより前記メモリーコンシステンシーモデルを設定することを特徴とするプログラム検証装置。
（付記１７）  検証対象プログラムの検証を行うプログラム検証方法であって、
前記検証対象プログラムの処理手順を記述した処理手順モデルを生成する処理手順モデル生成ステップと、
メモリーコンシステンシーモデルに基づいて、前記処理手順モデルに処理手順を追加する処理手順モデル変更ステップと、
前記処理手順モデルの検証を行う処理手順モデル検証ステップと、
を実行するプログラム検証方法。
（付記１８）  付記１７に記載のプログラム検証方法において、
前記処理手順モデル変更ステップは、前記処理手順モデルにおいて前記メモリーコンシステンシーモデルにより非決定的となる部分を検出し、該部分に別の発生し得る前記処理手順を追加することを特徴とするプログラム検証方法。
（付記１９）  付記１７または付記１８に記載のプログラム検証方法において、
前記非決定的となる部分は、前記メモリーコンシステンシーモデルにより順序の変更が許可された命令列の部分であり、前記別の処理手順は、前記命令列の順序を変更した処理手順であることを特徴とするプログラム検証方法。
（付記２０）  付記１７乃至付記１９のいずれかに記載のプログラム検証方法において、
前記処理手順モデルは、状態機械であることを特徴とするプログラム検証方法。
【図面の簡単な説明】
【００６８】
【図１】本発明に係るプログラム検証装置の構成の一例を示すブロック図である。
【図２】本発明に係るプログラム検証装置の動作の一例を示すフローチャートである。
【図３】本発明に係る状態機械変更部の動作の一例を示すフローチャートである。
【図４】本発明に係る検証対象プログラムの構成の一例を示すブロック図である。
【図５】本発明に係る検証対象プログラムの一例を示すソースコードである。
【図６】メモリーコンシステンシーモデルがＴＳＯである場合の順序制約の一例を示す表である。
【図７】メモリーコンシステンシーモデルがＰＳＯである場合の順序制約の一例を示す表である。
【図８】本発明に係る状態機械作成部により抽出されたＰｒｏｄｕｃｅｒの処理の一例を示す表である。
【図９】本発明に係る状態機械作成部により抽出されたＣｏｎｓｕｍｅｒの処理の一例を示す表である。
【図１０】本発明に係る状態機械作成部により作成されたＰｒｏｄｕｃｅｒのＦＳＭの一例を示す状態遷移図である。
【図１１】本発明に係る状態機械作成部により作成されたＣｏｎｓｕｍｅｒのＦＳＭの一例を示す状態遷移図である。
【図１２】本発明に係る状態機械変更部により変更されたＰｒｏｄｕｃｅｒのＦＳＭの一例を示す状態遷移図である。
【図１３】本発明に係る状態機械変更部により合成されたＦＳＭの一例を示す状態遷移図である。
【図１４】プログラムの記述における命令列の順序の一例を示す図である。
【図１５】プログラムの処理における命令列の順序の一例を示す図である。
【符号の説明】
【００６９】
１４  検証項目設定部、１５  モデル検査部、１６  検証結果表示部、２１  検証対象プログラム取得部、２２  状態機械作成部、２３  メモリーコンシステンシーモデル設定部、２４  状態機械変更部、３１  Ｐｒｏｄｕｃｅｒ、３２  バッファ、３３  Ｃｏｎｓｕｍｅｒ。
【図１】
2006277580.tif 000003
【図２】
2006277580.tif 000004
【図３】
2006277580.tif 000005
【図４】
2006277580.tif 000006
【図５】
2006277580.tif 000007
【図６】
2006277580.tif 000008
【図７】
2006277580.tif 000009
【図８】
2006277580.tif 000010
【図９】
2006277580.tif 000011
【図１０】
2006277580.tif 000012
【図１１】
2006277580.tif 000013
【図１２】
2006277580.tif 000014
【図１３】
2006277580.tif 000015
【図１４】
2006277580.tif 000016
【図１５】
2006277580.tif 000017