(57)【要約】【課題】コンカレントシステムにおいて、異なったスレッドまたはプロセスからの遷移のインターリービングの数が増えないようにする。【解決手段】コンカレントシステムのための、記号的部分的命令低減を行うシステムおよび方法は、条件または述語が当てはまるとき、一群の条件について独立である異なったスレッドからの遷移を含む、保護された独立関係を求めることを含む。部分的命令低減は、保護された独立状態が続くとき、冗長なスレッドインターリービングを自動的に取り除くことを許すために、保護された独立関係を用いて行なわれる。【選択図】図３
2009087356.tif 000002
【特許請求の範囲】
【請求項１】
コンカレントシステムのための、記号的部分的命令低減を行う方法であって、
条件または述語が当てはまるとき、一群の条件について独立である異なったスレッドからの遷移を含む、保護された独立関係を求めることと、
保護された独立状態が続くとき、冗長なスレッドインターリービングを自動的に取り除くことを許すために、保護された独立関係を用いて部分的命令低減を行うこと、
を有する方法。
【請求項２】
保護された独立関係を求めることが、スレッド遷移の全ての対間の、潜在的なコンフリクトを静的に計算することを含む、請求項1に記載の方法。
【請求項３】
独立したスレッド遷移の対を共通の独立条件とマージすることによって、前記の保護された独立関係の表現の大きさを小さくすることをさらに有する、請求項１に記載の方法。
【請求項４】
従属したスレッド遷移対を符号化することによって、前記の保護された独立関係の表現の大きさを小さくすることをさらに有する、 請求項１に記載の方法。
【請求項５】
コンピュータ上で実行させられると、請求項１に記載のステップを該コンピュータに行わせる、コンピュータ読み取り可能な媒体。
【請求項６】
コンカレントシステムのための、記号的部分的命令低減を行う方法であって、
異なったスレッドの遷移間の独立関係を求めることと、
冗長なスレッドインターリービングを自動的に取り除くことを許すために、前記の独立関係に基づいて状態における遷移の有限のウインドウに制約を課すピープホール符号化を用いて部分的命令低減を行うこと、
を有する方法。
【請求項７】
前記独立関係は、保護された独立関係を含む、請求項６に記載の方法。
【請求項８】
前記の独立関係を求めることが、スレッド遷移の全ての対間の潜在的なコンフリクトのセットを静的に計算することを含む、請求項７に記載の方法。
【請求項９】
独立したスレッド遷移の対を共通の独立条件とマージすることによって、前記の保護された独立関係の表現の大きさを小さくすることをさらに有する、請求項７に記載の方法。
【請求項１０】
従属したスレッド遷移対を符号化することによって、前記の保護された独立関係の表現の大きさを小さくすることをさらに有する、請求項７に記載の方法。
【請求項１１】
前記ピープホール符号化は、充足可能性モジュロ理論/プール充足可能性（SMT/SAT）によって行われるサーチの間、冗長なスレッドインターリービングを自動的に取り除くことを許すために、制約を加える、請求項６に記載の方法。
【請求項１２】
前記ピープホール符号化が、トランザクション境界におけるスレッド間のコンテクスト切替を示す遷移に対してのみ加えられる、コンカレントシステムのトランザクション境界を求めることをさらに有する、請求項１１に記載の方法。
【請求項１３】
設計エラーを見つけるために前記コンカレントシステムの、境界のあるモデルチェックに基づくSMT/SATの間、記号的部分的命令低減を行うことをさらに有する、請求項1１に記載の方法。
【請求項１４】
前記ピープホール符号かは、２つのスレッドを有するプログラムのためのスレッドインターリービングの最適な低減を保証する制約を出力する、請求項６に記載の方法。
【請求項１５】
前記ピープホール符号化が、トランザクション境界におけるスレッド間のコンテクスト切替を示す遷移に対してのみ加えられる、コンカレントシステムのトランザクション境界を求めることをさらに有する、請求項６に記載の方法。
【請求項１６】
コンピュータ上で実行させられると、請求項６に記載のステップを該コンピュータに行わせる、コンピュータ読み取り可能な媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明はコンカレントシステムの検証に関し、特に、保護された独立関係を有するピープホール部分的命令低減を用いたプログラム検証システムおよび方法に関する。
【０００２】
この出願は、2007年10月2日に出願された仮出願第60/976,871号に対する優先権を主張し、ここに参照によって組み込む。
【背景技術】
【０００３】
マルチスレッド化された(multi-threaded)プログラムを検証することは、異なったスレッドからの遷移(transition)のインターリービング(interleaving)の、潜在的に大きな数のために難しい問題である。明示状態のモデル検査（explicit-state model checking）において、独立した遷移のインターリービングの等価物を利用する部分的命令低減（POR）技術が、サーチ状態空間を減らすために用いられている。２つの遷移が従属しているかどうか決定することは、検証問題自体を解決することと同じく難しいので、持続的なセット(persistent sets)（頑固なセット(stubborn sets)を含む）またはスリープセットは、従属的な遷移を保守的な（したがって厳密でない）方法で事前に計算する静的解析を用いる必要があることが多い。
【０００４】
動的部分的命令低減は、持続的なセットを動的なコンフリクト(collision) 検出でオンザフライ(on-the fly)に計算することによって演繹的に静的解析を適用する必要性を高める。本方法は、ステーレスサーチ（stateless search）を実行し、サイクルフリー(cycle-free)なシステムに限定され、それをステートフルサーチ(stateful search)に拡大し、それを記号的(symbolic)方法と組み合わせる方法は困難であることがわかった。
【０００５】
SATベースの境界のあるモデルチェック(bounded model checking: BMC)のような記号的方法の主要な強みは、コンフリクト条項(conflict clauses)と非年代順のバックトラッキング(non-chronological backtracking)の追加によって特性依存サーチ空間(property dependent search space)の低減がブール(Boolean)、すなわち命題充足可能性(SAT)または充足可能性モジュロ理論(SMT)ソルバー(solver)内で自動的に利用されることである。実際、記号的な方法は明示状態の方法よりも、データ(例えば、大きなドメインを有する変数)を処理する上でより効率的である。明示状態モデルチェックは、SATとSMTのソルバーによってもたらされる上記の低減から利益を享受しない。持続セットベースの方法(および明示状態低減方法)を記号的モデルチェックと組み合わせることは容易な仕事ではない。
【０００６】
この難しさは、明示状態モデルチェックが、具体的な状態を個々に検査し、一方記号的方法が通常、状態の非常に大きなセットを暗黙に扱うことから生ずる。特に、パスのセットに対して動的に独立である遷移は、単一のパスに対して動的に独立である遷移よりも捕らえ、利用するのがより難しい。
【０００７】
図１において、例えば、２つの同時に起動しているスレッドがグローバルアレイaをアクセスし、２つのポインターｐとｑがエイリアスされている(aliased)。スレッドT1は３つの遷移tAtBtCを有している。スレッドT2は３つの遷移tαtβtγを有している。静的に、tA、tBはtα、tβとのコンフリクトを有している。しかしながら、もしある実行パス(i≠j)においてホールドすると、tA、tBはtα、tβは独立した遷移になり、このことは２つの実行シーケンス
【０００８】
【数１】
2009087356.tif 000003
【０００９】
が等価であることを意味している。残念なことに、この情報は既存の記号的な部分的命令低減方法によっては捉えることができない。例えば、この従来の方法は、もしi＝foo()とj=bar()がi＝１、j=２に代わると、上記の等価なインターリービングを検出し、利用できるが、これは一般的なケースではない。
【００１０】
明示的状態モデルチェックでは、保守的な静的分析に頼る従来の部分的命令低減方法はそのような条件付き等価(conditional equivalence)を利用する可能性が低い。動的部分的命令低減方法は、コンフリクトをオンザフライに検出することによってこれを改善する。適応的サーチ内の各具体的状態において、ｉとｊ(およびｐとｑ)の値は完全に求められ、(特定のパスに関しての)コンフリクトを検出するのがより容易になる。しかしながら、("happens-before"の考え方に基づく)この技術を記号的符号化と直接、組み合わせることは容易ではない。
【００１１】
記号的アルゴリズムでは、モデルチェッカーは、低減されたセットの実行を徹底的に調べる必要があるので、これらの種類の動的部分的命令低減を逃すことは高価なものとなる。マルチスレッド化されたプログラムＰが、各スレッドが多くともｋ個のステップを実行するn個のスレッドを有すると仮定する。すると、Ｐの全実行数は
【００１２】
【数２】
2009087356.tif 000004
【００１３】
と大きい。起動している例の場合、図２の格子構造を用いて全ての考えられるインターリービングを捉えることができる。
【００１４】
【数３】
2009087356.tif 000005
【００１５】
を２つのスレッド内の遷移のセットとする。格子の各頂点は、既に実行された複数の遷移からなる、transの明確なサブセットを表している。頂点のセットはパワーセット2Qを構成し、上の頂点は[]であり、下の頂点は
【００１６】
【数４】
2009087356.tif 000006
【００１７】
である。上から下へのパスは固有のインターリービングを示している。例えば、最も左のラインは
【００１８】
【数５】
2009087356.tif 000007
【００１９】
に対応している。
【発明の開示】
【発明が解決しようとする課題】
【００２０】
コンカレントシステムでは、異なったスレッドまたはプロセスからの遷移のインターリービングの数は非常に大きくなることがある。検証の間に冗長なインターリービングを削る、既存の部分的命令低減方法は正確には十分ではなく、記号的実行に適していない。
【課題を解決するための手段】
【００２１】
コンカレントシステムのための、記号的部分的命令低減を行うシステムおよび方法は、条件または述語が当てはまるとき(a condition or predicate holds)、一群の条件について独立である異なったスレッドからの遷移を含む、保護された独立関係を求めることを含む。部分的命令低減は、保護された独立状態が続くとき、冗長なスレッドインターリービングを自動的に取り除くことを許すために、保護された独立関係を用いて行なわれる。
【００２２】
コンカレントシステムのための、記号的部分的命令低減を行うシステムおよび方法は、異なったスレッドの遷移間の独立関係を求めることと、冗長なスレッドインターリービングを自動的に取り除くことを許すために、前記の独立関係に基づいて状態における遷移の有限のウインドウに制約を課すピープホール符号化を用いて部分的命令低減を行うことを含む。
【００２３】
コンカレントシステムのための、記号的部分的命令低減を行うシステムおよび方法は、保護された独立条件が当てはまる独立したトランザクションを含む、保護された独立関係を求めることを含む。
【００２４】
部分的命令低減は、保護された独立条件が満たされたとき、SMTソルバー内の冗長なインターリービングを自動的に取り除くことによって、SAT/充足可能性モジュロ理論(SMT)ソルバー内で部分的命令低減を容易にするためにピープホール充足可能性(SAT)を用いて行われる。
【００２５】
これらおよび他の特徴および利点は、添付の図面と関連して読まれるべぃ、例示的実施形態の以下の詳細な説明から明らかとなる。
【発明を実施するための最良の形態】
【００２６】
本開示は、図面を参照して好適な実施形態の以下の記述の詳細をもたらす。
【００２７】
本原理に従って、「保護された独立関係(GIR)」が、動的な独立遷移を簡潔な方法で正確に捉えるために提供される。本実施形態を、GIRを一群の制約として符号化する方法である「ピープホール(peephole)部分的命令低減」すなわちPPORと呼ぶ。2つのスレッドを有するシステムでは、GIR/PPOR方法は冗長ないかなるインターリービングの除去を保証する。従来技術の既存の方法によるそのような保証はない。
【００２８】
GIRとPPORの組み合わせは、SMT/SATソルバーを用いた記号的実行に良く適しており、(持続的セットに基づく)従来のPOR方法は記号的実行にはあまり適していない。
【００２９】
新しい記号的符号化方式とSMTソルバーが、遷移の動的独立を捉え、利用するために提供される。保護された独立関係(GIR)では、保護制約CGが持続するとき、各
【００３０】
【数６】
2009087356.tif 000008
【００３１】
が遷移の保護された独立な対t1、t2に対応するRGが導入される。これは、単一の状態または全ての状態のいずれかに対して定義された、(条件付き)独立関係の標準的な定義の延長である。保護CGは、単にローカルな制御状態ではなく、ローカルおよびグローバルなデータ状態(値)を指す述語である。保護された独立関係に基づいて、動的に独立な遷移を、抑制されたモデルチェックにおける充足可能性式を制限する制約として簡潔に取得するピープホール低減が提供される。ピーホール命令低減では、GIR制限を追加することは、一定の大きさの時間ウインドウのみ(例えば大きさ２)におけるパターンを識別する必要があり、したがって将来の衝突を検出しなければならない負担を和らげる。追加されたGIR制約は、SMTソルバーがサーチ状態空間を自動的に削ることを可能にする。より高速な認証実行時間(およびより大きなシステムを検証する能力)が与えられている。実験によって、GIR/PPORが検証実行時間を著しく減らせることがわかった。
【００３２】
ここに記載する実施形態はハードウェアのみ、ソフトウェアのみ、あるいはハードウェア要素とソフトウェア要素の両方を含んでいてよい。好適な実施形態では、本発明は、ファームウエア、常駐ソフトウェア、マイクロコードなどを含むが、これらに限定されないソフトウェアで実施することができる。
【００３３】
実施形態は、コンピュータによってあるいはコンピュータまたは他の命令実行システムに関連して使用されるプログラムコードを与えるコンピュータで使用可能なまたはコンピュータで読み取り可能な媒体からアクセス可能なコンピュータプログラムプロダクトを含む。コンピュータで使用可能なまたはコンピュータで読み取り可能な媒体は、命令実行システム、装置、デバイスによってまたはこれらと関連して使用されるプログラムを格納し、通信し、伝播させ、あるいは搬送するあらゆる装置を含む。媒体は、磁気的、光学的、電子的、電磁的、赤外線の、または半導体のシステム（または装置またはデバイス）また伝播媒質でありうる。媒体は、半導体またはソリッドステートのメモリ、磁気テープ、取り外し可能なコンピュータディスケット、ランダムアクセスメモリ（RAM）、リードオンリメモリ（ROM）、リジッドな磁気ディスク、光学ディスク等のコンピュータ読み取り可能な媒体を含む。
【００３４】
同じ番号が同じまたは類似の要素を示す図、そして最初に図3を参照すると、一実施形態による、プログラム検証流れの方法/システム10を示すブロック/流れ図が示されている。マルチスレッド化されたプログラムがブロック10内に設けられている。該マルチスレッドはスレッド同士間にコンフリクトが存在するかどうか判定するように検証される必要がある。マルチスレッド化されたプログラムは、各々が該プログラムを完全に検証するように検査される必要がある非常に多くの実行可能なスレッド実行を有している。マルチスレッド化されたプログラムは、ブロック18に入れられ、マルチスレッド化されたプログラム12のための保護された独立関係(GIR)情報20を計算する。ブロック18において、GIR情報を計算する方法は、SAT符号化に基づく記号的部分的命令低減のために用いられる。保護された全ての独立な遷移の対は、2つの遷移が独立である条件と共に、プログラムコントロールフローグラフを横切ることによって集められる。
【００３５】
保護された独立な遷移、すなわち、ある（しかし全てではない）実行パスにおいて独立であると見做すことができる遷移は、新しい記号符号化方式を用いることによって取得できる。新しい符号化方式は、部分的変数割り当て（すなわち、SMT/SATソルバーによってこの点まで具体的な値が割り当てられた変数）が、保護された,いくつかの独立の条件を真に評価させる(evaluate to true)とき、SMT/SATソルバー内で冗長なインターリービングを自動的に取り除くこと可能にする簡潔な制約を追加する。
【００３６】
GIR情報20とマルチスレッド化されたプログラム12に基づいて、ピープホール部分的命令削減（PPOR）符号化がブロック14において行われる。部分的命令削減（POR）は、検証において冗長なスレッド実行を取り除く方法である。PORによって、全てのスレッドの実行に対して、冗長でないスレッドの実行だけが検査される必要がある。本原理によるPPORは、2つのスレッドを有するプログラムに対して低減最適性を保証する。すなわち、全ての冗長なスレッド実行が除かれる。既存の方法はこのことを保証できない。PPORはSATベースの記号符号化に良く適している。PPORは従来技術の方法よりも効率的であり、結果は、サイズがもっと小さいSAT式である。
【００３７】
ブロック14の出力は、解くためにブロック22に与えられる充足可能性（SMT/SAT）式16である。ブロック30は、充足可能性式16を解くためにソルバー、例えばSMTソルバーを用いる。ブロック22が、式16が充足可能であると判定すると、バグ24が発見される。式16がブロック22において充足可能でないと、プログラムはブロック14に戻って他の式を生成する。本プロセスは、全てのバグが発見され、式が充足可能になるまで繰り返される。
【００３８】
定義1：関係式
【００３９】
【数７】
2009087356.tif 000009
【００４０】
は、全ての〈t1,ｔ2〉∈Rについて、全てのグローバルステートｓ∈Sに対して次の2つの特性が当てはまるとき、かつあてはまるときに限り独立関係である。ｔ1がｓおよび
【００４１】
【数８】
2009087356.tif 000010
【００４２】
においてイネーブルにされると、t2は、t2がｓ'においてイネーブルにされたときだけｓにおいてイネーブルにされる。ｔ1とt2がｓにおいてイネーブルにされると、
【００４３】
【数９】
2009087356.tif 000011
【００４４】
となるような固有の状態ｓ'が存在する。すなわち、独立な複数の遷移は互いにディセーブルにもイネーブルにもすることはできず、イネーブルにされた複数の独立な遷移が代る。本定義は、どの遷移が独立であるかを判断するために全ての状態についての上記の2つの特性をチェックすることは実際的ではないので、主として意味論的使用(semantic use)である。
【００４５】
持続的セットをベースとする方法では、各状態に対して、持続的セットと呼ばれるイネーブルにされた遷移のサブセットを計算し、適応的サーチでは持続的セット内の遷移を調べるだけである。遷移は、もしそれが他のスレッドの（おそらく無限の）未来とリードーライトのコンフリクトとライトーライトのコンフリクトを有するならば、持続的セットに入れられる。２つの遷移が従属しているかどうか正確に決定することは、内在する検証の問題を解決するのと同じくらい難しいので、従来、衝突(collision)検出は、固有の近似がより粗い持続的セットにつながることが多い静的解析を用いる。例えば、静的にチェックが容易な十分な条件が実際上記の条件、すなわち１）ｔ1の間アクティブであるスレッドのセットが、ｔ2の間アクティブであるスレッドのセットから外れているか、２）ｔ1によってアクセスされたオブジェクトのセットがｔ1によってアクセスされたオブジェクから外れている、を取り替えるのに用いられてきた。
【００４６】
そのような条件は、a［i］とa[j]が同じアレイ要素を指すかどうか先験的には明らかではないので、i≠ｊのとき、t1:[i]=ei およびt2:[i]=e2のような幾つかの独立な遷移を見逃すことがある。条件付き従属関係（conditional dependence relation）では、2つの遷移が、全てのs∈Sに対して単一の状態s∈Sに関して独立であると定められる。そのような拡張は、持続的セットが各グローバル状態s∈Sに対して計算できる明示的状態モデルチェックに合うように調整される。条件付き従属関係、例えば条件付きの確固としたセット(stubborn set)およびより最近の動的な部分的命令低減を利用する既存の方法が存在する。しかしながら、それらの両方とも明示的状態方法であり、これらの技術を記号モデルチェックに直接、適用する方法は明らかではない。動的な部分的命令低減方法はステートレスサーチを行い、サイクルフリーのシステムに限定される。さらに、全ての独立な遷移が静的に特定されても、持続的セットをベースとする方法は、依然として低減を逃すことがある。
【００４７】
これに対して、保護された独立関係の新しい考え方に基づく本方法は、著しくより多くの低減をもたらすことが多い。システム内にたった2つのスレッドが存在する特別なケースでは、本方法は全ての冗長なインターリービングを除去するのを保証する。
【００４８】
保護された独立関係：定義２：2つの遷移は条件cG（ローカルおよびグローバルな変数に対する述語）に関して独立して保護されている。すなわち〈t1,t2,cG〉∈RG、cGが有効(hold)であるときおよびそのときに限り、次の特性、すなわち、1)ｔ1がｓおよび
【００４９】
【数１０】
2009087356.tif 000012
【００５０】
においてイネーブルにされると、t2 は、t2がｓ'においてイネーブルにされたときのみｓにおいてイネーブルにされる、そして２）t1とt2がｓにおいてイネーブルならば、
【００５１】
【数１１】
2009087356.tif 000013
【００５２】
になるような固有の状態ｓ'が存在する、
がすべてのs∈Sに当てはまる。保護された独立関係の該2つの特性は、組(tuple)（t1,t2,s）が単一の状態s∈Sに関して定義され、その使用を明示的状態空間の調査に制限する、条件付き従属関係の延長である。本ケースでは、独立は、cGが有効である、すなわち状態の（おそらく大きな）セットに関してである全ての状態について有効である。
【００５３】
金のかかる計算コストのために定義1における特性を近似する以前の明示的部分的命令低減技術と異なり、SMT/SATソルバーを用いて定義2における特性を用いることができる。SMT/SATソルバーの、値を暗黙に推論する能力のために、そのような保護された独立関係は、充足可能性の式に対する追加の制約として捉えることができる。これらの制約は、SMT/SATソルバー内で状態空間を自動的に取り除くのを容易にする。保護された独立状態cGはプログラムの構造から容易に導きだせる。
【００５４】
遷移ｔについて、ｔによって読まれる変数のセットを示すｖRD(t)を用い、tによって書かれる変数のセットを示すｖRW(t)を用いる。t1とt2の間の潜在的なコンフリクトを
【００５５】
【数１２】
2009087356.tif 000014
【００５６】
と定義する。
【００５７】
実行中の例（図1）において、
【００５８】
【数１３】
2009087356.tif 000015
【００５９】
さて、保護された独立チュープル(tuples)を計算する異なったシナリオを以下に列挙する。
【００６０】
１）
【００６１】
【数１４】
2009087356.tif 000016
【００６２】
のとき、〈ｔ1,t2,true〉をRGに入れる。
【００６３】
２）a[i],a[j]がアレイアクセスである
【００６４】
【数１５】
2009087356.tif 000017
【００６５】
のとき、〈ｔ1,t2,i≠j〉をRGに入れる。
【００６６】
３）pi, pjが、別名である(aliased)ことがあるポインターである
【００６７】
【数１６】
2009087356.tif 000018
【００６８】
のとき、〈t1,t2,ｐi≠ｐj〉をRGに入れる。
【００６９】
４）
【００７０】
【数１７】
2009087356.tif 000019
【００７１】
のとき、次のケースを考慮する。
【００７２】
ａ）RD-WR：ｘ∈VRD(t1)で、割当てｘ：=eがｔ2に現れると、〈ｔ1,t2,x=e〉をRGに入れる。
【００７３】
ｂ）WR-WR：ｘ：＝e1がｔ1に現れ、ｘ：＝e2がｔ2に現れると、〈ｔ1、t2,e1=e2〉をRGに入れる。
【００７４】
ｃ）WR-C：ｘが、while(cond)のようなｔ1の保護condに現れ、ｘ：＝eがｔ2に現れると、cond［x→e］がxのeへの置換を示す、〈t1,t2,cond=cond[x→e]〉をRGに入れる。
【００７５】
パターン4(a)は、同じ変数に対する2つのリード・ライト操作が、ライトが該変数の値を変えなければ独立と保護されると述べている。パターン4(ｂ)は、同じ変数に対する２つのライト操作が、それらの新しく割り当てられた値が同じであるならば独立と保護されると述べている。これらのケースにおいて、これらの共通の変数の多くが、特にそれらが制御目的のために用いられるとき、小さい範囲を有するので、cGはしばしば正確に見積もる。ｂがブール変数であるならば、ｂ：＝ｅ1とｂ：＝e2は、保護された独立である50％の確率を有する。パターン4(c)は、4(a)の特別なケースである。x=eがcond=cond[x→e]を暗示することは事実であるが、x≠eでcond=cond[x→e]であるケースがある。もし（x＜10）がスレッド1における遷移で、x：＝eがスレッド２における遷移ならば、それらは、xの値が割当ての後異なっていたとしても、(x＜10)=(e<10)である限り、保護された独立である。
【００７６】
多数のパターンが遷移の同じ対に現れることがある。そのような場合、全体条件は個々の条件の結合または分離である。例えば、t1：もし(a[i]>5）でt1：a[j]:=xならば、cGはi≠jV(a[i]>5)=(x>5)と定義される。
【００７７】
制限のあるモデルチェック（BMC）：ここで提示する、制限のあるモデルチェックはSATをベースとするのが好ましい。サーチ空間を小さくするためにGIRを簡潔に符号化する記号的部分的命令低減が提示される。
【００７８】
マルチスレッド化されたプログラムと到達可能性(reachability)特性が所与のものとして、該プログラムの全ての実行パス上で該特性を最大で一定深度Ｋまで調べる。各ステップ0≦k≦Kについて、該特性に反する、長さkのインターリービング実行が存在するときかつ存在するときに限りψが満足できるように式ψを形成する。与えられた、広がる(unrolling)深さkでは、BMCのケースはψ=φ∧φpropであり、ここでψは、最大でkステップまでの、該プログラムの考えられる全てのインターリービングを表し、φpropは、該与えられた特性が破られた（violated）ことを示す制約である。該特性は式φpropへ符号化される必要がある。以下において、ψの形成に着目する。
【００７９】
Vを状態変数のセット
【００８０】
【数１８】
2009087356.tif 000020
【００８１】
とし、ここでVglobalはグローバル状態変数を含み、VlはスレッドTlにローカルな状態変数を含む。全てのプログラム変数について、状態変数をVlまたはVglobalのいずれかを割り当てる。アレイアクセスおよびポインターアクセスは特別な操作を必要とする。アレイアクセスa［i］について、インデックスiに対して状態変数を、コンテントa［i］に対して他の状態変数を割り当てる。同様に、ポインターアクセス*pに対して、(*p)とｐに対する個別の状態変数を割り当てる。各スレッドTiについてその現在のプログラム場所を表すためにpci変数を加える。非決定性(nondeterministic)のスケジューラーを形作るために、領域がN個のスレッドに対して[1,2,…,N]である変数selを加える。スレッドTiにおける遷移がsel＝iのときのみ実行される。
【００８２】
長さがkの全ての考えられるインターリービングを表すために、個々のスレッドとスケジューラーの遷移関係を符号化し、構成されたシステムを正確にk個の時間フレーム展開する必要がある。このために、全ての時間フレームにおいて、状態変数の新たなコピーを追加する。νl∈Vlが、i番目の時間フレームにおけるν∈Vのコピーを示すとする。
【００８３】
【数１９】
2009087356.tif 000021
【００８４】
ここで、I(V0)は初期状態のセットを表し、SCHはスケジューラーの遷移関係を表し、TRjはスレッドTjの遷移を表す。ここで、SCHとTRjに対する定式化を考える。
【００８５】
スレッド：オリジナルプログラム(例えば、C言語のような言語で書かれた)が簡単なアサインメント(assignments)と分岐命令のみを有するプログラムに簡単化される前処理が存在すると仮定する。同様の仮定が、従来技術で知られている、SLAM、BLAST、Ｆ-Softのような他の検証ツールにおいてなされた。VSj＝Vglobal∪VjがスレッドTjに見える変数のセットとする。i番目の時間フレームにおいて、制御場所loc1からloc2にあるあらゆる遷移t∈transjについて、制約
【００８６】
【数２０】
2009087356.tif 000022
【００８７】
を次のように生成する。
１．tが割り当てｖ：=eならば、
【００８８】
【数２１】
2009087356.tif 000023
【００８９】
【数２２】
2009087356.tif 000024
【００９０】
２.tが、if(c)またはwhile(c)におけるように、条件ｃならば、
【００９１】
【数２３】
2009087356.tif 000025
【００９２】
【数２４】
2009087356.tif 000026
【００９３】
全遷移関係
【００９４】
【数２５】
2009087356.tif 000027
【００９５】
は
【００９６】
【数２６】
2009087356.tif 000028
【００９７】
と定義され、ここで、第2項は、スレッドTjが実行のために選択されないと、Vjにおけるローカル変数は、それらの値を変えない(他の変数は制約されない)。
【００９８】
スケジューラー：スケジューラーの遷移関係をSCH(V)：＝（sel＝*）と表す。他の制約がなければ、SCH=trueであり、これは、selがあらゆるステップにおいて任意の値を取ることを意味する。このデフォルトSCHは全ての考えられるインターリービングを考慮する。部分的命令低減は、冗長なインターリービングを除くためにSCHに制約を付加することによって実行することができる。
【００９９】
ピープホール部分的命令低減：長さkの2つの実行シーケンスが同じ等価クラスにあると、それらの1つだけが特性違反ないかチェックされなければならない。そのような部分的命令低減を達成するために、保護された独立な遷移の各対について、スケジューラーを制限するためにSCHにいくらかの制約を付加する。t1∈transiでt2∈transj (i<j)である組(tuple)〈t1,t2,x=e〉∈RGの場合、SCHに次の制約を結合させる。
【０１００】
【数２７】
2009087356.tif 000029
【０１０１】
ここで、
【０１０２】
【数２８】
2009087356.tif 000030
【０１０３】
はk番目の時間フレームにおいてt1とt2がイネーブルにされる条件である。遷移t1とt2が独立で、両方ともイネーブルにされると、t1から始まるスケジュールを調べ、そしてt2から始まるスケジュールを調べる。しかし、上記の制約は、独立な遷移t1、t2をスケジューリングする優先度に対し一定の順序を押し付ける。次の2つの等価なシーケンス…;t1、t2;…と…;t2、t1;…は等価であるので、2つの独立な遷移がそれらのスレッドインデックス順序、すなわち、i＜ｊならばt1がt2の前にある順序でスケジューリングされる。冗長なインターリービングだけの除去を示す、図4に示されているように、制約
【０１０４】
【数２９】
2009087356.tif 000031
【０１０５】
を追加することによって第2のシーケンスを禁止る。インターリービング202は冗長で、除去される。
【０１０６】
現行の例（図1）において、k番目の時間フレーム(０≦k≦K)において
【０１０７】
【数３０】
2009087356.tif 000032
【０１０８】
i≠jのとき、
【０１０９】
【数３１】
2009087356.tif 000033
【０１１０】
で始まる全てのシーケンスが除去される。しかし、付加された制約は、
【０１１１】
【数３２】
2009087356.tif 000034
【０１１２】
で始まるシーケンスを除去しない。SCHは最初、スレッドの考えられる全てのインターリービングを含む。GIR制約を付加することによって除去されたあらゆるインターリービング
【０１１３】
【数３３】
2009087356.tif 000035
【０１１４】
について、等価なインターリービング
【０１１５】
【数３４】
2009087356.tif 000036
【０１１６】
が常に存在したままである。ピープホール低減(PPOR)によって除去された全てのインターリービングは冗長で、2つのスレッドの場合、ピープホール低減は図5に示されているようにSCHから全ての冗長なインターリービングを除去する。3つ以上のスレッドの場合、ピープホール低減は全ての冗長なインターリービングの除去を必ずしも保証しない。
【０１１７】
例えば、tAtαtxがそれぞれT1,T2,T3に属するとする。tAとtxが従属し、しかしtαがtAとtxの両方に対して保護された独立であると仮定する。すると、次の2つのインターリービングは等価である。
【０１１８】
【数３５】
2009087356.tif 000037
【０１１９】
しかし、セグメント
【０１２０】
【数３６】
2009087356.tif 000038
【０１２１】
がスレッド(tA)＜スレッド(tα)に従い、セグメント
【０１２２】
【数３７】
2009087356.tif 000039
【０１２３】
がスレッド(tα)＜スレッド(tx)に従うので、両方のインターリービングはGIR制約を利用するピープホール低減によって許される。該3つの遷移を2つの独立なセット：[ tA,tx ]と[tα]にグループ化してもよい。対毎に独立な遷移が、順序付けられたスレッドインデックスと一致するように順序付けられた2つのセットの順序が存在しないことから非最適性が生じる。
【０１２４】
より一般的なケースにおいて全ての冗長なインターリービングを除去することを保証するためにピープホール低減を拡張することは可能であるが、サイズが2のウインドウにわたる簡単なピープホール低減が最も少ないオーバーヘッドを有する最良の結果を得るために好ましい。3つ以上のスレッドの場合でも、本低減は、既存の記号的方法よりも冗長なインターリービングをより著しく除去することができる。
【０１２５】
GIR制約のオーバーヘッドの低減：符号化方式では、最悪のケースにおいて、SCHへの制約である
【０１２６】
【数３８】
2009087356.tif 000040
【０１２７】
を追加する必要がある。ここで、［Ti ]はスレッドTiにおける遷移の数を表す。これらの制約は、各時間フレームにおいて複製される必要があり、このことはSMTソルバーにとって著しい性能オーバーヘッドをもたらすことがある。このオーバーヘッドを著しく下げることができる最適化技術が提示される。
【０１２８】
制約をマージすること：cGが適用されるとき、遷移t1∈transiが他のスレッドにおける全ての遷移t2∈transjに関して独立であるならば、GIR制約を全ての〈ｔ1,ｔ2〉対に対して別個に付加する必要はない。その代わり、これらの全てのGIR制約をマージし、それを
【０１２９】
【数３９】
2009087356.tif 000041
【０１３０】
へと簡単化する。
【０１３１】
この最適化を適用できる簡単なケースはt1がローカルな遷移(他のスレッドには見えない)のときである。このケースでは、得られる効果はトランザクションを検出することから得られる効果と同様である。本低減の有効性は、インターリービングがトランザクションの境界で発生するときに最も良く観察される。ピープホール低減は、低減方法に基づくトランザクションに直交し、かつ補完的である。しかし、上記のルールはそのような簡単なケースにのみ限定されない。より複雑なケースとして、1つのスレッドにおける全てのトランザクションが目に見える(少なくとも、それ自身以外の1つの賢人にとって)N人の食事をしている賢人(dining philosophers)を考える。互いに隣接していない2人の賢人(iとj)の場合、(i番目の賢人における)遷移t1∈transiは常に独立で、全ての遷移はtransjにある。
【０１３２】
独立したトランザクション：緩く結合したスレッドの場合、独立なトランザクション対の数は、従属したトランザクション対(コンフリクト)の数よりも著しく大きい。そのようなケースでは、GIR制約のオーバーヘッドを減らす代わりの符号化方式を用いることができる。あらゆる独立の遷移に対する制約を加える代わりに、より少ない従属遷移対に焦点を当てることを選択する。
【０１３３】
スレッドTiとTj（i<j）の全ての対について、
【０１３４】
【数４０】
2009087356.tif 000042
【０１３５】
が、他のスレッドに従属することがある遷移の2つのサブセット示すとしよう。定義からして、
【０１３６】
【数４１】
2009087356.tif 000043
【０１３７】
,t1、t2は常に独立している。これは図6に示されている。
【０１３８】
【数４２】
2009087356.tif 000044
【０１３９】
の幾つかの遷移は依然として互いに独立していることがある。
【０１４０】
まず、スレッドTiに対してenTiを次のように定める。
【０１４１】
【数４３】
2009087356.tif 000045
【０１４２】
次に、これらの、常に独立な遷移対の全てに対する制約を要約する。各iとjについて、
【０１４３】
【数４４】
2009087356.tif 000046
【０１４４】
を加える。次に、各
【０１４５】
【数４５】
2009087356.tif 000047
【０１４６】
について、もし〈t1,t2,cG〉∈RGならば、
【０１４７】
【数４６】
2009087356.tif 000048
【０１４８】
を加える。この最適化は、
【０１４９】
【数４７】
2009087356.tif 000049
【０１５０】
が
【０１５１】
【数４８】
2009087356.tif 000050
【０１５２】
よりも著しく小さいケースに適している。一例として、2つのスレッドが完全に独立であるならば、1つの制約だけをSCHに加える必要がある。
【０１５３】
保護された独立関係の新しい考え方に基づいて、モデルチェックコンカレントシステムのための新しいピープホール部分的命令低減方法を提示した。特性違反を発見するSMT/SATを用いるのに良く適した、ローカルに独立した対の簡潔な記号符号化が提供される。新しいピープホールPOR方法は既存の方法に比べて著しくより多くの低減を達成することができる。2つのコンカレントのスレッドを有するシステムでは、この方法は全ての冗長なインターリービングの除去を保証する。
【０１５４】
モデルチェックコンカレントソフトウェアのための、記号的動的部分命令低減（POR）方法が提示された。保護された独立な遷移、すなわち、新しい記号符号化方式を用いることによって取得することができる、ある(しかし全てではない)実行パスにおいて独立であると見なすことができる遷移が実行された。この新しい符号化方式は、幾つかの保護された独立条件が部分的変数割り当てによって満たされるとき、SMT/SATソルバー内の冗長なインターリービングを自動的に取り除く簡潔な制約を付加する。2つのスレッドでは、本方法は、全ての冗長なインターリービングの除去を保証する。
【０１５５】
保護された独立な遷移を用いる部分命令低減システムと方法の好適な実施形態(例示であり、限定するものではない)を記載したが、種々の修正および変形が、上記の教示を考慮して当業者によってなされうることに留意すべきである。したがって、添付の特許請求の範囲によって概略を示す本発明の範囲と要旨内にある、開示された特定の実施形態において変形がなされうることが理解されるべきである。詳細が特許法によって要求される本発明の態様をこのように記載したが、特許証によって保護された、請求され、かつ所望されるものは添付の特許請求の範囲に記載されている。
【図面の簡単な説明】
【０１５６】
【図１】図１は、本明細書で述べる原理を説明する、２つのスレッド用のプログラムコードを示す図である。
【図２】図２は、図１のプログラムのインターリービングを示す格子図である。
【図３】図３は、一例示的実施形態による、マルチスレッド化されたプログラムを検証するシステム/方法を示すブック/フロー図である。
【図４】図４は、本発明の原理に従う、冗長なインターリービングの除去を示す図である。
【図５】図５は、本発明の原理に従う、冗長なインターリービングの除去を示す図である。
【図６】図６は、本発明の原理に従う、符号化を最適化する従属遷移の使用を示す図である。
【図１】
2009087356.tif 000051
【図２】
2009087356.tif 000052
【図３】
2009087356.tif 000053
【図４】
2009087356.tif 000054
【図５】
2009087356.tif 000055
【図６】
2009087356.tif 000056