(57)【特許請求の範囲】
【請求項１】
プログラムを記録する記録媒体から該プログラムを読み取るコンピュータが実行する検証方法であって、
プロダクトコントロールグラフ上の同期プリミティブによる制約を使用して、静的に到達不可能なノードを取り除くことと、
前記プロダクトコントロールグラフ上で静的プログラム解析を行い正常な不変条件を導き出すことと、
前記の導き出された不変条件を使用して静的に到達不可能なノードをさらに取り除くことと、
次の解析または検証のために、結果として得られたプロダクトコントロールグラフを用いて正当性の違反を検出することと、
を有する、並行プログラムの検証方法。
【請求項２】
静的に到達不可能なノードを取り除いて静的プログラム解析を行うことを、これ以上ノードを取り除くことができなくなるまで反復して繰り返す、請求項１に記載の方法。
【請求項３】
前記プロダクトコントロールグラフを、前記並行プログラムのスレッドまたはプロセス中のトランザクション限界に対応する制御状態について構築する、請求項１に記載の方法。
【請求項４】
前記静的プログラム解析は、並行プログラムに対する定数伝搬、範囲解析、八面体解析、および多面体解析の１つまたは２つ以上を含む、請求項１に記載の方法。
【請求項５】
異なる静的プログラム解析を、前記解析によって得られた精度を向上させる順に行なう、請求項４に記載の方法。
【請求項６】
前記静的プログラム解析を並行プログラムに関する抽象解釈を用いて行なう、請求項１に記載の方法。
【請求項７】
前記抽象解釈は、前記並行プログラムの異なるスレッドまたはプロセスの間で共有される状態に関する一貫性を維持するのに融合動作を用いる、請求項６に記載の方法。
【請求項８】
前記プロダクトコントロールグラフを、前記並行プログラムのスレッドまたはプロセス中のトランザクション限界に対応する制御状態について構築する、請求項１に記載の方法。
【請求項９】
正当性の潜在的な違反に対応する、前記プロダクトコントロールグラフ中のパスを、警告として報告する、請求項１に記載の方法。
【請求項１０】
次の解析または検証を前記警告に対応するプログラムスライス上でのみ行なう、請求項９に記載の方法。
【請求項１１】
次の解析または検証は、正当性の違反を示す実行トレースを発生するのにモデル検査を用いることを含む、請求項１に記載の方法。
【請求項１２】
データフロー解析によって導き出された不変条件を使用して、状態空間の低減によってモデル検査の拡張性を改善する、請求項１１に記載の方法。
【請求項１３】
コンピュータ読み取り可能なプログラムを有し、該コンピュータ読み取り可能なプログラムは、コンピュータで実行されたとき該コンピュータに請求項１のステップ群を実行させる、コンピュータ読み取り可能な記録媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明はコンピュータ検証に関し、特に同期制約(synchronization constraints)、正常な不変条件(sound invariants)、およびモデル検査(model checking)を用いることによって警告を低減するシステムおよび方法に関する。
【０００２】
本出願は、参照によってここに組み込まれる、２００７年１１月４日に出願された仮出願第６０／９７６、２８２号に対する優先権を主張する。
【背景技術】
【０００３】
具体的なエラートレースがソフトウェアのデバッグに重要である。あいにく、並行性(concurrency)に関連したバグ用のエラートレースを生成することは周知のように困難である。これに対する主要な理由の１つは、並行プログラムが、該並行プログラムの解析を困難にするスレッド間の微妙な相互作用を含み、動作が複雑であることにある。この複雑な動作は、所与の並行(concurrent)プログラムを有する種々のスレッドの局所処理の間の多くの考えられるインターリービングの結果である。
【０００４】
並行プログラムに対するデバッグ技術の開発は、現在、進行中のマルチコア革命による活発な研究の領域である。テスト、静的解析、およびモデル検査はすべて研究されてきたが、欠点がないわけではない。テストは、明らかに逐次プログラムに対する最も効果的なデバッグ技術であった。しかしながら、テストを並行プログラムに適用する主要な課題は、当然、スレッド間の多くの考えられるインターリービングであり、意味のある範囲メトリクス(coverage metrics)を提供するのは難しい。さらに、大抵、並行システムは、その再生性を確保するのは難しいので、すなわち同一の入力が並行プログラムの異なる実行において異なる結果を生じることがあるので、非決定論(non-determinism)を本来的に有している。
【０００５】
静的解析の使用は、データレース(data races)およびデッドロック(deadlock)のような標準の並行バグに対するある程度の成功を収めた。該データレースは、所与のプログラムの２つの異なるスレッドが共に同時に共有変数にアクセスできる場合に発生し、該アクセスの少なくとも１つは書き込み動作である。データレースをチェックすることは、並行プログラムのデバッグにおける重要な最初のステップであることが多い。確かに、プログラム中のデータレースの存在は通常、該プログラムの挙動を非決定論的にし、そのため、より多くの複雑で興味ある特性に対し該挙動について推論することが困難である。
【発明の開示】
【発明が解決しようとする課題】
【０００６】
しかしながら、静的解析の主な欠点は、真のバグに対応しない、多くの偽の警告を生成する可能性が高いということである。これは、プログラマに偽の警告から真のバグを選別する負担を負わせることになる。プログラマの見地から、これは明らかに望ましくない。偽の警告の割合がある閾値を越えた場合、プログラマは、そのような技術の使用を簡単にやめることがある。
【０００７】
モデル検査は、具体的なエラートレースのみを生成し、したがって警告を検査し該警告が真のバグかどうか決定することをプログラマに頼らないという利点を持つ。しかしながら、状態急増問題がその拡張性を厳しく制限している。モデル検査が大きな現実の並行プログラムへ拡張することを期待するのは非現実的である。
【課題を解決するための手段】
【０００８】
プログラムを検証するシステムおよび方法は、プログラム中の潜在的な問題に対する警告を生成することを含む。該警告は、経費(overhead expense)の順に適用される１つまたは２つ以上の静的解析方法を実行することによって除去される。具体的なエラートレースが、モデル検査を用いて残りの警告のために生成される。
【０００９】
並行プログラムの検証のシステムおよび方法は、プロダクトコントロールグラフ(product control graph)についてデータフロー解析を行い正常な不変条件を導き出すこと、導き出された不変条件を用いて、プロダクトコントロールグラフから静的に到達不可能な状態に対応するノードを取り除くこと、プロダクトコントロールグラフを次の解析／検証に用いて正当性の違反を検出すること、を含んでいる。
【００１０】
プログラム検証システムは、コンピュータ読み取り可能な媒体に格納され、実行時に、プログラムを解析して該プログラムの潜在的な問題を生成するように構成された警告発生手段を含む。警告フィルターが、コンピュータ読み取り可能な媒体に格納され、実行時に、経費の順に適用される１つまたは２つ以上の静的解析方法を実行するように構成されている。モデル検査器が、コンピュータ読み取り可能な媒体に格納され、実行時に、モデル検査を用いて残りの警告の具体的なエラートレースを生成するように構成されている。
【００１１】
これらおよび他の特徴および利点は、添付の図面に関して読まれるべき、その例示となる実施形態に関する以下の詳細な説明から明白になるであろう。
【発明を実施するための最良の形態】
【００１２】
本開示は、次の図面を参照する、好ましい実施形態の以下の記述においてその詳細を提供する。
【００１３】
コンカレンシバグエリミネータ(CoBE)と呼ぶことができる新しいフレームワークが提供される。このフレームワークは、コンカレンシバグに対する具体的なエラートレースを生成する。ソースコードから始まって、CoBEの目標は、証拠を正確に、効率的に、そして完全に自動的に生成することである。これは、一連の静的解析技術を、同時に該静的解析技術の既知の落とし穴を避けながら、該静的解析技術の個々の強みを利用するように、モデル検査と組み合わせることによって達成される。
【００１４】
本方法は広い利用可能性を有するが、本願の発明者らは本技術の有用性を説明する手段としてデータレースバグを選んでいる。データレースバグに対する具体的なエラートレースを生成するために、１つのステップは、所与の並行プログラム中でそのようなバグが発生し得る位置を切り離すことである。元のプログラムは、一般に大きくなる可能性があるので、この初期の警告生成は拡張可能である。静的解析をここで用いることができる。
【００１５】
静的なレース警告生成には３つの主なステップがある。まず、共有変数がアクセスされる各スレッドの制御位置をすべて決定する。次に、これらの関心のある位置の各々に保持されたロック群が算出される。（ｉ）同一共有変数ｓｈがアクセスされ、（ｉｉ）該アクセスの少なくとも１つが書き込み動作であり、（ｉｉｉ）互いに素なロックセットが保持される、異なったスレッド中の複数の制御位置対がｓｈへの潜在的データレースサイトを構成し、警告が出される。偽の警告の数を減らすために、本発明では警告生成を状況依存的（context-sensitively）に行う。したがって、各警告は１対の制御位置とそのそれぞれのスレッドコンテキストとを含んでいる。
【００１６】
前述したように、静的データレース警告技術に関する問題は、真のバグに相当しない偽の警告が多数生成される可能性があるということである。静的データレース検出技術は通常、スレッドの条件文を無視するので、潜在的なデータレースサイトとして印を付けられた１対の制御位置は、所与の並行プログラムのいかなる実行においても簡単には到達できないことがある。
【００１７】
一方、原則として、所与の警告に対応する１対の制御位置が同時に到達可能であるか、および警告が真のバグであるかどうかを判断するのにモデル検査を用いることができる。実際には、該モデル検査には状態急増の問題がある。したがって、モデル検査を利用して警告の証拠を生成しようとする前に、単なるロックセットベースの方法よりも高度な技術を利用してより多くの偽の警告を取り除く必要があり、さもなければ、（たとえ特定のコンテキストにおいてでも）モデル検査によって多数の警告を探索するコストが問題になる。言いかえれば、該モデル検査は最後の手段の道具としてのみを用いられる。
【００１８】
本発明の原理に従う実施形態は偽の警告を除去するが、該原理は完全に自動で、信頼性があり、完全で、拡張可能である。
【００１９】
潜在的データレースサイトとしてフラグを立てられたスレッドT1およびスレッドT2中の１対の制御位置c1およびc2をそれぞれ考える。この警告は、c1およびc2の対毎の到達可能性（pairwise reachability）とも呼ばれる、T1およびT2を持つ所与の並行プログラムの到達可能なグローバル状態ａがそれぞれ制御状態c1および制御状態c2に存在する場合にのみ、真のバグとなる。c1およびc2の対毎の到達可能性を除外するために、本発明では、偽の警告に対して、精度は高いが拡張性が低い一連の静的解析を用いている。本発明の目的は、ｃ1およびｃ2の対毎の到達不可能性をできるだけ安価に推定することである。
【００２０】
このために、本発明では以下の事項を利用する。１）同期制約：並行プログラムが、スレッド間で許可されたインターリービング群を制限するために、ロック（locks）、ランデブー（rendezvous)(Wait/Notify)、ブロードキャスト（  broadcasts）(Wait/NotifyAll）等の種々の同期プリミティブを用いるということを利用する。本発明者らは、これらのスケジューリング制約を単に利用することによって、多くの偽の警告について、対応する制御位置の対毎の到達不可能性を静的に推定できることを示す。２）正常な不変条件：対毎の到達不可能性を推定するために、並行プログラムの定数畳み込みおよび区間、八面体および多面体不変条件のような正常な解析を使用し、それによって同期制約の使用によって得た偽の警告の削減を超える、偽の警告の削減を達成できることを示す。
【００２１】
さらに、同期制約と正常な不変条件を、実際、相乗的に組み合わせて、それらを分離して適用することによって得られるよりもさらに多くの警告を除外することができる。他のステップは、残りの警告に対する具体的なエラートレースを生成するためにモデル検査を利用することである。モデル検査は、（ｉ）各スレッドを、警告を特定するコンテキストにおいてのみ探索すること、（ｉｉ）記号技術の、大きな状態空間を探索する能力を用いること、（ｉｉｉ）半順序の削減、（ｉｖ）探索される必要のあるインターリービング群を削減するために同期制約および正常な不変条件から得られた対毎の到達不可能性の情報を使用すること、によって、本発明が改善しようとしている状態急増の問題がある。項目（ｉ）と項目（ｉｖ）は、本発明者の知る限りでは、モデル検査に利用されたことがない。本発明の方法の有用性は、一連のリナックスデバイスドライバ上で実証されている。
【００２２】
ここに記載された実施形態は、完全にハードウェア、完全にソフトウェア、またはハードウェア要素およびソフトウェア要素の両方を含んでいてもよい。好ましい実施形態において、本発明は、ファームウェア、常駐ソフトウェア、マイクロコードなどを含むが、これらに限定されないソフトウェアで実施される。
【００２３】
実施形態は、コンピュータまたは任意の命令実行システムによってまたはそれらに関連して使用されるプログラムコードを出力する、コンピュータで使用可能な媒体またはコンピュータで読み取り可能な媒体からアクセス可能なコンピュータプログラム製品を含んでいてもよい。コンピュータで使用可能な媒体すなわちコンピュータで読み取り可能な媒体は、命令実行システム、命令実行装置、または命令実行デバイスによってまたはそれらに関連して使用されるプログラムを、格納、通信、伝搬、または搬送する任意の装置を含んでいてもよい。該媒体は、磁気的、光学的、電子、電磁気的、赤外線、または半導体のシステム（または装置またはデバイス）、または伝搬媒体であってよい。該媒体は、半導体または固体のメモリ、磁気テープ、リムーバブルコンピュータディスケット、ランダムアクセスメモリ（ＲＡＭ）、読み取り専用メモリ（ＲＯＭ）、剛性磁気ディスク、および光ディスク等のような、コンピュータで読み取り可能な媒体を含んでいてよい。
【００２４】
ここで、同じ参照番号が同一または類似の要素を示す図面、および最初に図１を参照すると、本発明の原理による、並行プログラムをデバッグするシステム／方法を示すブロック／フローチャートが具体的に図示されている。
【００２５】
ブロック１０２で、解析される並行プログラムが与えられる。ブロック１０４で、該プログラム中の静的に算出されたロックセット情報を用いてデータレース警告が生成される。ブロック１０６で、偽の警告は除去され、該警告は信頼度に基づいてランク付けされる。既存の静的技術はこの段階で停止し、プログラマに頼りそれが真のバグかどうかを判断するために該警告を手動で検査する。
【００２６】
本発明の原理にしたがって、この負担がプログラマから取り除かれる。ブロック１０８で、精度が高いが拡張性が低い一連の静的解析を用いて、警告が偽りであるかどうかをできるだけ安価に判断する。ブロック１０９で、これらの静的解析は、同期プリミティブの使用から生じるインターリービング制約と、定数伝播、値域、八面体、および多面体の解析のようなデータフロー解析によって算出された正常な不変条件とを利用する。
【００２７】
ブロック１１０で、モデル検査を利用して残りの警告に対する具体的なエラートレースが生成される。モデル検査の拡張性は、スレッドコンテキストによって特定されるプログラムの同じ局所部分の探索によって確保される。
【００２８】
（ｉ）現実のコードに利用可能で、（ｉｉ）拡張可能で、（ｉｉｉ）正確であり、および（ｉｖ）具体的なエラートレースを生成する、並行ソフトウェアのデータレース警告を生成する新規な方法が考案されている。この新規な方法は、具体的なエラートレースを、人間が介在することなくソースコードから直接自動的に生成することによって、プログラマから大幅に負担を取り除く。さらに、現在用いられているものよりも高度な静的警告削減技術が提供されている。既存の技術はその大部分がロックセットに基づいている。本発明の実施形態はロックセットをベースにした技術を越えており、様々な静的解析を利用して、誤った警告の割合を著しく低減する。例としてデータレースバグを用いて、静的解析とモデル検査とを組み合わせて具体的なエラートレースを生成する効果的な方策を示す。
【００２９】
共有変数を用いて通信し、ロック、ランデブー等の標準プリミティブを用いて互いに同期する複数のスレッドからなる並行プログラムを考える。
【００３０】
プログラム表現：並行プログラムの各スレッドは、１群の手順Ｆ、特殊な入力手順メイム(maim)、および１群のグローバル変数Ｇによって表される。各手順ｐ∈Ｆは、仮引数args(p)のトピック、戻り型tpローカル変数L(p)、および制御の流れを表す制御フローグラフ(CFG)に関連付けられている。制御フローグラフは、１群のノードN(p)と，N(p)のノード間の１群のエッジE(p)とを含んでいる。各エッジｍ→ｎ∈Ｅ（ｐ）は、割り当て、他の手順への呼び出し、リターン文、エッジの実行を保護する条件である動作、または同期動作と関連付けられている。手順ｐに対するCFGの動作は、群
【００３１】
【数１】
0005337454.tif 000002
【００３２】
中の変数ｐを指すことがある。
【００３３】
マルチスレッド化されたプログラム
【００３４】
【数２】
0005337454.tif 000003
【００３５】
は、Ｎ＞０のある一定のＮについて１群のスレッドT1、．．．、TNと、１群の共有変数Ｓとを含んでいる。各スレッドT1は単一のスレッド化されたプログラム
【００３６】
【数３】
0005337454.tif 000004
【００３７】
と関連し、入力関数eiを含んでいる。なお、すべての共有変数ｓ∈Ｓが各CFG
【００３８】
【数４】
0005337454.tif 000005
【００３９】
のグローバル変数であることに留意されたい。複数のスレッドは、ロック、ランデブー、およびブロードキャストのような標準プリミティブを用いて互いに同期する。これらのプリミティブのうち、最も一般的に用いられるのはロックである。ランデブーは、例えば、Apache(登録商標)のようなウェブサーバおよびFirefox(登録商標)のようなブラウザなどのウェブサービス、および例えば、autofsなどのデバイスドライバのようなニッチなアプリケーションに限定的に使用される。ブロードキャストは非常に稀で、オープンソースコードで見つけるのは難しい。したがって、本発明では、以下に説明するロックとランデブーを介して同期する複数のスレッドからなる並行プログラムを考えるものとする。
【００４０】
ロック(Locks)。ロックは共有リソースへの互いに排他的なアクセスを実行するために使用される標準プリミティブである。
【００４１】
ランデブー(Rendezvous)。ランデブーは、Java(登録商標)のWait/NotifyプリミティブおよびPthreadライブラリのpthread_cond_wait/pthread_cond_send関数によって動機づけられる。スレッドTiのランデブー遷移は、それぞれ形式ａ！およびｌ？のランデブー送信動作およびランデブー受信動作と呼ばれる遷移によって表される。ｌ！およびｌ？と呼ばれる１対の遷移をマッチングと呼ぶ。ランデブー遷移tr1：スレッドTiの
【００４２】
【数５】
0005337454.tif 000006
【００４３】
は、形式tr2：
【００４４】
【数６】
0005337454.tif 000007
【００４５】
のマッチングランデブー遷移が存在するように、ローカルな状態ｃにおいてTi以外のスレッドTjが存在する場合で、かつ存在する場合に限り、並行プログラムのグローバルな状態ａにおいて有効になる。ランデブーを実行するためには、対の送信遷移tr1と受信遷移tr2が共に、１つの原子ステップにおいて、それぞれｂ、ｄに遷移するT1、Tjと同期して始動されなければならない。なお、Java(登録商標)では、Notify(送信)ステートメントは、マッチングWaitステートメントが現在有効であるかどうかに関係なく、常に実行できることに留意されたい。しかしながら、説明を簡単にするために、WaitステートメントとNotifyステートメントは常に一致し、さもなければ静的警告の生成があまりにも多くの偽の警告を列挙するものとする。
【００４６】
準備段階：プログラム解析：ここで、異なるプログラム位置でのプログラム変数の値を特徴づけるアサーション(assertion)を使用して、データフロー解析の背後にある基本理論を提示する。本発明の手法は整数および実数のような無限の領域による推論を含んでいるので、そのような解析が構築される基準として抽象解釈(abstract interpretation）を用いる。抽象解釈を簡潔に説明する。
【００４７】
【数７】
0005337454.tif 000008
【００４８】
をシーケンシャル（単一のスレッド化された）プログラムのCFG表現とする。説明を簡単にするために、
【００４９】
【数８】
0005337454.tif 000009
【００５０】
が他の手順に対する呼び出しを含まない単一の手順を含むものとする。
【００５１】
【数９】
0005337454.tif 000010
【００５２】
に含まれる変数はすべて整数であるものとする。CFGの各エッジは割り当てまたは条件によってラベル付けされる。抽象領域
【００５３】
【数１０】
0005337454.tif 000011
【００５４】
は、部分的な順序包含関係
【００５５】
【数１１】
0005337454.tif 000012
【００５６】
によって順序付けられた、選択されたアサーション言語
【００５７】
【数１２】
0005337454.tif 000013
【００５８】
から引き出されたアサーションφを含んでいる。各オブジェクト
【００５９】
【数１３】
0005337454.tif 000014
【００６０】
は１群のプログラム状態［［ａ］］を表している。解析については、本発明では
【００６１】
【数１４】
0005337454.tif 000015
【００６２】
にわたって定義される以下の動作を必要とする。
【００６３】
a)Join(ジョイン）：
【００６４】
【数１５】
0005337454.tif 000016
【００６５】
が与えられたものとすると、join
【００６６】
【数１６】
0005337454.tif 000017
【００６７】
は、
【００６８】
【数１７】
0005337454.tif 000018
【００６９】
となるような最も小さな抽象オブジェクト
【００７０】
【数１８】
0005337454.tif 000019
【００７１】
となる。
【００７２】
それはCFGのジョインポイントで使用される。
B)Meet: meet
【００７３】
【数１９】
0005337454.tif 000020
【００７４】
は、論理積(logical conjunction)に相当し、条件付き分岐で用いられる。
c)Abstract post condition（伝達関数）
【００７５】
【数２０】
0005337454.tif 000021
【００７６】
は、割り当ての作用をモデル化する。形式的には、ｍ→ｎはCFGのエッジである。post-condition
【００７７】
【数２１】
0005337454.tif 000022
【００７８】
は、
【００７９】
【数２２】
0005337454.tif 000023
【００８０】
によって表されたプログラム状態上のエッジを実行する作用を含む最も小さなオブジェクトを算出する。
D)Inclusion test
【００８１】
【数２３】
0005337454.tif 000024
【００８２】
は終了を調べる。
e)Widening operator 
【００８３】
【数２４】
0005337454.tif 000025
【００８４】
は、プログラムループを強制的に収束させる。
f)Projection operator
【００８５】
【数２５】
0005337454.tif 000026
【００８６】
は、範囲外変数を取り除く。
g)Narrowing operator
【００８７】
【数２６】
0005337454.tif 000027
【００８８】
は、解決策の改善に使用される。
【００８９】
プログラム
【００９０】
【数２７】
0005337454.tif 000028
【００９１】
と抽象領域
【００９２】
【数２８】
0005337454.tif 000029
【００９３】
が与えられたものとすると、各CFG位置l∈Lを抽象オブジェクトπ(l)にマッピングするマップ
【００９４】
【数２９】
0005337454.tif 000030
【００９５】
を求める。そのようなマップは、データフロー解析で使用される順方向伝播繰り返し
【００９６】
【数３０】
0005337454.tif 000031
【００９７】
によって反復して構築される。
【００９８】
繰り返しが収束すれば、すなわちある
【００９９】
【数３１】
0005337454.tif 000032
【０１００】
のすべてのｌ∈Ｌについて
【０１０１】
【数３２】
0005337454.tif 000033
【０１０２】
は、本発明の解析の結果である。しかしながら、格子
【０１０３】
【数３３】
0005337454.tif 000034
【０１０４】
が有限の高さでないか、昇鎖条件を満たさなければ、収束は確保されるとは限らない。一方、プログラム検証で一般に使用される領域の多くはこれらの条件を示さない。収束は、wideningとnarrowingの使用によって強制的に行われる。
【０１０５】
抽象解釈を用いて、区間、多面体、形状グラフ、および他の領域のような意味論的に豊かな領域にデータフロー解析を高めて、高度でデータ量の多い特性を検証してもよい。最近の３０年間にわたって多くの抽象領域が存在し、各抽象領域は、扱いやすい解析を得ることと複合属性を証明することとの間でのトレードオフを示してきた。
【０１０６】
区間制約定義(Interval Constraint Definition)。整数上の区間は
【０１０７】
【数３４】
0005337454.tif 000035
【０１０８】
となり、ここで、
【０１０９】
【数３５】
0005337454.tif 000036
【０１１０】
は整数または±∞、および
【０１１１】
【数３６】
0005337454.tif 000037
【０１１２】
である。記号
【０１１３】
【数３７】
0005337454.tif 000038
【０１１４】
によって空の区間を示す。IがZ上の全ての区間の群を示すものとする。区間領域は
【０１１５】
【数３８】
0005337454.tif 000039
【０１１６】
の形式のアサーションから成り、各変数をその考えられる値を含んだ区間に関連付けている。
【０１１７】
Join、meet、post condition、inclusionなどの区間領域に対する領域動作は効率的に行うことができる。区間領域は相関的(non-relational)でない。該領域は他の変数の区間と無関係な各変数の区間を算出する。その結果、該領域は、より複雑で相関的な不変条件を必要とする多くの一般的に発生する状況を処理できない場合がある。多面体領域は表現に富む(expressive)線形不変条件を算出し、極めて強力である。しかしながら、この強力さは、post condition、join、projectionなどのような指数関数の時間領域動作を持つことを犠牲にするところからきている。八面体(octagonal)の領域は区間領域と多面体(polyhedra)領域との間の良い妥協である。
【０１１８】
八面体(Octagons)。八面体領域は、プログラム変数の全ての考えられる対に対する、ｘ−ｙ、ｘ＋ｙなどのようなプログラム表現にわたって区間を算出することによって、区間領域を十分に拡張する。該領域は、制約のグラフ表示、および全ての対の最短路アルゴリズムに基づいた正準ファーム(canonical farm)を用いて、post、join、およびprojectionのような動作を効率的に行うことができる。
【０１１９】
図２を参照すると、警告低減およびエラートレース生成システム／方法の実施を示すブロック図／フローチャートが例で示されている。ブロック２０２で、警告が生成される。古典的に、静的なレース警告の生成には３つの主なステップがある。１）各スレッド内の、共有変数がアクセスされるすべての制御位置を決定する。２）ロックセット、すなわちこれらの制御位置の各々で保持されるロック群を算出する。３）（ｉ）同じ共有変数shがアクセスされる、（ｉｉ）アクセスの少なくとも１つが書き込み動作である、（ｉｉｉ）互いに素なロックセットが保持される、異なるスレッドにおける制御位置の対はshの潜在的なデータレースサイトを構成し、警告が出される。アクセスイベントの概念は、データレース警告を形式的に定義することに有用である。
【０１２０】
アクセスイベントは(V,T,L,CAN,a,c)形式のタプル(tuple)であり、ここで、ｖは、
ロックセット（保持されたロック群)Lおよびアクセスタイプ（読み出しまたは書き込み）ａを持つスレッドTのコンテキストconの制御位置cで読み出されるかまたは書き込まれる変数である。ここで、コンテキストconは、入力関数から始まり、位置ｃを含んでいる関数呼び出しまでへの一連の関数呼び出しであると定義される。
【０１２１】
レース警告は、ｖが共有変数であり、
【０１２２】
【数３９】
0005337454.tif 000040
【０１２３】
で、a1またはa2の少なくとも１つが書き込みであるような、１対のアクセスイベント
【０１２４】
【数４０】
0005337454.tif 000041
【０１２５】
と
【０１２６】
【数４１】
0005337454.tif 000042
【０１２７】
である。データレース警告の生成における重要な課題は、（ｉ）共有変数アクセスを正確に決定すること、（ｉｉ）これらアクセスに対応する制御位置のロックセットを効率的に算出することである。本発明の主な目標は警告の生成ではなく該警告を解析する技術にあるので、本発明の説明をシール可能なフローとコンテキストに敏感なポインタエイリアス解析に焦点を当てる。
【０１２８】
ブートストラッピング（Bootstrapping）。フローとコンテキストに敏感なエイリアス解析は、２つの主な理由で、偽の警告数の急増を防ぐのに重要である。まず、不正確なポイント対解析（points-to analysis）は、一般に、共有変数の群に対する大きなポイント（points sets）につながり、次にすべてのアクセスが潜在的なデータレース位置としてフラグを立てられる必要がある。第２に、ロックは通常ロックポインタによってアクセスされるので、ロックセットを決定するためにポイントに対する解析を実行する必要がある。ロックセットを静的に算出する際に条件文を無視するので、ｌが、不可欠なロックセットｃと呼ばれる、ｃに至るあらゆるパスに沿って取得されれば、ロックｌを位置ｃのロックセットに含ませることができる。ロックポインタは、通常異なるコンテキストにおけるポイントに対する異なったロック（point-to different locks）であるので、これらのロックセットを算出するために使用されるポイントに対する解析はコンテキストに敏感であり、そうでなければ、空の不可欠なロックセットを生成することになる。これによって、偽の警告の数が爆発的に増えることになる。
【０１２９】
しかしながら、フローおよびコンテキスト依存のエイリアス解析は拡張可能ではないかもしれない。拡張性を確保するために、本発明では、（ｉ）分割および獲得（divideとconquer）、（ii）並列化（parallelization）と、（iii）関数要約（function summarization）との組み合わせを利用するブートストラッピングと呼ばれる技術を用いる。本発明は、非常に拡張可能なSteensgaardの解析を適用して、（Steensgaardの）ポイント対グラフ(points-to graph)によって定義されたポイント対群としてクラスタを識別することから始める。Steensgaardの解析は双方向であるので、これらのクラスタが事実、ポインタの同値類であることがわかる。重要なことには、Steensgaardのこれらのパーティションは、各ポインタを、それを含んでいる同値類のポインタにだけエイリアスされる(aliase)特性がある。これは、実際には、プログラム中のすべてのポインタに対してコンテキスト依存の解析を行う代わりに、ポインタ解析の問題をはるかに小さな副問題に分解するが、これは小クラスタごとに別個のポインタ解析を行うえば十分である。
【０１３０】
そのため、小サイズの各クラスタは、フローおよびコンテキスト依存のエイリアス解析の計算のより大きな複雑さを相殺する。（しきい値サイズによって決定される）濃度（cardinality）が高すぎてコンテキスト依存のエイリアス解析が実行できないSteensgaardパーティションが存在する場合、次にAndersenの解析がこれらの大きなパーティションに対して別々に行われて、各クラスタのサイズをさらに小さくする。以下のことに留意されたい。
【０１３１】
局所化（Localization）。本発明の適用において興味があるのは、ロックポインタおよび共有変数のエイリアスにあり、そのため少なくとも１つのロックポインタまたは共有変数を含んだクラスタについてのみサマリを構築する必要がある。ロックポインタは他のロックポインタにのみエイリアスするので、少なくとも１つのロックポインタを含んでいるクラスタのポインタはすべて実際にロックポインタになる。言いかえれば、通常大きくないロックポインタからのみなるクラスタを考慮する。これはサマリ計算を拡張可能にするのに重要である。確かに、ブートストラッピングを用いなければ、プログラム中のすべてのポインタのサマリを構築しなければならなかった。これは明らかに拡張性を制限していたであろう。さらに、ロックおよび共有変数のポインタは通常、関数の総数のごく一部分においてアクセスされるので、拡張性をさらに高めるこれらの関数のサマリのみを構築すれば十分である。
【０１３２】
並列化（Parallelization）。各クラスタは互いに無関係に解析することができ、並列化を利用することができる。
【０１３３】
ブロック２０４で、警告除去リングが行われる。ロックセットベースの静的警告生成技術の主な欠点は、真のバグを調べて選択するという大きな負担をプログラマにかける、あまりにも多くの偽の警告が生成されることがあるということである。正常な警告の方法は、ｗ2が真のデータレースであるという事実からｗ1も真のデータレースであると推定できる場合およびその場合に限り、警告ｗ1がｗ2よりも低いと言える警告に順序付けを課す静的技術を用いることに重点的に行う。次に、ｗ1を支持してｗ2は廃棄される。効果的であっても、上記のような順序付けベースの除去リングを受けない警告の大部分は依然として残ることがある。さらに改善され、かつロックセットベースの順序付け技術によって得られた警告低減に加えて警告低減を得るためにも使用できる、完全に自動で、正常および完全で、拡張可能な警告除去リング技術を次に説明する。
【０１３４】
対毎の到達可能性（Pairwise Reachability）。レース警告
【０１３５】
【数４２】
0005337454.tif 000043
【０１３６】
が与えられたとすると、それが真のバグであるためには、c1およびc2は対毎に到達可能でなければならない、すなわち、T1およびT2がグローバル状態ｓ中の制御位置c1およびc2にそれぞれあるように、２つのスレッドT1およびT2からなる並行プログラム
【０１３７】
【数４３】
0005337454.tif 000044
【０１３８】
の到達可能なグローバル状態ｓが存在しなければならない。時相論理(temporal logic)の言語において、レース警告が真のバグであるかどうかを調べる問題は、c1およびc2の対毎の到達可能性とも呼ばれる決定問題
【０１３９】
【数４４】
0005337454.tif 000045
【０１４０】
と定義することができる。
【０１４１】
警告が与えられたとすると、該警告を真のバグとして検証するためにモデル検査を用いることを考える前に、本発明では、より軽量でしたがってより拡張可能な技術を用いて真のバグを取り除く。この目的のために、スレッドT1とスレッドT2の抽象的に解釈されたバージョンからなる並行システムにおいて、対毎の到達可能性を決定する問題として静的な対毎の到達可能性の概念を導入する。該抽象解釈は警告低減に使用されている静的解析に依存する。なお、抽象解釈は通常、該所与のプログラムの挙動群に近似しすぎるので、対毎の到達可能性は、静的な対毎の到達可能性を意味しているがその逆はあり得ないことに留意されたい。言いかえれば、レース警告に含まれる２つの制御状態が静的に対毎の到達可能でなければ、警告は偽りのものとして廃棄することができる。
【０１４２】
静的な対毎の到達可能性（Static Pairwise Reachability）。主な目標は、c1およびc2が静的に対毎の到達可能にならないように制御位置c1およびc2に関するできるだけ多くの警告を識別することである。このために、本発明では、同期制約と正常な不変条件を共に利用する種々の静的解析技術を用いる。
【０１４３】
例。本発明の方策を、異なるスレッドがPage Alloc関数とPage#Dealloc関数を実行する、図３に示す並行プログラムの例を用いて説明する。カウンタpg#countは、今までに割り当てられたページの数を格納する。Page_Allocルーチンは、新しいページを割り当てようとする。既に割り当てられたページの数が最大許容限界LIMITに達すると、該ルーチンは、page_deallocルーチンおよび信号で送られた待ちスレッド（b3）によってページの割り当てが解除されるまで待つ（a3）。簡単のために、本発明は、pt_lock、pt_unlock、Pthread関数pthread_mutex_lock、pthread_mutex_unlack、pthread_cond_send、pthread_cond_waitのpt_send、pt_wait、を用いる。
【０１４４】
共有変数pg_countは、位置a4、a11、ｂ4、およびb9においてアクセスされる。位置a4およびb4にあるロックセットは（plk）であり、a11およびb9にあるロックセットは（count_lock）である。これらの２つのロックセットは互いに素であるので、対の制御位置(a4,b11)、（a4,b9）、(a11,b4)、及び(b4,b9)は全て、潜在的なデータレースが発生する可能性のある位置としてラベルが付けられる。しかしながら、（a4,b9）および（a11,ｂ4）は偽りである。重要なことには、これらの警告は、ここで説明するような簡単な静的解析によって偽りとして検出できる。
【０１４５】
ブロック２０６（図２）において、警告低減は、プログラムを解析する際に同期制約および正常な不変条件を用いて警告数を削減または除去する。
【０１４６】
同期制約による静的な対毎の到達不可能性（Static Pairwise Unreachability via Synchronization Ｃonstraints）:ランデブーの静的な対毎の到達可能性（Static Pairwise Reachability Foｒ Rendezvous）:レース警告（ａ4、ｂ9）を考えることから始める（図３）。Page_AllocとPage_Deallocをそれぞれ実行する２つのスレッドT1およびT2のみからなる並行プログラムが与えられたものとする。なお、位置a4および位置ｂ9が対毎の到達可能であるためには、スレッドT1はローカルな列ｘ：a1、a2、a3およびa4を実行しなければならず、一方、スレッドT2はローカルな列ｙ：ｂ1、ｂ6、B7、b8およびb9を実行しなければならないことに留意されたい。位置a3のステートメントは待ちステートメントであるので、T1がb3を実行するためには、T2はマッチング送信ステートメント、すなわちb3を実行しなければならない。b3がｙに沿って実行されないので、制御位置a4および制御位置b9は、２つのスレッドインスタンスでは対毎の到達可能でなく、したがって（a4,b9）はまのデータレースではない。事実、それが任意のｋ≧２のｋ-スレッドインスタンスのレースではないことも示すことができる。
【０１４７】
より一般には、スレッドT1およびT2における位置c1およびc2は、入力位置T1およびT2から始まり、c1およびc2に至る送信／待ちステートメントのマッチング列が存在する場合のみ、
【０１４８】
【数４５】
0005337454.tif 000046
【０１４９】
においてそれぞれ対毎の到達可能になる。したがって、上記のレースを取り除くために、各スレッドTの開始位置から
【０１５０】
【数４６】
0005337454.tif 000047
【０１５１】
で示す関心のある各位置ｃへの待ち／送信列の言語を、各スレッドについて静的に算出する。次に、スレッドT1およびT2における制御位置およびc2は、
【０１５２】
【数４７】
0005337454.tif 000048
【０１５３】
の場合にのみそれぞれ対毎の到達可能であり、逆もまた同様である、ここで、
【０１５４】
【数４８】
0005337454.tif 000049
【０１５５】
は、形式ａ？のあらゆる待ち記号をマッチング送信ａ！に反転させることによって、L（c,con,T）から得られた言語である。本発明の例では、
【０１５６】
【数４９】
0005337454.tif 000050
【０１５７】
で、一方
【０１５８】
【数５０】
0005337454.tif 000051
【０１５９】
と、したがって
【０１６０】
【数５１】
0005337454.tif 000052
【０１６１】
は共に｛ε｝に等しく、ここでεは空列である。
【０１６２】
【数５２】
0005337454.tif 000053
【０１６３】
であるので、(a4,b9)が偽の警告であると推定する。なお、ランデブー待ち動作ｐg_lim？を持つa3でのステートメントpt_wait（&pg_lim,&plk）を表したことに留意されたい。
【０１６４】
一般に、再帰的プログラムについては、所与のプログラム位置での待ちおよび送信の言語はコンテキストフリーである。したがって、それぞれT1およびT2内の関心のある位置ctおよびc2での送信言語L1および待ち言語L2を算出できたとしても、
【０１６５】
【数５３】
0005337454.tif 000054
【０１６６】
かどうかを調べることは決定不可能である。この問題を克服するために、本発明は２つの異なる過大近似技術を用いる。
【０１６７】
正規言語による過大近似（Over−approximation via Regular Languages）：本発明の目標は、スレッドTのコンテキストcon（本発明の警告生成がコンテキスト依存であるので、conは必要である）の位置cでの、正規の送信／待ちの言語の規則的近似
【０１６８】
【数５４】
0005337454.tif 000055
【０１６９】
を算出することである。本質的に、該過大近似は、ループおよび再帰的手順に対してKleenestar閉包をとることによって算出される。なお、原理的に、スレッドＴ自身のCFG Tcは、唯一の最終状態としてcを、そして初期状態としてTの入力関数の入力位置を持つオートマトンとして処理することができることに留意されたい。しかしながら、Tは非常にわずかの位置でしか他のスレッドと同期しないことがあるので、Tcのほとんどの遷移は空になる。しかしながら、本発明では、（ｉ）大きなプログラムに対して、（ｉｉ）警告によって特定された各コンテキストにおいて、効率的に算出可能な
【０１７０】
【数５５】
0005337454.tif 000056
【０１７１】
を受け取る小さな正規のオートマトンを求める。これらの目標を達成するために、本発明では要約を用いる。コンテキストconが、fciがｆiにおいて関数fi+1に対する呼び出しである関数呼び出し
【０１７２】
【数５６】
0005337454.tif 000057
【０１７３】
の列であると仮定する。
【０１７４】
【数５７】
0005337454.tif 000058
【０１７５】
を算出するために、各関数ｆiについて、正規言語
【０１７６】
【数５８】
0005337454.tif 000059
【０１７７】
を、fiにおける入力位置ｅniから、関数の呼び出し位置または共有変数がアクセスされる位置のいずれかである位置fcまで要約する。次に、言語
【０１７８】
【数５９】
0005337454.tif 000060
【０１７９】
は単に連結
【０１８０】
【数６０】
0005337454.tif 000061
【０１８１】
となる。
【０１８２】
【数６１】
0005337454.tif 000062
【０１８３】
ここで、calliはfciに対応するfiにおけるfi+1の呼び出し位置である。
【０１８４】
なお、再帰関数は、これが単にCFGのSCCになるので、特殊な処理は必要としないことに留意されたい。ランデブープリミティブは通常、関数のごく一部分で用いられるので、
【０１８５】
【数６２】
0005337454.tif 000063
【０１８６】
は大半の関数fの大半の位置ｃに空列を含み、したがって上記の手順は計算量が多くはない。たとえ、言語
【０１８７】
【数６３】
0005337454.tif 000064
【０１８８】
が特別なコンテキストで算出されても、本発明の構成は、該言語がなお正規のものでありコンテキストフリーではないことを確保しており、それによって上で説明した非決定性の問題に直面しないことが確保されている。
【０１８９】
パラメータ化（Parameterization）：２つのスレッドT1およびT2からなる並行プログラム
【０１９０】
【数６４】
0005337454.tif 000065
【０１９１】
における対毎の到達可能性を調べる代わりに、本発明では、c1およびc2がTiのniのコピーからなる並行プログラム
【０１９２】
【数６５】
0005337454.tif 000066
【０１９３】
において静的に対毎の到達可能になるように、c1およびc2がパラメータ化された静的に対毎の到達可能であるかどうか、すなわち、n1、n2が存在するかどうかを探索する。一般に、パラメータ化は静的に対毎の到達可能な制御状態群を過大近似する。しかし、驚くことに、静的なパラメータ化された対毎の到達可能性の問題は、スレッドが再帰的な場合でさえ、ロックおよび待ち通知ステートメントを使用して、スレッドの同期について効率的に決定できる。これは、一般に、静的な対毎の到達可能性は、一定数（２さえ）の再帰的なスレッドを持つプログラムに対して決定不可能である。
【０１９４】
まとめると、対毎の到達可能性を決定するために、（ｉ）規則的な過大近似の使用によって再帰を無視するか、または（ｉｉ）再帰を正確に処理するが一定数のスレッド（各々のコピー）を持つという制限を取り除く。両技術は異なる方法で静的な対毎の到達可能な状態群を過大近似するが、同じ目標、すなわち静的な対毎の到達可能性を決定する立証可能で扱いやすい技術を達成する。
【０１９５】
ロックに対する静的な対毎の到達可能性（Static Pairwise Reachability   for Locks）。専らロックを用いて通信するスレッドの静的な対毎の到達可能性に対する必要かつ十分条件は、c1およびc2の静的な対毎の到達可能性が、（本発明の警告生成が既に処理している）c1およびc2に持されたロック群が互いに素であるだけでなく、ロックがciに到達するためにスレッドTiによって取得された順序であることによっても決まることである。ロックに対するこの順序付けは以下に定義する取得履歴の概念を用いて捕えられる。Lock−Set（Ti,ｃ）は、スレッドTiによって制御位置cに保持されたロック群を示すものとする。
【０１９６】
取得履歴（Acquisition History）:xをグローバル構成ｃに至る並行プログラム
【０１９７】
【数６６】
0005337454.tif 000067
【０１９８】
のグローバルな計算とする。次に、スレッドTiと
【０１９９】
【数６７】
0005337454.tif 000068
【０２００】
について、
【０２０１】
【数６８】
0005337454.tif 000069
【０２０２】
は、ｘに沿ったTiによるｌの最後の取得後にTiによって取得された（および恐らく割り当て解除された）ロック群であると定義される。
【０２０３】
Ｌをロック群とすると、各取得履歴AHは、各ロックのどれがロックセットであるかに関連する、すなわちそのロックの取得履歴に関連するマップ
【０２０４】
【数６９】
0005337454.tif 000070
【０２０５】
である。本発明では、
【０２０６】
【数７０】
0005337454.tif 000071
【０２０７】
であるように、ロックｌ1およびｌ2が存在しない場合でかつ存在しない場合に限り、取得履歴AH1およびAH2は一致していると言う。制御状態c1およびc2は、（ｉ）c1およびc2でのロックセットが互いに素で、（ｉｉ）これらのローカルパスに沿った取得履歴が一致するように、c1およびc2にそれぞれ至るスレッドT1およびT2のローカルパスが存在する場合で、かつ存在する場合に限り、静的に対毎の到達可能である。この結果を利用するために、本発明では、AH拡張アクセスイベントを（v,T,L,AH,ａ,ｃ）形式のトピックとして定義する。ここで、（v,T,L,ａ,ｃ）はアクセスイベントであり、AHはcに至るいくつかのパスに沿った取得履歴である。これらの取得履歴は、ロックセットに非常に類似した静的解析によって追跡することができる。取得履歴の一貫性が同時到達可能性に対する必要条件であるので、すべての警告（e1,e2）を廃棄する。ここで、
【０２０８】
【数７１】
0005337454.tif 000072
【０２０９】
であり、AH1とAH2とは一致しない。
【０２１０】
ブロック２０６（図２）において、警告は正常な不変条件を使用しても取り除かれる。図３における警告（ｂ4,a10）を考える。この場合、ｂ4およびa10での送信および待ちの言語を単に算出するだけでは、この警告を除外することはできない。確かに、ローカルな列b1,b2,b3、およびb4と、a1、a6、a7、a8、a9、およびa11は、それぞれスレッドT1およびT2によって同時に実行することができる。これは、待ちステートメントと異なり、通知ステートメントがノンブロッキングであるからである、すなわち通知ステートメントは、それを待つスレッドが存在するかどうかに関係なく実行することができるからである。この警告を偽りとして規定するために、位置b4では、変数page_count＞MAX_COUNTを、一方位置a10では、page_count＜MAX_COUNTを持つことに注意を払う。これらの条件は互いに一致していないので、すなわち同時に保持することはできないので、位置a10およびｂ4が同時に到達可能ではないと推定することができる。
【０２１１】
本発明では、静的に対毎の到達可能でない対の制御状態を識別するための正常な不変条件の算出を可能にする、精度および拡張性を変えるいくつかの技術を提示する。これらの技術は、精度を向上させ、かつ拡張性を下げる順でリストされた、立証可能な定数、範囲解析、八面体不変条件、および多面体不変条件を含んでいる。これらの技術は、所与の警告を取り除くのに計算上最もコストの低い技術を用いるためにリストされた順に適用されるのが好ましい。
【０２１２】
例えば、すべての必要な対のプログラム変数x、yについての
【０２１３】
【数７２】
0005337454.tif 000073
【０２１４】
形式の関係を追跡する八面体解析を行うことによって、上記の警告を偽りと識別することができるであろう。なお、八面体解析は、２つのスレッドの代わりに並行プログラムに対して個々に行われる必要があることに留意されたい。制御状態の初期の対（a1,b1）で開始すると、T1がまずa1を実行するか、またはT2がまずb１を実行するかの２つのいずれかの可能性がある。T2がまずb1を実行する場合、T2は、時間T1がどのような遷移も実行することができなくなるまでは、ｂ4を実行した後まで割り当てを解除しない、ロックpage_limit_mutexを取得する。このようにして、対毎の到達可能なa11およびa4について、まずT1が実行されなければならない。その場合、T1が位置a8に達するまで、T2は実行することができない。次に、対の位置（a8,b1）において、八面体の不変条件page_count_MAX_PAGES<0が条件文a6によって成立することがわかる。ここで、たとえT2がb1を実行しても、b2での条件文が誤りと評価し、T2はif分岐を実行してNに到達することができない。このように、対の位置b4およびa10は静的に対毎の到達可能ではない。
【０２１５】
正常な不変条件を使用した静的な対毎の到達可能性（Static Pairwise Reachability using Sound Invariants）：マルチスレッド化されたプログラムは、プログラマによって維持される単純なデータ不変条件を用いることによって不必要な同期を避ける。図４は、各スレッドが、最小のローカルな配列を見つけて最小値を共有配列に書き込もうとする、２つのスレッドを持つプログラムの単純な例を示している。なお、ローカルな変数「tid」は、レース自由度を確保し、グローバルな配列「minval」にアクセスしている間ロックの必要性を回避するために用いられることに留意されたい。一方、ロックセットに基づいたレース検出ツールは、「minval」の配列要素に対する非保護のアクセスを警告することになる。
【０２１６】
本発明では、定数畳み込みのような正常な解析、区間解析、八面体解析および多面体解析の使用を明示して、位置対
【０２１７】
【数７３】
0005337454.tif 000074
【０２１８】
が同時到達不可能であることを証明する。これはプログラムにおけるレースの可能性を除去する。本発明のツールを、ミューテックおよびセマフォーのような同期プリミティブを用いて、ローカル変数と共有変数との間の複雑な相互作用を含む些細でない状況に自動的に拡張することができる。
【０２１９】
遷移グラフ（Transitions Graphs）。共有変数に関する不変条件は両スレッドの動作によって影響を受けることがあるので、該スレッドの全ての必要なインターリービングを考慮する必要がある。コンテキスト切り替えが発生する必要がある各スレッドにおけるポイントを決定するために、スレッドレベルのコンフリクト解析が実行される。この解析に基づいて、スレッドTiごとにトランザクショングラフGiを抽出することができる。Giの各ノードはTiのコードセグメントを表している。さらに、Giのノード間のエッジは、Ti自身内の制御フローによって誘導されたトランザクションの間のプログラムフローを表している。各トランザクションは、単一の入力ポイントと恐らくは多くの出力ポイントを持っているものとする。そのような各出力ポイントは、（異なるトランザクションの入力に至る）トランザクションの出力エッジに対応している。
【０２２０】
トランザクショングラフは、モデル検査で広範囲に使用されていた半順序低減（POR：partial order reduction）を用いて算出され、唯一の違いは、本発明では、並行プログラムの状態空間の代わりに、２つのスレッドのCFGの積グラフＰにPORを用いていることである。直、Pにおけるノードの数は、多くても２つのスレッド内のソースコードの行数の積であり、したがってPは底から始めるには大きすぎないことに留意されたい。PORの利用によって、大きい原子的なセクションを得ることができ、したがって大きなプログラムに本発明の技術のロバストな拡張性を確保するスレッド全体にわたってコンテキスト切り替えの数を大きく低減する。
【０２２１】
半順序低減（Partial Order Reduction）。PORは、並行計算が共有変数についてのスレッドの動作に関して半順序であるという事実を利用している。したがって、この半順序を実現するインターリービングをすべて探索する代わりに、PORはわずか２、３（理想的にはちょうど１）を探索すれば十分である。インターリービングのこの除去リングは、永続的な群の概念を用いることによって正常、かつ完全に実行される。グローバルな状態の永続的な群は、その状態から探索される必要のある有効な遷移の部分集合を捕える。永続的な群の計算は、所与の並行プログラムを構成するスレッドの制御位置に対するコンフリクト解析の実行に基づいている。
【０２２２】
コンフリクト解析（Conflict analysis）。それぞれスレッドT1およびT2の制御位置c1およびc2は、（ｉ）共有変数shがc1でアクセスされ、c1で始まり、shのあるｘに沿った第１の位置であるような位置ｄ2に至る、Ｔ2のCFO内にパスｘがある場合、または（ｉｉ）その逆の場合、衝突していると言う。もしそうである場合には、第１の場合にT2がｄ1を実行する前にT1がc1を実行し、第２の場合にT1がc1を実行する前にT2がｄ2（およびパスｘ全体）を実行する両方のインターリービングを探索する必要がある。したがって、アクセスされているshに至るtrで始まるパスがあるようなT1のすべての有効な遷移およびT2のすべての遷移trは、永続的な群に含まれる。しかしながら、位置（c1,c2）で始まると、スレッドT2は、c1にT1を残したままshにアクセスする位置ｄ1に到達できないことを静的に推定することができるが、その場合、たとえc1がc1内のshに現在アクセスしていても、T2はc1と並行して始動することができるshにアクセスする位置に到達することはできないことがわかる。したがって、T2のどのような遷移も永続的な群に含まれる必要はない。
【０２２３】
言いかえれば、（c1,d1）が（c1,c2）から静的に対毎の到達可能でないと推定できれば、その場合、c1とc2は衝突していない。上に示したように、同期制約を用いて静的に対毎の到達可能な状態を算出する方法は既に公知である。該方法は、初期遷移グラフを構築するのに使用するコンフリクトの初期集合をもたらす。専ら同期制約を用いて算出されたこのグラフを使用して、正常な不変条件の初期集合を算出できる。しかしながら、正常な不変条件に基づいて、より大きなトランザクション、したがってより小さなトランザクショングラフを順番に生み出す、本発明のコンフリクト解析を改善することを可能にするＣＦＧの到達不可能な部分を取り除くことができることもある。これによってより明確な不変条件が得られる。一定点に達するまで上記の全工程が繰り返される。
【０２２４】
図５を参照すると、トランザクショングラフ３０２が図４で説明したプログラム中のスレッドについて例示的に示されている。ノードｎ0、ｎ1、ｎ2は、正常なデータフロー解析のための原子と考えることができるコードセグメントを表している。１つの目標は、各々がそのトランザクショングラフを実行する多重スレッドのレベルまで静的解析を高めることである。
【０２２５】
積トランザクショングラフGπは、各スレッドTiのトランザクショングラフのデカルト積集合を考えることによって得られる。各ノードはトランザクションのタプルである。さらに、各エッジはスレッドTiによるトランザクションmiの実行を含んでいる。具体的には、エッジは
【０２２６】
【数７４】
0005337454.tif 000075
【０２２７】
の形式であり、ここで、jγiに対して
【０２２８】
【数７５】
0005337454.tif 000076
【０２２９】
そして
【０２３０】
【数７６】
0005337454.tif 000077
【０２３１】
となるようなインデックスi上にある。
【０２３２】
図６を参照すると、積トランザクショングラフ３１０の一部分が、図４からの実行中の例について例示的に示されている（例えば、n3に関するノードは図示していない）。各エッジはスレッドの１つによって実行されているトランザクションに対応している。例えば、エッジ
【０２３３】
【数７７】
0005337454.tif 000078
【０２３４】
はスレッドT2によって実行されているトランザクションn0を示しており、トランザクションn2の開始時に存在するその制御に至る。
【０２３５】
なお、本発明では、２つのスレッドによるトランザクションの同時実行を考慮していないことに留意されたい。コンフリクト解析は、そのような各実行が一連の単一のスレッドの実行によって事実、捕えられることを保証している。
【０２３６】
並行プログラムのフロー解析（Flow Analysis for Concurrent Programs）。本発明では、ｕをスレッドT1、T2を持つ２つのスレッド化されたプログラム
【０２３７】
【数７８】
0005337454.tif 000079
【０２３８】
と見なす。共有変数はＳで示され、各スレッドのローカルな変数がL1、L2で表されている（本発明では、すべての関数に属するすべてのローカルな変数を１つにまとめている）。
【０２３９】
【数７９】
0005337454.tif 000080
【０２４０】
がスレッドT1のトランザクションを示し、
【０２４１】
【数８０】
0005337454.tif 000081
【０２４２】
がスレッドT2のトランザクションを示すものとする。トランザクショングラフはエッジの集合E1、E2を有する。
【０２４３】
多重スレッドについてのフロー解析は、スレッドごとに１つのデータフローファクトのタプルを含んでいる。２つのスレッドのケースについては、事実は
【０２４４】
【数８１】
0005337454.tif 000082
【０２４５】
の形式であり、ここで、
【０２４６】
【数８２】
0005337454.tif 000083
【０２４７】
はスレッドT1についての共有変数およびローカルな変数の値に関連し、
【０２４８】
【数８３】
0005337454.tif 000084
【０２４９】
はスレッドT2の共有変数およびローカルな変数の値に関連する。プログラムは共有変数を介して通信するので、任意の対
【０２５０】
【数８４】
0005337454.tif 000085
【０２５１】
によって記載された共有変数の集合は
【０２５２】
【数８５】
0005337454.tif 000086
【０２５３】
と同じであることが必要である。この一貫性条件は解析全体にわたって維持される。
【０２５４】
プリミティブとして、グローバルな変数およびローカルな変数、およびトランザクションni上でアサーション(assertion)
【０２５５】
【数８６】
0005337454.tif 000087
【０２５６】
が与えられると、上記した抽象解釈技術を用いて、トランザクションniの出力エッジにおける出力アサーション
【０２５７】
【数８７】
0005337454.tif 000088
【０２５８】
を算出する。
【０２５９】
【数８８】
0005337454.tif 000089
【０２６０】
がトランザクションni全体のアサーションφの伝搬の結果を示すものとすると、エッジ
【０２６１】
【数８９】
0005337454.tif 000090
【０２６２】
での
【０２６３】
【数９０】
0005337454.tif 000091
【０２６４】
によって示される出力アサーションを得る。なお、
【０２６５】
【数９１】
0005337454.tif 000092
【０２６６】
を算出している間、第２のスレッドは実行しないと仮定してもよいことに留意されたい。
【０２６７】
融合（Melding）。基本のステップは、トランザクションni全体にわたってアサーション対
【０２６８】
【数９２】
0005337454.tif 000093
【０２６９】
を伝搬する（スレッドT2によるトランザクションの実行は同様に処理される）ことを含んでいる。φkがいくつかの出口ノードnkに対する順方向伝搬
【０２７０】
【数９３】
0005337454.tif 000094
【０２７１】
の結果を示しているものとする。
【０２７２】
なお、そうする際に共有変数Gは変更されてもよいことに留意されたい。したがって、たとえスレッドT2がムーブ（move）の間サイレント（silent）でも、それにもかかわらずそのグローバルな状態はムーブの結果として影響されてもよい。その結果、ψjのグローバル状態を、結果φiのグローバル状態と一致するように変更する必要がある。
【０２７３】
上記の変更をするために、本発明では、ψjによって表されたグローバルな状態値がφkのグローバル状態値と一致させる演算子meld（φk,ψj）を導入する。融合は以下のように定義することができる。φ［S,L1］およびψ［S,L2］をスレッドごとの共有変数およびローカル変数にわたるアサーションとする。アサーションγ：meld（φ,ψ）は以下のようなものである。
【０２７４】
１．γは
【０２７５】
【数９４】
0005337454.tif 000095
【０２７６】
にわたるアサーションである。
【０２７７】
２．
【０２７８】
【数９５】
0005337454.tif 000096
【０２７９】
３．
【０２８０】
【数９６】
0005337454.tif 000097
【０２８１】
４．演算子は入力としては単調でなければならない、すなわち、
【０２８２】
【数９７】
0005337454.tif 000098
【０２８３】
であれば、
【０２８４】
【数９８】
0005337454.tif 000099
【０２８５】
である。
【０２８６】
言いかえれば、新しいアサーションγは、φによって記載されたグローバル変数値と、ψによって記載されたローカル変数値の過大近似である。要約すると、エッジ
【０２８７】
【数９９】
0005337454.tif 000100
【０２８８】
に対するアサーション
【０２８９】
【数１００】
0005337454.tif 000101
【０２９０】
によって記載された初期状態から始まるトランザクション
【０２９１】
【数１０１】
0005337454.tif 000102
【０２９２】
を実行する作用は、アサーション対
【０２９３】
【数１０２】
0005337454.tif 000103
【０２９４】
によって与えられ、ここで、
【０２９５】
【数１０３】
0005337454.tif 000104
【０２９６】
である。
【０２９７】
形式上、伝搬演算子propagateを用いて、エッジ
【０２９８】
【数１０４】
0005337454.tif 000105
【０２９９】
全体にわたってトランザクションniを実行する作用をモデル化する。伝播
【０３００】
【数１０５】
0005337454.tif 000106
【０３０１】
目標は、
【０３０２】
【数１０６】
0005337454.tif 000107
【０３０３】
が共有変数Ｓをローカル変数L1と、同様にψjに関連させるように、プロタクトグラフ（ni,mj）の各ノードを１対のアサーション
【０３０４】
【数１０７】
0005337454.tif 000108
【０３０５】
でラベルを付けるマップηを生成することである。第２に、個々のスレッドの制御がノード
【０３０６】
【数１０８】
0005337454.tif 000109
【０３０７】
内に同時に存在するときはいつも、アサーション
【０３０８】
【数１０９】
0005337454.tif 000110
【０３０９】
の各々が成立する。
【０３１０】
形式上、任意のエッジ
【０３１１】
【数１１０】
0005337454.tif 000111
【０３１２】
について、
【０３１３】
【数１１１】
0005337454.tif 000112
【０３１４】
であることが必要である。
【０３１５】
対称な条件がスレッドT2のムーブについて成立する必要がある。マップηは、post-conditionとしてpropagateを用いて、積グラフＧに対し順方向伝搬を用いることで構築することができる。
【０３１６】
積グラフ順方向伝搬（Product Graph Forward Propagation）。積グラフ上の順方向伝搬は、各ポスト状態（post condition）（伝達関数）がスレッドの１つのトランザクションコードセグメントの本格的な解析であるという例外を除いて、単一のスレッド化されたCFGに対するのと同じ方法を用いる。第２に、順方向伝搬は定義されるべきmeld演算子を用いる。単純な融合演算子は、投射（projection）と、結合（conjunction）
【０３１７】
【数１１２】
0005337454.tif 000113
【０３１８】
が論理結合
【０３１９】
【数１１３】
0005337454.tif 000114
【０３２０】
（すなわち、ムーア（moore）の閉領域）と一致する領域に対する働き（works）を用いて構築することができること示す。形式的に、本発明では
【０３２１】
【数１１４】
0005337454.tif 000115
【０３２２】
である。
【０３２３】
抽象領域が投射と結合を許せば、上記で定義した数式は、最良の考えられる融合演算子をもたらすことを示すことができる。
【０３２４】
同期制約と正常な不変条件とを組み合わせること（Combining Synchronization Constraints and Sound Invariants）。２つの技術を個々に利用することによって達成することができるよりも多くの警告を除外するために、同期制約と正常な不変条件とを相乗的に組み合わせる方法を示している。これも図２のブロック２０６で行われる。
【０３２５】
方法１：
１．１対のスレッドT1およびT2が与えられると、ロックの制約およびランデブーの制約を用いることによって初期遷移グラフT0を構築する。
【０３２６】
２．繰り返し：
３．範囲、八面体、多面体不変条件を算出し、可能であればTiからパスを除去し、Ti+1’になる。
【０３２７】
４．除去された遷移グラフTi’に同期制約を用いて、遷移グラフTiを再計算する。
【０３２８】
５．Ti+1＝Tiまで
６．Tiを返す
一般に、一定点に到達するまで同期制約および正常な不変条件を交互に利用することによって、反復して同期骨組み（skeleton）を改善することができる。方法１は遷移グラフを除去するので、該方法は、コンフリクトの数を低減するだけでなく正常な不変条件を改善することを可能にする。コンフリクトの削減は一方で、大きなトランザクション、すなわちコードの原子的なセクションを同定することを可能にし、それによってコンテキスト切り替えの数を低減することが可能になる。結果として生じる遷移グラフは、警告低減にだけでなく、とりわけポインタエイリアス解析およびモデル検査のようなデータフロー解析を含む並行プログラムの任意の解析にも使用することができる。その意味において、本技術ははるかに広い利用可能性を持っている。
【０３２９】
ブロック２０８で、具体的なエラートレースが、例えばモデルチェッカーによって生成される。該モデルチェッカーはモデル検査および静的解析を用いることを含んでいるのが好ましい。このステップでは、モデル検査を利用して、ブロック２０４での除去リング後に残された警告の具体的なエラートレースを生成する。該モデル検査は状態急増の問題があり、本発明はこの問題を、（ｉ）各スレッドを、警告を特定するコンテキストにおいてのみ探索すること、（ｉｉ）記号技術の能力を用いて大きな状態空間を探索すること、（ｉｉｉ）半順序削減と、（ｉｖ）探索される必要のあるインターリービング群を削減する同期制約および正常な不変条件から算出された遷移グラフを利用すること、によって、改善しようとするものである。本発明は、まずスレッドごとに回路を構築することによって所与の並行プログラムの回路ベースのモデルを構築し、次にスケジューラによって該モデルを１つに構成することから始める。
【０３３０】
個々のスレッドを複数の回路に変えること(Translating Individual Threads into Circuits)。各スレッドの回路は限界データと限界制御（再帰）の仮定のもとで得られる。本発明は、配列およびstructsをすべてフラットにし、それらを単純なスカラ変数の集合に置き換え、各スカラ変数にそのメモリアドレスを表す固有の番号を割り当てることによってプログラムの内部メモリ表現を構築することから始める。プログラムメモリにおいて互いに隣接する変数が、本発明のモデルにおける連続するメモリアドレスに与えられ、これはポインタ演算のモデル化を容易にする。本発明は、ヒープ(heap)を有限の配列としてモデル化し、ポインタを該配列に戻すmalloc()の単純な実現を付加している。
【０３３１】
該単純化されたプログラムは単純なタイプ（Booleanの列挙整数）のスカラ変数を含んでいる。該単純化されたプログラムのCFGは状態ベクトル（pc,V）を持つ有限状態マシンとして見ることができ、ここで、pcは基本ブロックの符号化を示し、Vは整数値のプログラム変数のベクトルである。次に、pcおよびプログラムに現われる各データ変数に対する記号遷移関係を構築する。Pcの場合、遷移関係はCFG内の制御位置間の保護された遷移を反映している。データ変数の場合、遷移関係は種々のスレッド位置の変数に割り当てられた式から構築される。最後に、ハードウェア回路に似ているこれら遷移関係の記号表現を構築する。pc変数の場合、
【０３３２】
【数１１５】
0005337454.tif 000116
【０３３３】
個のラッチが割り当てられ、ここでNは基本ブロックの総数である。各プログラム変数については、ｎ個のラッチのベクトルが割り当てられ、ここでｎは変数のビット幅である。最後に、スレッドのスレッドごとの回路ベースのモデルが得られ、ここで、各変数は２進値のラッチのベクトル、およびラッチごとのBooleanのnext-stale関数（または関係）で表される。
【０３３４】
警告特定のモデル化(Warning Specific Modelling)。各警告がコンテキストを特定するので、このコンテキスト内の関数をすべてインライン化し、残りのスレッドをスライスして取り除く。このようにして、本発明では、ブロック２１０での除去リング後に残る警告コンテキストによって特定されたプログラムの一部分だけを探索する。インライン化することは、プログラムスライシング、範囲解析、定数伝搬等のモデル縮小に使用するすべての静的解析の効果を著しく改善する。しかしながら、特別なコンテキストにおいてスレッドを探索する最大の効果はメモリのモデル化時に発生する。
【０３３５】
一般に、ポインタアクセスを処理する場合、まずSteensgaardのポイントへの解析を行ってポインタ変数が指すことができる変数群を決定する。次に、ポインタまたは配列参照によって、各間接メモリアクセスを直接メモリアクセスに変換する。例えば、ポインタpが所与のプログラム位置での変数a, b,…,zを指すことができると判断すれば、ポインタを、形式
【０３３６】
【数１１６】
0005337454.tif 000117
【０３３７】
の条件式として
【０３３８】
【数１１７】
0005337454.tif 000118
【０３３９】
に書き換える。ここで、&a、&b,．．．はそれぞれ変数a,ｂに割り当てられた数値メモリアドレスである。
【０３４０】
間接割り当て(An indirect assignment)
【０３４１】
【数１１８】
0005337454.tif 000119
【０３４２】
は、一連の条件付き割り当て
【０３４３】
【数１１９】
0005337454.tif 000120
【０３４４】
に置き換えることができる。これらの割り当てのちょうど１つは実行中に効果がある。なお、割り当ての数はポイントツー群(points-to set)a,b,、．．．,ｚの濃度に等しいので、ポイントツー群の大きさ、または間接的にポイントツー解析の精度は、結果として生じる回路モデルの大きさに直接影響を与えることに留意されたい。警告特定のコンテキストにおける関数をインライン化するので、ブートストラッピングを用いて、Steensgaardのポイントツー群よりはるかに小さいそのコンテキストにおけるフローおよびコンテキスト依存のポイントツー群を算出できる。これは、特定のコンテキストのモデル検査がさらに拡張可能な理由の１つである。
【０３４５】
並行プログラム用の回路を構築すること(Building the Circuit for the Concurrent Program)。各スレッドTiに対する回路Ciが与えられたとして、これらのスレッドからなる並行プログラムCP用の回路Cを得る方法についてここに示す。同じ識別名を持つローカル変数が多重スレッドにおいて生じる場合、一貫性を確保するために、スレッドTiの各ローカル変数の識別名の前にthread_iを付ける。次に、各スレッドTiについて、PがCPの次のステップにおいて実行するようにスケジュールされているかどうかを示す、ゲートexecute_iを導入する。
【０３４６】
各ラッチｌについては、
【０３４７】
【数１２０】
0005337454.tif 000121
【０３４８】
が回路Ｃiにおける次の状態関数ｌを示すものとする。次に、回路Cにおいて、スレッドTiのローカル変数に対応するラッチthread_i_1の次の状態値は、execute_iが真であれば
【０３４９】
【数１２１】
0005337454.tif 000122
【０３５０】
と定義され、そうでなければthread_i_1の現在値と定義される。一方、ラッチｌは共有変数に対応しており、next-state（1）は
【０３５１】
【数１２２】
0005337454.tif 000123
【０３５２】
と定義され、ここでexecute_iは真である。なお、本発明では、execute_iがちょうど１つのスレッドTiに対して真であることを確実にする必要があることに留意されたい。そのために、本発明は、実行された信号のいずれの１つがtrueに設定されるかをCPの各グローバル状態において決定し、それによってスレッド構成のセマンティックスを決定するスケジューラを実現する。
【０３５３】
条件付きの扱いにくい群ベースの永続的な群(Conditional Stubborn Sets based Persistent Sets)。半順序低減を組み込むためには、各グローバル状態ｓから、ｓの条件付きの扱いにくい群に属する遷移のみが探索されることを確保する必要がある。RとRiがそれぞれCP、Tiの遷移関係をそれぞれ表しているものとする。CPがｎ個のスレッドを有するものとすれば、各グローバル状態ｓについて条件付きの扱いにくい群を識別するｎビットのベクトルcstubiを導入する。すなわち、ｓにおいて、イネーブルされたTiの（固有の）遷移が、ｓの同じ最小の条件付きの扱いにくい群に属するように、cstubiは、ｓにおいて正にそれらのスレッドTiに対してtrueである。したがって、
【０３５４】
【数１２３】
0005337454.tif 000124
【０３５５】
である。
【０３５６】
本発明は、静的解析とモデル検査とを組み合わせて、データレースに対する具体的なエラートレースを生成する有効な方策を提示した。これらの静的解析は、定数伝搬、範囲解析、八面体解析、および多面体解析のようなデータフロー解析によって算出された正常な不変条件だけでなく、ロック、ランデブー等の同期プリミティブの使用から発生するインターリービング制約も利用する。本技術は、偽の警告低減だけでなく一般の並行プログラムの解析にも適用可能である。
【０３５７】
並行バグのエラートレースを生成するシステムおよび方法の好ましい実施形態（例示として意図したものであり、限定するものではない）を説明したが、変更および変形が当業者によって、上記の教示に照らして行うことができることに留意されたい。したがって、添付の請求項によって略述されるような本発明の範囲と要旨を逸脱することなく、開示された特定の実施形態において、変更がなされてもよいことが理解されるべきであろう。このように、特許法によって要求された詳細さで本発明の態様を説明したが、特許証によって保護された要求および所望のものは、添付の請求項に記載されている。
【図面の簡単な説明】
【０３５８】
【図１】図１はコンピュータ検証のために具体的なエラートレースを生成する例示的システム／方法を示すブロック／流れ図である。
【図２】図２はコンピュータ検証のために具体的なエラートレースを生成する他の例示的システム／方法を示すブロック／流れ図である。
【図３】図３は本発明の原理にしたがって除去リング警告を示すプログラム例の図である。
【図４】図４はレースがないマルチスレッドプログラムを示す例である。
【図５】図５は図４に示したプログラムのスレッドの遷移グラフである。
【図６】図６はｎ3のペアが示されていない、図４に示したプログラムの２つのスレッドのプロダクトコントロール／遷移グラフの一部である。
【符号の説明】
【０３５９】
１０２、１０４、１０６、１０８〜１１０  ステップ
２０２  警告発生器
２０４  警告フィルター
２０８  モデル検査器/具体的なエラートレース発生器
【図１】
0005337454.tif 000125
【図２】
0005337454.tif 000126
【図３】
0005337454.tif 000127
【図４】
0005337454.tif 000128
【図５】
0005337454.tif 000129
【図６】
0005337454.tif 000130