(57)【要約】コンピュータプログラム検証用の競合警告を生成するシステムおよび方法は、共有変数を決定すること、ロックポインタのエイリアスに影響を及ぼす可能性のあるポインタに注目することおよび要約関数を活用することにより、ロックポインタの文脈依存性ポイントツー集合を決定することを含んでいる。ロックセットは、ロックポインタのポイントツー集合を使用して共有変数がアクセスされる位置で決定される。警告は互いに素なロックセットに基づいている。
2010517163.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータプログラム検証用の競合警告を生成する方法であって、
共有変数を決定することと、
ロックポインタのエイリアスに影響を及ぼす可能性のあるポインタに注目することおよび要約関数を活用することにより、ロックポインタの文脈依存性ポイントツー集合を決定することと、
前記ロックポインタのポイントツー集合を使用して共有変数がアクセスされる位置でロックセットを決定することと、
互いに素なロックセットに基づいて警告を生成することとを有する方法。
【請求項２】
前記共有変数の決定はデータフロー解析を行うことを含む、請求項１に記載の方法。
【請求項３】
前記データフロー解析は、最大更新シーケンスを追跡して真の変数更新のみを特定する、請求項２に記載の方法。
【請求項４】
前記ロックポインタの文脈依存性ポイントツー集合を決定することは、各ロックポインタが同じクラスのポインタにのみエイリアスすることができるように、前記プログラム中のすべてのポインタ群を互いに素なクラスに分割することを含む、請求項１に記載の方法。
【請求項５】
各ロックポインタが同じサブクラスのポインタにのみエイリアスすることができるように、前記プログラム中の前記すべてのポインタ群をサブクラスに再分割することをさらに含む、請求項４に記載の方法。
【請求項６】
前記ロックポインタの文脈依存性ポイントツー集合を決定することは、ロックアクセスを持つ低減された関数の数について要約関数を計算することを含む、請求項１に記載の方法。
【請求項７】
前記ロックポインタのポイントツー集合を使用して共有変数がアクセスされる位置で取得履歴を計算することをさらに含む、請求項１に記載の方法。
【請求項８】
前記警告を生成することは、       ロック取得履歴が整合しているかどうかを調べることを含んだ、同じ共有変数にアクセスする異なるスレッド中の対の位置についての警告を生成することを含む、請求項１に記載の方法。
【請求項９】
警告を生成した後競合警告を低減する請求項１に記載の方法。
【請求項１０】
前記競合警告を低減することは、２つのスレッド間のプログラム位置への同時到達可能性を表すロック取得履歴間の整合性を決定することと、不整合なロック取得履歴に関連する警告を無視することとを含む、請求項９に記載の方法。
【請求項１１】
前記ロックセットおよび取得履歴に基づいて、順位付けよりも弱い関係を判断して警告をランク付けすることと、その後順位が低い警告を削除することとをさらに含む、請求項９に記載の方法。
【請求項１２】
コンピュータ可読プログラムを含んだコンピュータプログラム検証用の競合警告を生成するコンピュータ可読媒体であって、前記コンピュータ可読プログラムがコンピュータ上で実行されるとき、前記コンピュータ可読プログラムは該コンピュータに、
共有変数を決定するステップと、
ロックポインタのエイリアスに影響を及ぼす可能性のあるポインタに注目することおよび要約関数を活用することにより、ロックポインタの文脈依存性ポイントツー集合を決定するステップと、
前記ロックポインタのポイントツー集合を使用して共有変数がアクセスされる位置でロックセットを決定するステップと、
互いに素なロックセットに基づいて警告を生成するステップと、
を実行させるコンピュータ可読媒体。
【請求項１３】
前記共有変数を決定することは、最大更新シーケンスを追跡して真の変数更新のみを特定するデータフロー解析を行うことを含む、請求項１２に記載のコンピュータ可読媒体。
【請求項１４】
前記ロックポインタの文脈依存性ポイントツー集合を決定することは、各ロックポインタが同じクラスのポインタにのみエイリアスすることができるように、前記プログラム中のすべてのポインタ群を互いに素なクラスに分割することを含む、請求項１２に記載のコンピュータ可読媒体。
【請求項１５】
各ロックポインタが同じサブクラスのポインタにのみエイリアスすることができるように、前記プログラム中の前記すべてのポインタ群をサブクラスに再分割することをさらに含む、請求項１４に記載のコンピュータ可読媒体。
【請求項１６】
前記ロックポインタの文脈依存性ポイントツー集合を決定することは、ロックアクセスを持つ低減された関数の数について要約関数を計算することを含む、請求項１２に記載のコンピュータ可読媒体。
【請求項１７】
前記ロックポインタのポイントツー集合を使用して共有変数がアクセスされる位置で取得履歴を計算することをさらに含む、請求項１２に記載のコンピュータ可読媒体。
【請求項１８】
前記警告を生成することは、ロック取得履歴が整合しているかどうかを調べることを含んだ、同じ共有変数にアクセスする異なるスレッド中の対の位置についての警告を生成することを含む、請求項１２に記載のコンピュータ可読媒体。
【請求項１９】
警告を生成した後競合警告を低減する請求項１２に記載のコンピュータ可読媒体。
【請求項２０】
前記競合警告を低減することは、２つのスレッド間のプログラム位置への同時到達可能性を表すロック取得履歴間の整合性を決定することと、不整合なロック取得履歴に関連する警告を無視することとを含む、請求項１９に記載のコンピュータ可読媒体。
【請求項２１】
前記ロックセットおよび取得履歴に基づいて、順位付けよりも弱い関係を判断して警告をランク付けすることと、その後順位が低い警告を削除することとをさらに含む、請求項２０に記載のコンピュータ可読媒体。
【請求項２２】
コンピュータプログラム検証用の競合警告を生成する方法であって、
データフロー解析を行うことにより自動的に共有変数を決定し、どの変数がプログラムに書き込まれているかを判断することにより真の変数更新のみを決定することと、
ロックポインタのエイリアスに影響を及ぼす可能性のあるポインタに注目することおよび要約関数を活用することにより、ロックポインタの文脈依存性ポイントツー集合を効率的に決定することと、
共有変数がアクセスされる位置でロックセットを決定することと、
前記ロックセットおよびロック取得のパターンに基づいて競合警告を生成することとを含む方法。
【請求項２３】
前記ロックセットを決定することは、
各ロックポインタが、同じクラスのポインタにのみエイリアスすることができるように、前記プログラム中のすべてのポインタ群を互いに素なクラスに分割することと、
共有変数およびロックのローカル参照を用いて関数の数を低減することにより、不可欠なエイリアス解析において低減された関数の数について要約関数を計算することとを含む、請求項２２に記載の方法。
【請求項２４】
前記クラスに分割することは、各ロックポインタが同じサブクラスのポインタにのみエイリアスすることができるように、前記プログラム中の前記すべてのポインタ群をサブクラスに再分割することを含む、請求項２２に記載の方法。
【請求項２５】
前記ロック取得のパターンに基づいて競合警告を生成することは、
２つのスレッド間のプログラム位置への同時到達可能性を表すロック取得履歴間の整合性を決定し、不整合なロック取得履歴に関連する警告を無視することと、
ロック取得履歴をランク付けするために、整合性より弱い履歴を判断して、該弱いロック取得履歴に関連する警告を削除することとを含む、請求項２２に記載の方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、コンピュータシステムの検証に関し、特にマルチスレッドソフトウェアをデバッグするシステムおよび方法に関する。
【背景技術】
【０００２】
現代のコンピュータシステムでは、並列ソフトウェアの広範な使用により、マルチスレッドソフトウェアを効率的にデバッグする方法の開発が必要とされている。しかしながら、マルチスレッドプログラムは挙動的に複雑であり、手動での解析を困難にしているスレッド間の微妙な相互作用を含んでいる。このことは、そのようなシステムについて推論する自動化された形式的方法の使用を促している。特に捕捉し難いのはデータ競合違反から発生するエラーである。
【０００３】
データ競合は、所与のプログラム中の２つの異なるスレッドが書き込み動作という少なくとも１つのアクセスで、共有変数に同時にアクセスできる場合に発生する。該データ競合を調べることは、並列プログラムのデバッギングの重要な第一歩であることが多い。確かに、プログラム中でのデータ競合の存在は、通常該プログラムの挙動を非決定的にするので、より複雑でより関心のある特性の挙動を推論することを困難にしている。
【０００４】
データ競合検出に対する従来のアプローチは、３つのステップを含んでいる。最初の最も重要なステップは、共有変数、すなわち２つ以上のスレッドによってアクセスできる変数の自動的な発見である。これらの共有変数が読み出されるかまたは書き込まれる制御位置が、データ競合が発生する可能性のある位置を決める。事実、共通の共有変数が、互いに素なロックセットが保持されている２つの異なるスレッド中の同時到達可能なプログラム位置でアクセスされる場合に、ロック関連データの競合が発生する。該ロックは通常ポインタを介してアクセスされるので、第２のステップでは、関心のあるプログラム位置でこれらのロックセットを決定するのに、不可欠なポインタのエイリアス解析が実行される。つまり、静的解析の主な欠点は、真のバグに該当しない多数の偽りのデータ競合警告を生成する可能性が高いということである。したがって、最後のステップは、信頼度に基づいて該偽りの警告をろ過するかまたはそれらに優先順位を付けるランキングを使用するかのいずれかに対して、警告低減およびランキング技術を使用することである。
【０００５】
課題は、種々の要因により決定される拡張性と正確性という、相反する目標を満たしながら、競合検出を実行することにある。これらの要因の中で重要なのは、（ｉ）共有変数発見の正確性、および（ｉｉ）共有変数（エイリアスでなければならない）およびロックセット（エイリアスであってもよい）を決定するエイリアス解析の正確性および拡張性である。変数を誤って共有と表示することは、その変数について生成された警告のすべてを偽りにしてしまう。他方、変数を共有とする報告が見逃された場合、この種々の結果を伴う真のデータ競合についての警告は生成できない。
【０００６】
共有変数を自動的に発見することについては、多くの研究がなされている。しかし、ほとんどの既存の技術は、共有変数にアクセスする場合、ｖへの任意のアクセスの前に取得する必要があるロック１ｖに各共有ｖ変数を関連付けることにより、並列プログラムはほとんどいつもロックの原則に従うという基本的な前提に基づいている。既存の技術は、ロックと変数の間のこの関連を計算することに注目している。その目的に対して、種々の相関に基づく技術、すなわち統計および制約の両方に基づく技術が開発された。統計に基づく技術の利点は、拡張可能であること、およびボトルネックになることが多いエイリアス解析に左右されないということである。しかしながら、相関に基づく技術によって例えば一連のリナックスドライバにおいてデータ競合の原因である共有変数が検出できないことは、該技術の主な弱点がロッキング規範の存在に対するまさに信頼にあるという事実を露見した。
【０００７】
勿論、ロッキング規範が破られる場合には、確かに多くのデータ競合が発生する。さらに、考慮されたほとんどのドライバにおいて、最初の実装はロッキング規範に正確に従っていたことがわかった。データ競合バグは、プログラムが、最適化のためにまたはバグを修正するために新しいコードを追加することにより後で変更されたときにのみ持ち込まれていた。通常、この新しく追加されたコードは、最初のコードにはなかった共有変数へのロックフリーアクセスを持ち込んだ「ハッカー」であった。これらの変数はロックによって防御されていない領域でのみ発生していたので、これらの変数に対し意味のある相関性を構築することができず、意味のある相関性を開発できなかったことが、相関に基づく技術が役立たなかった重要な理由であった。
【０００８】
競合検出はよく研究された課題であり、以下のような種々の技術がその問題に取り組むために採用された。１）ランタイムデータの競合検出：重要な発想は、所与のプログラムの具体的な実行を調べることであり、コードに存在するデータ競合へとプログラムを導く系統的方法である。しかしながら、通常並列プログラムの状態空間は広く原則的には無限でさえあるので、十分な適用範囲を得て保証を提供するのは難しい。２）モデル検査：所与の並列プログラムの状態空間全体を調べる。該状態空間を計り大規模な実プログラムを取り扱う見込みはほとんどない。３）静的解析：所与のプログラムの制御フローグラフを調べてロックセットの情報を抽出する。この利点は大きなコードベースへの拡張性を含んでいることである。不利な点は余りにも多くの偽りの警告を含んでいることである。
【非特許文献１】Ｂ．Ｓｔｅｅｎｓｇａａｒｄ著，”Ｐｏｉｎｔｓ−ｔｏ  ａｎａｌｙｓｉｓ  ｉｎ  ｍｏｓｔ  ｌｉｎｅａｒ  ｔｉｍｅ”，ＰＯＰＬ，１９９６年
【発明の開示】
【発明が解決しようとする課題】
【０００９】
共有でない変数を検出しないことを確保するために、非常に自由度の高い基準を使用して変数を共有として分類する。本発明の共有変数検出ルーチンは、すべての共有変数が、スレッドのグローバル変数、スレッドのエイリアス、アプリケーションプログラムインタフェース（ＡＰＩ）関数へパラメータとして渡されたポインタまたは拡張変数のいずれかであるという前提に基づいている。さらに、本発明は、変数のみがデータ競合に参加することができるように、所与のプログラムに書き込まれる上記セットから変数のサブセットを正確に特定することに関心がある。本発明における主な課題は、ローカルポインタを介してグローバル変数にアクセスすることができるので、そのようなローカルポインタへ誘導するエイリアス割り当てを追跡する必要があることである。さらに複雑なのは、グローバル変数のエイリアスへのすべての割り当てが、グローバル変数へ有意な更新になるとは限らないということである。当然、ポインタｐから始まりグローバル構造Ｓに至る、ｐl＝ｐ，…，ｑ＝ｐkというポインタ割り当てのシーケンスにおいては、上記のシーケンスにおける割り当ては、任意の（スカラ）変数の値を更新しないで、エイリアス情報を渡すだけであることがわかる。しかしながら、形式ｐ→ｆ＝ｅｘｐのＳのフィールドｆへの割り当てが上記シーケンスに続く場合、該割り当ては、それを関心のある変数にするｆに対する真の更新である。本発明では、効率的なデータフロー解析によって、そのような更新シーケンスを検出することができることを示している。実際、ほとんどのリナックスドライバでは、スレッドに対してグローバルなデータは、通常多くのフィールド、典型的には５０から１００のフィールドを持っているグローバル構造として格納される。そのごく一部分だけが、新しい方法が高精度で分離できた共有データを格納するために実際に使用されており、グローバル構造のすべてのフィールドを共有と宣言することは、余りにも多くの偽りの警告を生成するだけであろう。
【００１０】
静的な競合検出の第２のステップは、共有変数がアクセスされるプログラム位置で、ロックセットを正確に決定することである。通常、ロックはポインタを介してアクセスされるので、このステップはこれらのロックポインタの不可欠なエイリアスの計算を含んでいる。したがって、警告生成の正確性は、不可欠なエイリアスポインタ解析の正確性に直接左右される。さらに、正確性のためには、ロックエイリアスは、計算された文脈依存であるべきである。これは、Ｃプログラミングの不可欠なエイリアスの大半は、関数のポインタ引数のパラメータ受け渡しから発生するためである、すなわち異なるコンテキストの異なるポインタにエイリアスするためである。結果として、文脈依存のエイリアス解析は、コンテキストに鈍感なエイリアス解析に比べて偽りの警告を生み出すことが非常に少なくなる。しかしながら、大きなプログラムに存在できるコンテキストの数は容易に激増することがあるので、文脈依存解析の重要な欠点はその拡張性にある。
【００１１】
近年、ＢＤＤのようなデータ構造を使用してコンテキストを記号で格納することによって、この問題を改善する相当な研究がなされてきた。ＢＤＤＢＤＤＢのようなＢＤＤベースの文脈依存のポインタ解析の実装が先行技術に示されており、Ｊａｖａ（登録商標）プログラムに好結果をもたらしている。しかしながら、Ｊａｖａ（登録商標）プログラムほど構造化されていないＣプログラムは、通常プログラムの大きさが成長するにつれてＢＤＤＢＤＤＢを使用しての処理を困難にする、余りにも多くのポインタ変数、およびそれらの間の複雑なエイリアス関係を持っている。これは、ＢＤＤＢＤＤＢのダウンロードされたバージョンを用いた本発明の実験によって確証された。
【課題を解決するための手段】
【００１２】
拡張可能な文脈依存のポインタ解析の新しいシステムおよび方法は、次の態様を組み合わせてもよい。（１）分断攻略：これは、各ポインタがそのクラス内のポインタだけにエイリアスすることができるように、プログラム中のすべてのポインタ群を互いに素なクラスに分割することができるという事実を活用するものである。一般にエイリアシングが同値関係でない間、多くの広く使用されているポインタ解析は、エイリアシングの過剰近似である同値関係を生成する。この最初のポインタ解析は分割化にのみ使用されるので、拡張性が正確性より重要であるが、これはまさにＳｔｅｅｎｓｇａａｒｄの（参照により本書に組み込まれた、１９９６年、ＰＯＰＬの、非特許文献１を参照されたい）解析が提案するものである。この分割化には２つの重要な帰結がある。まず、本発明ではロックポインタにしか関心を抱いていないので、また該ロックポインタは他のロックポインタしかエイリアスすることができないので、非ロックポインタを無視することができる。これにより、本発明の解析で考慮する必要のあるポインタの数を大幅に低減できる。第２に、一般に、ロックポインタの全セットの小さなサブセットに所与のロックポインタをエイリアスすることができるので、Ｓｔｅｅｎｓｇａａｒｄ解析は、ロックポインタ群をより小さな分割へとさらに分解してくれる。次に、第２のより正確な文脈依存のエイリアス解析がこのような最終分割で実行され、一般に高価ではあるがこのような小さなクラスで拡張可能になる。
【００１３】
（２）プロシージャ要約：これは、参照の局所性、すなわちロックおよび共有変数が関数のごく一部分でアクセスされるという事実を利用するものである。したがって、不可欠なエイリアス解析プロシージャに基づいた本発明の新しい要約は、この少関数の数についてのみ概要を計算する必要があるだけであり、それによって本発明のアプローチを大きなプログラムに適用可能にする。本発明は、プロシージャ要約がどんな静的解析も拡張可能にする点で非常に重要であることを強調している。確かに、典型的な実コードには、種々のコンテキストから呼び出すことができる多数の小さな関数を持っている。プログラムは大きく成長するので、ＢＤＤＢＤＤＢのような非要約に基づいた技術を容易に凌駕することができる。本発明で拡張性を達成することができるのは、２つの技術の組み合わせにより生じた相乗作用のためであることに留意されたい。確かに、分断攻略により要約を実行可能にする、参照の局所性を利用することができるようになる。
【００１４】
最後に、静的な競合検出技術を使用する主な弱点の１つは、（偽り）の競合警告を多数生成することがよくあるということである。本発明では、ロックセットの代わりにロック取得パターンを追跡することが、２つの方法における警告低減技術に基づいた既存のロックセットよりも正確な警告低減技術になることを示している。まず、ロックセットに加えて取得履歴を活用することによって、まさに警告生成段階でロックセットに基づいた技術によって生成された警告をろ過することができる。第２に、いったん警告が生成されると、取得履歴を活用してより良い警告低減を証明可能に与えるドミネータに基づく技術を使用することができる。さらに、ランキングの使用により、本発明の低減技術が適切なこと、すなわち偽りのデータ競合を支持して真のデータ競合を落とさないことを確保することができる。
【００１５】
コンピュータプログラム検証用の競合警告を生成するシステムおよび方法は、データフロー解析を行うことにより共有変数を決定することを含んでいる。ロックポインタのロックセットを分断攻略法と要約関数を組み合わせることができる文脈依存のエイリアス解析で決定して、不足している取得パターンを提供する。競合警告はロック取得パターンに基づいて生成される。
【００１６】
コンピュータプログラム検証用の競合警告を生成するシステムおよび方法は、データフロー解析を行うことにより共有変数を決定すること、分断攻略法と要約関数を組み合わせることができる文脈依存のエイリアス解析において、ロックポインタのポイントツー集合を決定すること、を含んでいる。ロックセットおよび取得履歴は、共有変数がアクセスされる位置で決定される。警告は、互いに素なロックセットおよび取得履歴の整合性に基づいて生成される。競合警告は、ロックセットおよびロック取得パターンの両方に基づいた順位付け関係を使用して低減される。
【００１７】
コンピュータプログラム検証用の競合警告を生成する方法は、データフロー解析を行うことにより共有変数を決定し、どの変数がプログラムに書き込まれているかを判断することにより真の変数更新のみを決定すること、分断攻略法を要約関数と組み合わせてロック取得パターンを提供する文脈依存のエイリアス解析において共有変数がアクセスされるプログラム位置で、ロックポインタのロックセットの不可欠なエイリアスを決定すること、ロック取得パターンに基づいて競合警告を生成すること、を含んでいる。
【００１８】
コンピュータプログラム検証用の競合警告を生成するシステムおよび方法は、共有変数を決定すること、ロックポインタのエイリアスに影響を及ぼす可能性のあるポインタに注目することおよび要約関数を活用することにより、ロックポインタの文脈依存性ポイントツー集合を決定することを含んでいる。ロックセットは、ロックポインタのポイントツー集合を使用して共有変数がアクセスされる位置で決定される。警告は互いに素なロックセットに基づいている。
【００１９】
コンピュータプログラム検証用の競合警告を生成するシステムおよび方法は、共有変数を自動的に決定すること、通常少数であるロックポインタのエイリアスに影響を及ぼす可能性のあるポインタにのみ本発明の解析を集中させることおよび要約関数を活用することによって、ロックポインタの文脈依存性ポイントツー集合を効率的に決定すること、計算されたロックポインタのポイントツー集合を使用して共有変数がアクセスされる位置でロックセットを決定すること、互いに素なロックセットに基づいて警告を生成することを含んでいる。
【００２０】
これらおよび他の特徴および利点は、添付の図面に関して読まれるべき、その例示となる実施形態に関する以下の詳細な説明から明白になるであろう。
【００２１】
本開示は、次の図面に参照して、以下の好ましい実施形態においてその詳細を提供するだろう。
【発明を実施するための最良の形態】
【００２２】
本発明の実施形態は、コンピュータ検証システムにおけるデータ競合の問題を改善する解決策を提供している。新しいシステムおよび方法が、並列プログラムでの高速で、正確で、拡張可能な静的競合検出に提供される。リナックスデバイスドライバに解析を集中させることにより、大規模な実コードをデバッグすることによって引き起こされる固有の課題、および既存の競合警告生成方法における固有の欠点が特定可能になる。これは、競合警告生成システムにおける３つの主なステップの各々の拡張性および正確性の両方を改善するのに有用な新しい技術の開発を促した。データ競合検出の第１のステップは、自動的に共有変数を発見することである。この目的のために、本発明のベンチマークスイートのドライバの大多数におけるデータ競合に関与する共有変数を検出できない既存の相関に基づく技術よりもより効果的な共有変数検出についての新しい効率的なデータフロー方法を説明する。
【００２３】
第２に、競合警告生成の正確性は、ロックポインタのエイリアスを計算するのに使用されるポインタ解析の正確性に強く左右される。分断攻略戦略と要約関数を有効に組み合わせて、既存のＢＤＤに基づいた技術よりも明らかに効率的な、新しい拡張可能な文脈依存のエイリアス解析が考案された。第３に、ロック取得パターンを活用する新しい警告低減システムおよび方法が提供され、既存のロックセットに基づいた方法よりも優れた警告低減が生成される。
【００２４】
大規模な実コードのデバッギングによって生じた実用上の課題を特定するために、１つの解析は、リナックスデバイスドライバにおけるデータ競合の検出に注目した。バグレポートおよびＣＶＳログに関する注意深い研究により、ドライバにデータ競合が存在する２つの主な理由が、誤ったロッキングおよびタイミングに関連する問題であることが明らかになった。タイミングに関連するデータ競合は、ソフトウェアレベルで解析することが困難であるため、本発明ではロッキングに関連するバグだけに注目することにした。
【００２５】
本書に説明された実施形態は、完全にハードウェア、完全にソフトウェア、またはハードウェア要素およびソフトウェア要素の両方を含んでいてもよい。好ましい実施形態において、本発明は、ファームウェア、常駐ソフトウェア、マイクロコードなどを含むソフトウェアに実装されるが、これらに限定されるものではない。
【００２６】
実施形態は、コンピュータまたは任意の命令実行システムによってまたはそれらに関連して使用されるプログラムコードを提供するコンピュータ使用可能媒体またはコンピュータ可読媒体からアクセス可能なコンピュータプログラム製品を含んでいてもよい。該コンピュータ使用可能媒体またはコンピュータ可読媒体は、命令実行のシステム、装置、またはデバイスによってまたはそれらに関連して使用されるプログラムを、格納、通信、伝搬、または搬送する任意の装置を含んでいてもよい。該媒体は、磁気、光学、電子、電磁気、赤外線、または半導体のシステム（すなわち装置またはデバイス）、または伝搬媒体であることができる。媒体は、半導体または固体メモリ、磁気テープ、リムーバブルコンピュータディスケット、ランダムアクセスメモリ（ＲＡＭ）、読み取り専用メモリ（ＲＯＭ）、剛性磁気ディスクおよび光ディスクなどのような、コンピュータ可読媒体を含んでいてもよい。
【００２７】
ここで、同じ数字が同一または類似の要素を表わしている図面を参照するが、まず図１を参照してデータ競合検出およびデータ競合警告用のシステムおよび方法１０を表すブロック図およびフロー図が示されている。ブロック１２では、共有変数の発見が実行される。どんな共有変数も見逃さないために、変数が共有変数として宣言される場合についての非常に自由度の高い定義が使用される。本質的に、本発明の関心は、グローバル変数、そのエイリアス、ＡＰＩ関数にパラメータとして渡されたポインタ、および拡張変数に対するすべての真の変更に向けられている。直接書き込まれるスレッドのグローバル変数は共有として宣言されている。そのような変数は、所与のドライバの各プログラムステートメントを単にスキャンするだけで決定することができる。しかしながら、グローバル変数はローカルポインタを介してアクセスすることもできる。そのようなポインタｑは、ポインタｐから始まり、例えばグローバルであるかまたはパラメータとしてＡＰＩ関数に渡される、グローバル構造Ｓに至る一連のポインタ割り当てｐ1＝ｐ、ｐ2＝ｐ1、．．．、ｑ＝ｐkの最後に発生することがある。ｐを通したアクセスによって変更されるどんな変数ｖも関心のある変数である。しかしながら、シーケンスに発生するすべてのポインタを共有と宣言するだけで、多くの偽りの警告に到達できることもある。確かに、上記の割り当てシーケンスでは、割り当ては真の更新ではなく、単にフィールドＳの値を伝搬する役目をするだけである。しかしながら、形式ｐk+1→ｆ＝ｅｘｐの割り当てが上記のシーケンスに続いている場合（ここで、ｅｘｐはデータ値の単純な伝搬でなく、ローカル変数または式のいずれかである）、その割り当ては真の更新であり関心のある共有変数と宣言されるべきである。
【００２８】
各ｉについて、ポインタｐiが書き込まれた後およびシーケンスで読み出される前に、ポインタｐiへの割り当てが存在しない場合、ポインタへの割り当てのシーケンス、ｐ1＝ｐ、ｐ2＝ｐ1、．．．、ｑ＝ｐkは、ｐからｑまでの完全な更新シーケンスと呼ばれる。したがって、１つの目標は、ｑによってアクセスされたスカラ変数の変更が続くｐからｑまでの完全な更新シーケンスを検出することであり、ここでｐは、グローバル変数を指すかまたはパラメータとしてＡＰＩ関数に渡されるかのいずれかである。
【００２９】
このようなシーケンスは、ブロック１８で新しい内部手順データフロー解析を使用して決定される。本質的に、上に説明したように、図２に示した解析プロシージャ１８は、共有と宣言されたローカルなグローバル変数に真の更新を達成させるまで、完全な更新シーケンスで割り当てを伝搬する。プロシージャ１８は、集合Ｐshのように共有変数の可能性があるものを追跡し続ける。スレッドＴを考えると、Ｐshで始まることは、グローバル変数にまたはパラメータとしてＡＰＩ関数に渡されるポインタであるＴの変数を含んでいる。別個の変数Ｖshは、結果的に共有される真の更新に関わる変数を追跡し続ける。ｗ∈Ｐshの場合、形式ｖ＝ｗの各割り当ては伝搬である。したがって、
【００３０】
【数１】
2010517163.tif 000003
【００３１】
の場合、各割り当てがＰshに追加される（例えば、図２の共有変数検出用データフロー解析の４行目から６行目を参照されたい）。形式ｖ＝ｅｘｐの割り当てがあり、ｅｘｐが上に説明したように（７行目から１２行目）真の更新である場合、変数ｖ∈ＰshはＶshに含まれている。
【００３２】
図１を再び参照して、ロックセットは、共有変数がブロック１４でアクセスされる制御位置で決定される。いったん共有変数が特定されると、正確なロックセットに基づいて警告を生成するボトルネックとなるのは、共有変数がアクセスされる制御位置でロックセットを決定するブロック２０における、拡張可能な文脈依存の不可欠なエイリアス解析である。拡張可能な文脈依存のエイリアス解析を行う新しい方法は、分断攻略戦略と要約関数を効果的に組み合わせ、両技術の利点を活用することに基づいている。
【００３３】
分割化：本発明は、たとえエイリアシングが一般に同値関係になくても、（上に引用された）Ｓｔｅｅｎｓｇａａｒｄの解析のような多くのエイリアス解析が、エイリアシングの過剰近似であるけれども、重要なことには同値関係となる関係を計算するという事実を利用することができる。さらに、Ｓｔｅｅｎｓｇａａｒｄの解析の同等に重要な特徴は、それが高度に拡張可能であるということである。これは、プログラム中のすべてのポインタ群を、エイリアス関係を尊重する互いに素なクラスに分割するという本発明の目的、すなわちポインタをそれが属するクラス内のポインタにだけエイリアスすることができるという目的に理想的に適するようにする。Ｓｔｅｅｎｓｇａａｒｄの解析の欠点は、正確性の不足である。しかしながら、この本発明の目的は、より正確な解析を個々のＳｔｅｅｎｓｇａａｒｄ分割に集中させることにより達成することができる。
【００３４】
確かに、分割化は、プログラム中のすべてのポインタのポインタ解析を実行する代わりに、ポインタ解析の問題を各同値クラスの別個のポインタ解析を実行するのに十分なはるかに小さな下位の問題に効果的に分解する。分割化がエイリアス関係を尊重するという事実は、本発明がエイリアスを見逃さないことを保証している。小さなサイズの各分割は、より正確な解析についてのより高度な計算の複雑性を相殺する。言及したように、Ｓｔｅｅｎｓｇａａｒｄの生成されたロックポインタの同値クラスは、そのような小さな各分割に対し、文脈依存のエイリアス解析の拡張性を保証する所与のプログラムのロックポインタの小さなサブセットだけを含んでいる。分断攻略法を分割化に用いてもよい。
【００３５】
ブロック２０の別の態様は、要約によって参照の局所性を利用することを含んでいる。分解を使用することにより、いったん考慮中のポインタ群がロックポインタの小さな集合に制限されると、拡張可能な文脈依存のポインタ解析のプロシージャ要約を有効に活用することを可能にする、参照の局所性をさらに利用することができる。
【００３６】
実プログラムの中、共有変数、および結果としてロックが非常に少関数の数でアクセスされる。すべてのコンテキスト中のすべてのポインタのエイリアスをあらかじめ計算するＢＤＤＢＤＤＢ手法に従う代わりに、ロックポインタに関する手順を実行する可能性のあるすべての影響を捕らえるプロシージャ要約をその代わりに使用するほうが、はるかに拡張可能がある。プロシージャ要約の使用がより拡張可能性があるのは、ロックポインタがアクセスされる関数のごく一部分に対してだけこれらの要約を計算すればよいからである。
【００３７】
いったん要約を事前に計算すると、所与のコンテキストにおけるプログラム位置でのロックポインタのエイリアスを、要求があり次第効率的に生成することができる。本発明は、参照の局所性を活用することを可能にするのがこの分解であるということを重視している。該分解なくしては、ポインタアクセスを持つ各関数、すなわち実際に所与のプログラム中のすべての関数の要約を計算しなければならないであろう。さらに、各関数では、単にロックポインタだけでなく、関数において変更されるすべてのポインタに対する要約を計算する必要があり、このことは本方法の終了時間を大幅に増加させるかもしれない。分断攻略をブロック２０の要約と任意に組み合わせて、２つの技術間の相乗作用を利用してもよい。
【００３８】
文脈依存のポインタ解析のプロシージャ要約を計算することは、次のことを含んでいてもよい。要求主導の文脈依存のポインタ解析の新しい要約に基づいた技術が提供されている。コンテキストすなわち関数呼び出しのシーケンスｃｏｎ＝ｆ1、．．．、ｆnが与えられると、ｃｏｎで関数が実行される間、完全な更新シーケンスｐ1＝ｐ’、ｐ2＝ｐ1、．．．、ｐ＝ｐmがある場合、ポインタｐおよびｐ’はｃｏｎでエイリアスされる。
【００３９】
コンテキストのｃｏｎの関数ｆnの制御位置１でポインタｐの不可欠なエイリアスの集合を計算するために、各ｑ∈Ａnについて、位置１を制御する関数ｆnのエントリ位置から始まる各パスに沿ってｑからｐまで完全な更新シーケンスがあるように、ポインタ群Ａnをまず計算する。Ａnを取得した後、ｃｏｎの関数のシーケンスに沿って後方に横断を開始する。これは、ｆn-1のエントリ位置から始まりｆnが呼び出された位置へと至る各パスに沿って、ｒからｑまで完全な割り当てシーケンスがあるように、各ポインタｑ∈Ａn、すべてのポインタｒの集合Ａqn-1を計算することを含んでいる。Ａn-1＝Ｕq∈AnＡqn-1に設定する。その後、ｃｏｎの各関数の上記プロシージャをルート関数ｆlに達するまで繰り返すことにより、ｐの不可欠なエイリアスが与えられる。これは、ロックポインタの各関数の影響を捕らえる要約を計算することである。
【００４０】
所与のプログラムにおける関数ｆの要約は形式（ｐ、ｌ、Ａ）のすべてのタプル（ｔｕｐｌｅ）の集合となり、ここで、ｐは、エントリ位置で始まりｌで終了する各パスに沿ってｑからｐまで完全な更新シーケンスがあるようにｆにおいて位置ｌで書き込まれたポインタであり、Ａはすべてのポインタ群ｑである。集合Ａは、Ｓｕｍ（ｆ、ｐ、ｌ）によって示される。
【００４１】
例として図３を参照して、プログラム１００は、グローバルポインタｐおよびｑを含んでいる。まず、ポインタが「ｂａｒ」の中で変更されないのでその要約は空である。ｇ3∈Ｓｕｍ（ｇｏｏ、２ｃ、ｐ）およびｇ4∈Ｓｕｍ（ｇｏｏ、２ｃ、ｑ）である。同様に、ｇ4∈Ｓｕｍ（ｇｏｏ、５ｃ、ｑ）であるが、
【００４２】
【数２】
2010517163.tif 000004
【００４３】
である。これは、制御フローが、１つのブランチでｇ5に設定され、もう一方のブランチで古い値ｇ3を保持しているｐによって位置３ｃで分岐するからである。ｇ3とｇ5が同一のポインタかどうかを静的に判断する方法はない。したがって、Ｓｕｍ（ｇｏｏ、５ｃ、ｐ）＝０となる。Ｓｕｍ（ｆｏｏ、２ａ、ｐ）＝｛ｇ1｝およびＳｕｍ（ｆｏｏ、２ａ、ｑ）＝｛ｇ2｝であり、一方、Ｓｕｍ（ｆｏｏ、３ａ、ｐ）＝０およびＳｕｍ（ｆｏｏ、３ａ、ｑ）＝｛ｇ4｝である。
【００４４】
なお、関数の各プログラム位置に関する要約タプルをキャッシュに格納する必要がないことを理解されたい。関数ｆiについて、
【００４５】
【数３】
2010517163.tif 000005
【００４６】
の場合、必要なのは、ｆi+1が呼び出される位置の要約タプルだけである。さらに、データフロー解析を行う間に必要となる可能性もあるので、出口位置の要約タプルをキャッシュに格納する必要もある。ｃｏｎの最後の関数ｆnについては、ロックポインタがアクセスされる関数中の各位置の要約タプルが必要である。そのような位置の数はわずかであるので、生成される要約の大きさは小さい。
【００４７】
図４を参照して、ロックポインタ解析の要約を計算する方法を示している。関数ｆでポインタｐおよび位置ｌを与えられると、ｌで始まる所与のプログラムの制御フローグラフ（ＣＦＧ）上で後方への横断を行ない、形式（ｍ、Ａ）のタプルとして完全な更新シーケンスを追跡するが、ここで、ｍから始まりｌで終了するｑからｐまでの完全な更新シーケンスが存在するように、ｍはプログラム位置にあり、Ａはロックポインタ群ｑである。図４の方法は、まだ処理されていないタプルの集合Ｗと、既に処理されているタプルの集合Ｐとを保持している。最初に、Ｗはタプル（ｌ、｛ｐ｝）（図４の２行目）を含んでいる。なお、Ｗからタプル（ｍ、Ａ）を処理する前に、１つの目標は不可欠なエイリアスを計算することであるので、ｌに至るＣＦＧのパスが存在するｍの各後続ｍ’が、後方への横断中に既に処理されたこと、すなわちＷには現在、形式（ｍ’、Ｄ）のタプルがないことを確認する必要があることに留意されたい。そのようなタプルはレディ（ｒｅａｄｙ）と呼ばれる（図４の４行目）。ｍのステートメントがｔ∈Ａとなる形式ｒ＝ｔの場合には、処理（ｍ、Ａ）において、ｔをｒで置き換えることによりＡ’をＡから得る集合にするか、さもなければＡ’＝Ａにする（図４の５行目から７行目）。
【００４８】
Ａ’中のポインタを後方に伝搬するのに考慮すべき２つの事例がある。まず、ｍがｆの内部から呼び出された関数ｇのリターンサイトであると仮定する。次に、Ａ’中の各ポインタの後方でｇを実行する効果を伝搬しなければならない。まず、ｇの出口位置ｅｘｉｔgに対するＡ’中のポインタの各々について、ｇの要約タプルが既に計算されているかどうかを調べる。既に計算されている場合には新しいタプル（ｍ’、Ｂ）を形成する、ここで、ｍ’はリターンサイトｍ、およびＢ＝Ｕr∈A'Ｓｕｍ（ｇ、ｅｘｉｔg、ｒ）に対応するｇの呼び出しサイトである（図４の１２行目から１５行目では、ｔがｒの代わりに用いられている）。他方、要約タプルが計算されていない場合にはワークリストに新しいタプル（ｅｘｉｔg、Ａ’）を導入する（図４の１６行目）。第２の事例の場合、ｍが関数呼び出しリターンサイトではないと仮定すると、ｆにおけるｍのすべての先行オペレーション位置の集合Ｐｒｅｄを考慮する。各ｍ’∈Ｐｒｅｄについて、タプル（ｍ’、Ａ’）を形成する。タプル（ｍ’、Ａ’）が既に処理されている場合にはアクションは不要である。そうでなく、Ｗに形式（ｍ’、Ｃ）のタプルが既に存在する場合、位置ｍ’への新しい後方パスが発見される（図４では、ｌは、ｍ’の代わりに用いられたｍ’である）。不可欠なエイリアス、すなわちすべての後方ＣＦＧパスに沿って発見されたエイリアスの共通集合を計算しているので、タプル（ｍ’、Ｃ）はタプル（ｍ’、Ａ’∩Ｃ）に置き換えられる（図４の２３行目にある（ｍ’、Ｃ∩Ｂ））。そのようなタプルが存在しない場合、Ｗ（図４の２５行目）に新しいタプル（ｍ’、Ａ’）（または図４の（ｌ、Ｂ））を追加するだけである。
【００４９】
図１を再び参照して、ブロック１６で、警告が警告低減の取得履歴を活用して生成されている。ブロック２２では、ロック取得パターンの追跡に基づいて、既存のロックセットに基づく警告低減技術よりも証明可能で正確である２つの新しい競合警告低減技術が提供、採用されている（参照によって本書に組み込まれ、以下でＣｈｏｉとして参照されるＪ．Ｃｈｏｉ、Ｋ．Ｌｅｅ、Ａ．Ｌｏｇｉｎｏｖ、Ｒ．Ｏ’Ｃａｌｌａｈａｎ、Ｖ．Ｓａｒｋａｒ、およびＭ．Ｓｒｉｄｈａｒａｎ著、”Ｅｆｆｉｃｉｅｎｔ  ａｎｄ  ｐｒｅｃｉｓｅ  ｄａｔａ  ｒａｃｅ  ｄｅｔｅｃｔｉｏｎ  ｆｏｒ  ｍｕｌｔｉｔｈｒｅａｄｅｄ  ｏｂｊｅｃｔ−ｏｒｉｅｎｔｅｄ  ｐｒｏｇｒａｍｓ”、２００２年、ＰＬＤＩを参照されたい）。
【００５０】
新しい低減技術は、２つの段階で進行する。第１の段階では、２つの異なるスレッド中のプログラム位置が同時到達可能かどうかを管理する、ロック取得履歴の整合性についての概念を利用する。これにより、たとえ互いに素なロックが対応するプログラム位置で保持されていたとしても、ロック取得履歴が不整合となるこれらの警告を適切な方法で廃棄することが可能になる。ロックセットに基づく技術は、そのような警告を除去することができなかった。第２の段階では、第１の段階に対して補足的なさらに別の警告低減技術を使用するが、この技術は、Ｃｈｏｉで定義された関係よりも弱いロックセットに基づく技術よりも正確であって、残りの警告についての関係よりも弱い取得履歴に基づいた技術を定義することに基づいている。
【００５１】
本発明の戦略は、（ｉ）取得履歴の不整合性を活用して適切な方法で警告を除去し、（ｉｉ）関係よりも弱い、証明可能により正確な技術を提供するという、少なくとも２つの方法においてＣｈｏｉを改善する。Ｃｈｏｉの関係技術よりも弱いロックセットに基づく技術は、アクセスイベントを形式（ｖ、Ｔ、Ｌ、ａ、ｃ）の４つのタプルとして定義し、ここでｖはロックセットＬを持つスレッドＴの制御位置ｃでアクセスされる共有変数であり、ａはアクセスの形態、すなわち読み取りまたは書き込みを示している。スレッドの同じ局所的計算パスに沿ってｅ2およびｅ3が発生するように、ｅ1、ｅ2、およびｅ3をアクセスイベントとする。ここで、ｅ1とｅ2の間の競合の発生がｅ1とｅ3の間の競合の発生を意味している場合には、対（ｅ1、ｅ2）への警告を生成する必要はない。この場合、イベントｅ3は、
【００５２】
【数４】
2010517163.tif 000006
【００５３】
によって表示されたｅ2より弱いと言われている。関係
【００５４】
【数５】
2010517163.tif 000007
【００５５】
は、プログラムの状態空間を調査しないで正確に決定することは困難であり、この調査は非効率的である。その代わりに、それは静的解析により過剰に近似される。Ｃｈｏｉにおいて与えられるロックセットに基づく近似
【００５６】
【数６】
2010517163.tif 000008
【００５７】
は、「より弱いロックセットに基づく技術」として定義される（Ｃｈｏｉ）。スレッドＴの共通のローカル計算ｘに沿ってアクセスイベントｑ＝（ｖ、Ｔ、Ｌ2、ａ2、ｃ2）の前に発生するアクセスイベントｐ＝（ｖ、Ｔ、Ｌ1、ｃ1）について、
【００５８】
【数７】
2010517163.tif 000009
【００５９】
、ｉｆｆ  Ｌ1⊆Ｌ2、およびａ1＝ａ2またはａ1は、書き込み動作である。
【００６０】
図５を参照して、取得履歴に基づいた警告低減では、図５に示すように、共有変数ｘにアクセスする２つのスレッドＴ1およびＴ2で構成された単純な並列プログラムＣＰを活用してこの技術を促進している。図５において、ｅ1、ｅ2、ｅ3、およびｅ4は、位置６ａ、６ｂ、９ｂ、および２ｂでのｘへのアクセスをそれぞれ示すものとする。制御位置６ｂおよび９ｂのロックセットは、それぞれＬ2＝｛ｌｋ２｝およびＬ3＝｛ｌｋ２｝であることに留意されたい。Ｌ2⊆Ｌ3、
【００６１】
【数８】
2010517163.tif 000010
【００６２】
であるため、ロックセットに基づいた低減技術は、（ｅ1、ｅ2）を支持し、（ｅ1、ｅ3）を落としてしまうだろう。
【００６３】
しかしながら、いずれかの場合において互いに素なロックセットが２つの位置で保持されても、制御位置６ａおよび６ｂは同時到達可能ではなく、一方制御位置６ａおよび９ｂは同時到達可能である。これは、別個のスレッドの２つの制御位置の同時到達可能性が、これらの位置に保持されたロックのみならず、それらが個々のスレッドにおいて取得されたパターンにも左右されるからである。Ｔ2が６ｂに到達するには、位置３ｂおよび５ｂでステートメントを実行すること、すなわち、ロックｌｋ１を取得および解除することが必要である。しかしながら、いったんＴ1が位置２ａでｌｋ１を取得すると、該Ｔ1は６ａを出てしまうまでｌｋ１を解除しないことに留意されたい。したがって、２つのスレッドが６ａと６ｂに同時に到達するには、Ｔ2がまずｌｋ１を取得および解除すること、すなわちＴ1が２ａを実行する前に５ｂを既に実行していることが必要である。しかしながら、その場合、Ｔ2、自らが解除することができないロックｌｋ２を（ｌｂの実行によって）保持しているので、Ｔ2が３ａを実行し、さらに通過するのを防ぐことができる。一方、６ａと９ｂの同時到達可能性を調べるのが簡単である。したがって、Ｃｈｏｉの
【００６４】
【数９】
2010517163.tif 000011
【００６５】
に基づいた低減は、偽りのデータ競合を支持し、真のデータ競合に対応する警告を落としてしまう。一般に、２つの異なるスレッドの制御状態ｃおよびｃ’の到達可能性をテストする場合、上記のシナリオの見落としを防ぐように、互換性のあるやり方で取得することができるロックセットＬおよびＬ’を保持する状態ｃおよびｃ’に至る個々のスレッドに、パスｘおよびｙが存在するかどうかをテストする必要がある。互換性は、取得履歴についての概念を使用して捕らえることができる。
【００６６】
取得履歴：ｓを、グローバル構成ｃに導く並列プログラムＣＰのグローバル計算とする。次に、ｌ∈Ｌｏｃｋ−Ｓｅｔ（Ｔi、ｃ）となるようなＣＰのスレッドＴiおよびロックｌについて、ＡＨ（Ｔi、ｌ、ｘ）を、ｘに沿ったＴiによるｌの最後の取得の後にＴiによって取得（および恐らく解除）されたロックのセットであると定義する。Ｌがロックのセットである場合、各取得履歴ＡＨは、各ロックにロックセット（そのロックの取得履歴）を関連付けるマップＬ→２Lである。ロックｌ1およびｌ2、ｌ1∈ＡＨ2（ｌ2）およびｌ2∈ＡＨ1（ｌ1）が存在しない場合、ＡＨ1およびＡＨ2が整合していると言う。上記の説明を次のように形式化することができる。
【００６７】
分解結果：ＣＰを２つのスレッドＴ1およびＴ2で構成された並列プログラムとする。次に、Ｔ1およびＴ2の制御状態ａ1およびｂ2のそれぞれについて、（ｉ）ａ1およびｂ2でＴ1およびＴ2のロックセットがそれぞれ互いに素であり、（ｉｉ）ａ1およびｂ2の取得履歴ＡＨ1およびＡＨ2がそれぞれ整合するように、制御状態ａ1およびｂ2にそれぞれ至るスレッドＴ1およびＴ2の局所的計算ｘおよびｙがある場合のみ、ａ1およびｂ2は同時到達可能である。スレッドがネスト化したロックを介してのみ通信する場合には上記の条件でも十分である。これらの取得履歴は、ロックセットに非常に類似した静的解析により追跡することができる。分解結果を活用するために、したがって、ＡＨを増補したアクセスイベントを形式（ｖ、Ｔ、Ｌ、ＡＨ、ａ、ｃ）のタプルとして定義する、ここで、（ｖ、Ｔ、Ｌ、ａ、ｃ）はアクセスイベントであり、ＡＨは現在の取得履歴である。ブロック２２の警告低減は２つの段階で進行する。
【００６８】
段階Ｉ：取得履歴の整合性が同時到達可能性にとっての必要条件であるため、ｅi＝（ｖ、Ｔ、Ｌi、ＡＨi、ａi）およびＡＨ1およびＡＨ2が不整合の場合、警告（ｅ1、ｅ2）はすべて落とされる。本発明の例では、（ｅ1、ｅ3）はこの段階で落とされる。
【００６９】
段階ＩＩ：残りの警告に関しては、関係⊆ａより弱い新しい取得履歴に基づく技
術を課している。ＡＨ1およびＡＨ2という２つの取得履歴が与えられた場合、各ロックｌについてＡＨ1（ｌ）⊆ＡＨ2（ｌ）である場合、
【００７０】
【数１０】
2010517163.tif 000012
【００７１】
であると言う。即時であるが重要な結果は、次のとおりである。
【００７２】
【数１１】
2010517163.tif 000013
【００７３】
となるように取得履歴タプルＡＨ、ＡＨ1、およびＡＨ2が与えられた場合、ＡＨがＡＨ2と整合しているということは、ＡＨがＡＨ1と整合していることを示唆している。
【００７４】
より弱い取得履歴に基づく技術：スレッドＴの共通の計算
【００７５】
【数１２】
2010517163.tif 000014
【００７６】
に沿ったｅ2＝（ｖ、Ｔ、Ｌ2、ＡＨ2、ａ2、ｃ2）の前に発生するアクセスイベントｅl＝（ｖ、Ｔ、Ｌ1、ＡＨ1、ａ1、ｃ1）について、Ｌ1⊆Ｌ2の場合には、
【００７７】
【数１３】
2010517163.tif 000015
【００７８】
および、ａ1＝ａ2またはａ1のいずれかは書き込み動作である。
【００７９】
本発明の例では、イベントｅ1、ｅ3、およびｅ4の取得履歴はそれぞれ、ＡＨ1＝｛（ｌｋ１、｛ｌｋ２｝）｝、ＡＨ3＝｛（ｌｋ２、（０）｝、およびＡＨ4＝｛（ｌｋ２、（０）｝である。明らかであるが、
【００８０】
【数１４】
2010517163.tif 000016
【００８１】
であれば、
【００８２】
【数１５】
2010517163.tif 000017
【００８３】
である。したがって、（ｅ1、ｅ3）を落とし、（ｅ1、ｅ4）を保持する。この事実を洞察すれば、アクセスｅ3に至るＴ2の任意の局所的計算は、アクセスｅ4を通過しなければならないということになる。さらに、
【００８４】
【数１６】
2010517163.tif 000018
【００８５】
であるので、ＡＨ1とＡＨ3が整合している場合、ＡＨ1とＡＨ4が整合しているということになる。したがって、Ｔ1およびＴ2は分解結果によりネスト化したロックを介してのみ通信するので、警告（ｅ1、ｅ3）に対応するデータ競合を実現している計算がある場合には、（ｅ1、ｅ4）を実現している計算も存在している。そのため、（ｅ1、ｅ4）を支持し、（ｅ1、ｅ3）を落としてもよい。
【００８６】
取得履歴に基づくカバー：一般に、アクセスイベントｅkに到達するパスは複数ある可能性があるが、その場合、対（ｅi、ｅk）を落とす前に、ｅkに到達するプログラム中の各パスに沿ってアクセスイベント
【００８７】
【数１７】
2010517163.tif 000019
【００８８】
が存在することを確認する必要があることに留意されたい。これは、アクセスイベントのカバーについての概念を使用することにより、達成することができる。アクセスイベントｅが与えられると、ｅのカバーは、
【００８９】
【数１８】
2010517163.tif 000020
【００９０】
となるようなアクセスイベントの集合ｃになる。このようなカバーは、ｅに対応するプログラム位置から後方のデータフロー解析により容易に決定できる。
【００９１】
ランキングによって低減を確実にすること：スレッドの同期が単なるロックに基づいていない場合、
【００９２】
【数１９】
2010517163.tif 000021
【００９３】
のいずれかに基づいた低減戦略は正確でないことに留意されたい。Ｃｈｏｉでは、実用的ではないかもしれないが落とされてもよい真の警告を特定するために、手動の検査ルーチンが提案されている。本発明は、ランキングを使用して正確性を確保することを提案している。本発明では、
【００９４】
【数２０】
2010517163.tif 000022
【００９５】
に基づいた警告は１つも落とさず、警告をランク付けするだけである。次に、順位の低い警告が検査されるかどうかは、順位の高い警告が偽りの警告であると判明する事実に左右される。
【００９６】
図６を参照して、コンピュータプログラム検証用の競合警告を決定、生成、および低減するシステムおよび方法が示されている。ブロック３０２では、共有変数の決定がデータフロー解析を使用して行われる。ブロック３０４では、データフロー解析を用いて、どの変数がプログラムに書き込まれるかを判断することにより、真の変数更新のみを決定する。これは変数空間を制限することになる。
【００９７】
ブロック３０６では、ロックポインタのポイントツー集合が、要約関数を用いた文脈依存のエイリアス解析において決定される。ブロック３０８では、ロックセットおよび取得履歴は、好ましくも、共有変数がロックポインタの不可欠なエイリアス解析でアクセスされるプログラム位置で決定される。
【００９８】
ブロック３１０では、各ポインタが同じクラスのポインタにのみエイリアスすることができるように、プログラム中のすべてのポインタ群を互いに素なクラスに分割することを行ってもよい。これは、各ポインタがブロック３１２の同じサブクラスのポインタにのみエイリアスすることができるように、プログラム中のすべてのポインタ群をサブクラスに再分割することを任意に含んでいてもよい。
【００９９】
ブロック３１４では、要約関数が共有変数およびロックのローカル参照を用いて関数の数を低減することにより、不可欠なエイリアス解析において低減される関数の数が計算される。ローカル参照は分断攻略戦略によって強化され、解析された要約関数の数を低減するために利用されてもよい。
【０１００】
ブロック３１６では、競合警告がロック取得パターンに基づいて生成／低減される。競合警告は警告数の低減も含んでいる。該警告は、互いに素なロックセットおよび取得履歴の整合性に基づいて生成される。競合警告は、ロックセットおよびロック取得パターンの両方に基づいた順位付け関係を使用して低減されるのが好ましい。ブロック３１８では、整合性が、２つのスレッド間のプログラム位置への同時到達可能性を表すロック取得履歴間で決定される。このように、不整合なロック取得履歴に関連する警告を無視して警告の数を低減することができる。ブロック３２０では、ロック取得履歴をランク付けするために「より弱い」整合性が判断され、より弱いロック取得履歴に関連する警告が削除される。
【０１０１】
本発明のシステムおよび方法は、コンピュータ検証システムおよび方法におけるデータ競合警告の改善／低減を提供するものである。実験結果を以下に示す。
【０１０２】
実験結果：ｋｅｒｎｅｌ．ｏｒｇからダウンロードされた、本発明による一連の１０個のリナックスデバイスドライバについての実験結果を下の表１に示している。この結果は、（ｉ）本発明の共有変数発見ルーチンの有効性、（ｉｉ）本発明の新しい要約に基づいたポインタ解析の拡張性および効率（時間列）、および（ｉｉｉ）有効性、およびその結果として警告低減技術を活用する重要性を明白に実証している。ＢＤＤＢＤＤＢエンジン、または不可欠なエイリアス解析用の本発明による新しい要約に基づく技術をそれぞれ使用する場合、ＢＤＤＢＤＤＢおよび時間列は、（ＣＦＧを構築するのに要した時間を含まないで−通常１分未満で）要した時間を指している。効率における改善は全く明白である。ＢＤＤＢＤＤＢエンジンは、第１の３つのドライバでのみ実行された。列をＷａｒおよびＡｆｔとラベル付けしている。Ｒｅｄは、最初のおよび
【０１０３】
【数２１】
2010517163.tif 000023
【０１０４】
関係に基づいた低減を適用した後に生成された警告の総数をそれぞれ示している。リナックスドライバには、これらの低減を適用した後でさえ、通常多数のコンテキストを発生する多数の小さな関数があるので、まだ多くの警告が生成される可能性がある。したがって、同じプログラム位置は、実質的に同じデータ競合ではあるが異なるコンテキストに起因する多くの警告を発生することができる。列Ａｆｔ．Ｃｏｎは、各プログラム位置につき１つだけ警告を生成し、コンテキストを取り除いた後に残された警告の数を示している。
【０１０５】
【表１】
2010517163.tif 000024
【０１０６】
根本的な関心のある問題であるデータ競合検出は、広範囲にわたる研究の対象であった。動的なランタイム検出、静的解析、およびモデル検査を含む問題に取り組むために、多くの技術が活用された。そのようなアプローチの１つが、静的解析の使用を活用して、ランタイム解析によって実証される必要があるデータ競合警告の数を低減するＣｈｏｉである。該ランタイム技術の利点は偽の警告がないことである。他方、不利な点は、コードを計測する際に発生する追加費用および狭い適用範囲であり、そのいずれも、特に並行プログラムとの関連においてコードの大きさが増加するにつれて悪化する。さらに、ランタイム検出技術は、デバイスドライバのようなアプリケーションのオプションではないかもしれない所与のコードを実行できると仮定している。
【０１０７】
モデル検査は所与のプログラムの状態空間の効率的な探査であり、並列プログラムの検証で採用されたもう１つの強力な技術である。しかしながら、状態空間爆発は、１０，０００行のコードを超える並列プログラムの検証を困難にしたので、現在の最新技術を用いて大規模な実コードをデバッグするオプションにはなりえない。
【０１０８】
近年、データ競合検出の静的解析技術を適用する活動が活発化してきた。そのような技術の利点は、大規模なプログラムへと拡張できることにある。不利な点で重要なのは、静的解析はオリジナルプログラムの非常に抽象化されたバージョンで機能するので、該バージョンは十分に改良されず、偽の警告を多数発生できることである。
【０１０９】
本発明の原理によるアプローチは、静的解析を強化し、偽りの警告の数を低減する目標により該解析をより洗練されたものにする。正確な競合検出プロシージャへのステップは、（ｉ）正確な共有変数の発見と、（ｉｉ）不可欠なロックセットを決定するための拡張可能な文脈依存のポインタ解析と、（ｉｉｉ）効果的な警告低減を含んでいる。既存の相関に基づく技術を強化するために使用することができる、新しい共有変数検出解析を説明した。本発明では、競合検出解析の拡張性および正確性の両方を確保する、新しい拡張可能な文脈依存の不可欠なエイリアス解析を提供した。
【０１１０】
従来の文脈依存のエイリアス解析技術は、ＣよりＪａｖａ(登録商標）でよりうまくいくことが示されたが、一方、他の技術は単に全くポインタ解析を使用しないので該技術の正確性が制限されてしまう。
【０１１１】
本発明の原理によれば、Ｃｈｏｉで与えられた既存のロックセットに基づいた解析よりもより正確であることが証明可能な、新しい２段階にわたる取得履歴に基づいた警告低減技術が採用された。一連のリナックスドライバに関する実験結果は、有効性すなわち本発明の原理の正確性と拡張性の両方を実証している。
【０１１２】
並列プログラムについて、高速で正確な静的データ競合を検出するシステムおよび方法の好ましい実施形態（例示となるように意図したものであり、限定するものではない）を説明したが、当業者には、上記の教示に照らして変更および変形を行うことができることに留意されたい。したがって、添付の請求項によって略述されるような本発明の範囲と精神を逸脱することなく、開示された特定の実施形態において、変更がなされてもよいことが理解されるべきであろう。このように、特許法により要求された詳細および特殊性で本発明の態様を説明したが、特許証によって保護された要求および所望のものは、添付の請求項で説明されている。
「関連出願情報」
本出願は、参照によって本書に組み込まれている２００７年１月２４日に出願された仮出願番号第６０／８８６，３０４号に対する優先権を主張する。
【図面の簡単な説明】
【０１１３】
【図１】１つの例示的な実施形態による、データ競合警告を検出、生成するシステムおよび方法を示すブロック図およびフロー図である。
【図２】本発明の原理による、共有変数検出用のデータフロー解析を実行するプログラムコードを示している。
【図３】本発明の原理による、文脈依存のポインタ解析における計算プロシージャ要約が実証されるプログラム例を示している。
【図４】本発明の原理による、ロックポインタ解析の要約計算の例示的なプログラムコードを示している。
【図５】本発明の原理による、警告低減を実証する例示的なプログラムコードを示している。
【図６】別の例示的な実施形態による、データ競合警告を検出、生成、および低減するシステムおよび方法を示すブロック図およびフロー図である。
【図１】
2010517163.tif 000025
【図２】
2010517163.tif 000026
【図３】
2010517163.tif 000027
【図４】
2010517163.tif 000028
【図５】
2010517163.tif 000029
【図６】
2010517163.tif 000030
【手続補正書】
【提出日】平成21年7月15日(2009.7.15)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】請求項２４
【補正方法】変更
【補正の内容】
【請求項２４】
前記クラスに分割することは、各ロックポインタが同じサブクラスのポインタにのみエイリアスすることができるように、前記プログラム中の前記すべてのポインタ群をサブクラスに再分割することを含む、請求項２３に記載の方法。
【国際調査報告】
2010517163.tif 000031
2010517163.tif 000032