(57)【要約】【課題】データ構造に対し並列に実行される複数の動作を含む、実行履歴の正しさを検証するためのコンピュータ実装方法、システム及びコンピュータ・プログラムを提供する。【解決手段】マルチコア・プロセッサが汎用マシンの標準アーキテクチャになったので、プログラマは、並列性について最適化されたソフトウェアを書くことが必要とされる。正しさの検証は、並列コードについては、その複雑さのために重要な問題である。しかし、複雑なコードの検証（例えば、コードの実行のテスト）を提供するためのツールは、依然として見当たらない。従って、本明細書では、プログラム・トレースの正しさを評価するためのシステム及び方法を開示する。さらに、本明細書に開示したシステム及び方法は、評価中のプログラム・トレースのサイズが増大しても、過度の計算要件を必要としない。【選択図】  図５
2010186476.tif 000002
【特許請求の範囲】
【請求項１】
データ構造に対し並列に実行される複数の動作を含む、実行履歴の正しさを検証するためのコンピュータ実装方法であって、
（ａ）前記データ構造上の動作挙動を定義する動作ルール・セット、新しい状態ルール・セット及び古い状態ルール・セットを含む、ルール・セットを定義するステップと、
（ｂ）前記実行履歴をストレージ装置から読み取るステップと、
（ｃ）前記実行履歴内に含まれる動作ごとに、開始イベント及び終了イベントを含む、イベント・セットを構築するステップとを有し、
各イベントが、各動作の開始時間及び終了時間に従ったタイムスタンプを含み、
（ｄ）各イベントの前記タイムスタンプに従って、前記イベント・セット内の各イベントを順次に処理するステップと、
（ｅ）前記処理するステップ（ｄ）に応答して、状態セットを構築するステップとをさらに有し、
イベントを処理する際に、前記新しい状態ルール・セット内に含まれる新しい状態ルールに従って新しい状態を作成するときは、新しい状態が前記状態セットに追加され、イベントを処理する際に、前記古い状態ルール・セット内に含まれる古い状態ルールに従って古い状態を除去するときは、前記状態セット内の古い状態が除去され、
（ｆ）前記状態セットが空であるときは、正しくない結果をストレージ装置又はディスプレイ装置に出力するステップと、
（ｇ）全てのイベントが処理され且つ前記状態セットが少なくとも１つの状態を含むときは、正しい結果をストレージ装置又はディスプレイ装置に出力するステップとをさらに有する、コンピュータ実装方法。
【請求項２】
前記データ構造が、並行式優先キューであり、前記ルール・セットが、挿入動作及び除去動作を含む、請求項１に記載のコンピュータ実装方法。
【請求項３】
データ・セットを含む確定ヒープを定義するステップをさらに有し、前記並行式優先キューが、前記状態セット内の全ての状態にわたる前記データ・セットを含む、請求項２に記載のコンピュータ実装方法。
【請求項４】
前記古い状態ルール・セット内で古い状態ルールが定義され、当該古い状態ルールが、終了イベントを処理する際に当該終了イベントを未処理として記述する状態を除去する、請求項２に記載のコンピュータ実装方法。
【請求項５】
前記新しい状態ルール・セット内で新しい状態ルールが定義され、当該新しい状態ルールが、前記並行式優先キュー内の最大優先値よりも小さい値が前記挿入動作に従って前記並行式優先キューに追加されるときに新しい状態を作成する、請求項２に記載のコンピュータ実装方法。
【請求項６】
前記処理するステップ（ｄ）が、新しいイベントを処理するときにイベントを各状態に追加するステップをさらに有する、請求項１に記載のコンピュータ実装方法。
【請求項７】
前記状態セット内の状態ごとに  前記イベントに対応する動作が開始イベントを処理する際に完了しているか否かを決定するステップをさらに有する、請求項６に記載のコンピュータ実装方法。
【請求項８】
前記状態セット内の少なくとも１つの状態が未処理の動作を有するときは、各動作を完了させるために、各状態内の未処理の動作を適用するステップをさらに有する、請求項７に記載のコンピュータ実装方法。
【請求項９】
コンピュータ上でデータ構造に対し並列に実行される複数の動作を含む、実行履歴の正しさを検証するためのシステムであって、
（ａ）前記データ構造上の動作挙動を定義する動作ルール・セット、新しい状態ルール・セット及び古い状態ルール・セットを含む、ルール・セットを定義するための手段と、
（ｂ）前記実行履歴をストレージ装置から読み取るための手段と、
（ｃ）前記実行履歴内に含まれる動作ごとに、開始イベント及び終了イベントを含む、イベント・セットを構築するための手段とを有し、
各イベントが、各動作の開始時間及び終了時間に従ったタイムスタンプを含み、
（ｄ）各イベントの前記タイムスタンプに従って、前記イベント・セット内の各イベントを順次に処理するための手段と、
（ｅ）前記処理するための手段（ｄ）に応答して、状態セットを構築するための手段とをさらに有し、
イベントを処理する際に、前記新しい状態ルール・セット内に含まれる新しい状態ルールに従って新しい状態を作成するときは、新しい状態が前記状態セットに追加され、イベントを処理する際に、前記古い状態ルール・セット内に含まれる古い状態ルールに従って古い状態を除去するときは、前記状態セット内の古い状態が除去され、
（ｆ）前記状態セットが空であるときは、否定的な結果をストレージ装置又はディスプレイ装置に出力するための手段と、
（ｇ）全てのイベントが処理され且つ前記状態セットが少なくとも１つの状態を含むときは、肯定的な結果をストレージ装置又はディスプレイ装置に出力するための手段とをさらに有する、システム。
【請求項１０】
前記データ構造が、並行式優先キューであり、前記ルール・セットが、挿入動作及び除去動作を含む、請求項９に記載のシステム
【請求項１１】
データ・セットを含む確定ヒープを定義するための手段をさらに有し、前記並行式優先キューが、前記状態セット内の全ての状態にわたる前記データ・セットを含む、請求項１０に記載のシステム。
【請求項１２】
前記古い状態ルール・セット内で古い状態ルールが定義され、当該古い状態ルールが、終了イベントを処理する際に当該終了イベントを未処理として記述する状態を除去する、請求項１０に記載のシステム。
【請求項１３】
前記新しい状態ルール・セット内で新しい状態ルールが定義され、当該新しい状態ルールが、前記並行式優先キュー内の最大優先値よりも小さい値が前記挿入動作に従って前記並行式優先キューに追加されるときに新しい状態を作成する、請求項１０に記載のシステム。
【請求項１４】
前記処理するための手段（ｄ）が、新しいイベントを処理するときにイベントを各状態に追加するための手段をさらに有する、請求項９に記載のシステム。
【請求項１５】
前記状態セット内の状態ごとに  前記イベントに対応する動作が開始イベントを処理する際に完了しているか否かを決定するための手段をさらに有する、請求項１４に記載のシステム
【請求項１６】
状態セット内の少なくとも１つの状態が未処理の動作を有するときは、各動作を完了させるために、各状態内の未処理の動作を適用するための手段をさらに有する、請求項１５に記載のシステム。
【請求項１７】
請求項１ないし請求項８の何れか１項に記載の方法の各ステップをコンピュータに実行させるためのコンピュータ・プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、データ構造に対し並列に実行される複数の動作を含む、実行履歴の正しさを検証することに係る。
【背景技術】
【０００２】
新しいマルチコア・プロセッサ・アーキテクチャによって導入されて、現在のコンピュータ・ハードウェアにおける複数の処理ユニットが使用可能になったことにより、従来のアルゴリズム及びデータ構造を使用するプログラムによっては利用することができない、計算能力が提供されている。以前の単一プロセッサ・アーキテクチャでは、任意の所与の時間において１つのスレッドしかを実行することができなかった。従って、２つのスレッドが同一のデータ構造上で同時に動作するのを防止することにより、このデータ構造内のデータの破損を回避することは、比較的簡単であったし、性能に及ぼす影響も最小限に留まっていた。
【０００３】
しかし、マルチコア・プロセッサを使用する場合には、複数のスレッドは、異なる処理ユニット（又は「コア」）上で並行的に走るように、コンピュータ実行可能コード（又は単に「コード」）によってプログラムすることができる。データ構造上のそれらの並行処理を防止することは、データの破損を回避するための効率的な方法ではない。なぜなら、高々１つのスレッドだけが走るのであれば、資源（すなわち、マルチコア・プロセッサ内のコア）が浪費されるからである。当分野では、複数のスレッドがデータ構造を並行的にアクセスすることを可能にするための新しいアルゴリズムが必要とされている。このことは、データ構造を実装するコードを書き直すことを意味する。この新しいコードは、正しさについて検証することがより困難である。なぜなら、この新しいコードは、単一の実行パスの代わりに、複数の並行実行パスを考慮するために、その複雑度が本質的により大きくなっているからである。
【０００４】
並列アルゴリズムの正しさを検証するための幾つかの検証ツールが存在するが、そのどれもが、データ構造の非常に簡単な特性を検証するか、又は簡単な特性を有するデータ構造を検証するに過ぎない（例えば、Vafeiadis, Shape-value Abstraction for Verifying Linearizability,VMCIA 2009 及び Fraser, Practical lock-freedom, Technical Report, University ofCambridge, 2004 を参照）。従って、書かれたコードの正しさを開発者が評価するのを助け且つ生産性を向上させるとともに、データ構造自体の品質及び信頼性を改良するためには、正しさの検証ツールのような自動化ツールが必要とされている。
【先行技術文献】
【非特許文献】
【０００５】
【非特許文献１】Vafeiadis, Shape-value Abstraction for Verifying Linearizability,VMCIA 2009
【非特許文献２】Fraser, Practical lock-freedom, Technical Report, University ofCambridge, 2004
【非特許文献３】Herlihy, et al. “Linearizability: A Correctness Condition for Concurrent Objects”, ACM Transactionson Programming Languages and Systems, 12(3):463-492 (1990)
【非特許文献４】Zakhour et al., The Java Tutorial: A Short Course on theBasics, 4th Edition (2006)
【発明の概要】
【発明が解決しようとする課題】
【０００６】
さらに、並列アルゴリズムの正しさの検証は、これまで計算集中的な複雑な動作として見なされてきた。従って、アルゴリズムの実行に関する分析を行うことは、たとえあったとしても、制限されていた。例えば、データ構造を使用して実行することができる全ての可能な原子(atomic)動作（すなわち、他の幾つかの可視的な小動作に分割できない動作）が与えられると、ソフトウェア・テスト・プログラムは、複数の並行スレッドを使用して、これらの動作を反復的に且つ特定のランダム順序で実行することになる。このテスト・プログラムの出力は、実行された全ての原子動作及びそれらの結果の履歴である。一般に、テスト・プログラムのより長い履歴は、動作のより豊富な組み合わせ（例えば、より多数のオーバーラップ動作）を含み、従って検証ツールの正確性を改良する。しかし、従来の検証方法を使用する場合は、より長い履歴がより大きな計算要件を必要とすることを暗示する。従って、計算要件が履歴の長さに応じて過度に増大しないという、効率的な検証ツールが必要とされている。
【課題を解決するための手段】
【０００７】
データ構造は、異なる基準に従って、「正しい」と定義することができる。本発明の非制限的な側面では、本発明の実施形態（以下「実施形態」と表記）は、正しさについて広範に受け入れられている１つの基準を利用する。この基準は、「直線化可能性（linearizability）」と呼ばれ、Herlihy, et al. “Linearizability: A Correctness Condition for Concurrent Objects”, ACM Transactionson Programming Languages and Systems, 12(3):463-492 (1990) において定義されている。「直線化可能性」特性は、複数の順次アルゴリズムが並列に実行される場合に、これらの順次アルゴリズムが正しく実行されることを検証するための理論モデルである。
【０００８】
以下で詳述する実施形態では、順次アルゴリズムを実装し且つデータ構造を使用するテスト・プログラムによって生成された実行履歴の「直線化可能性」特性を検証するための方法及びシステムを説明する。さらに、実施形態は、生成された履歴結果を１回だけ探索することによって、バックトラック探索を回避する。従って、実施形態に関連する計算要件は、出力履歴の長さが増大しても、過度に増大しないのである。
【０００９】
従って、本発明の１つの側面は、データ構造に対し並列に実行される複数の動作を含む、実行履歴の正しさを検証するためのコンピュータ実装方法を提供する。この方法は、
（ａ）前記データ構造上の動作挙動を定義する動作ルール・セット、新しい状態ルール・セット及び古い状態ルール・セットを含む、ルール・セットを定義するステップと、
（ｂ）前記実行履歴をストレージ装置から読み取るステップと、
（ｃ）前記実行履歴内に含まれる動作ごとに、開始イベント及び終了イベントを含む、イベント・セットを構築するステップとを有し、
各イベントが、各動作の開始時間及び終了時間に従ったタイムスタンプを含み、
（ｄ）各イベントの前記タイムスタンプに従って、前記イベント・セット内の各イベントを順次に処理するステップと、
（ｅ）前記処理するステップ（ｄ）に応答して、状態セットを構築するステップとをさらに有し、
イベントを処理する際に、前記新しい状態ルール・セット内に含まれる新しい状態ルールに従って新しい状態を作成するときは、新しい状態が前記状態セットに追加され、イベントを処理する際に、前記古い状態ルール・セット内に含まれる古い状態ルールに従って古い状態を除去するときは、前記状態セット内の古い状態が除去され、
（ｆ）前記状態セットが空であるときは、正しくない結果をストレージ装置又はディスプレイ装置に出力するステップと、
（ｇ）全てのイベントが処理され且つ前記状態セットが少なくとも１つの状態を含むときは、正しい結果をストレージ装置又はディスプレイ装置に出力するステップとをさらに有する。
【００１０】
本発明の他の側面は、コンピュータ上でデータ構造に対し並列に実行される複数の動作を含む、実行履歴の正しさを検証するためのシステムを提供する。このシステムは、
（ａ）前記データ構造上の動作挙動を定義する動作ルール・セット、新しい状態ルール・セット及び古い状態ルール・セットを含む、ルール・セットを定義するための手段と、
（ｂ）前記実行履歴をストレージ装置から読み取るための手段と、
（ｃ）前記実行履歴内に含まれる動作ごとに、開始イベント及び終了イベントを含む、イベント・セットを構築するための手段とを有し、
各イベントが、各動作の開始時間及び終了時間に従ったタイムスタンプを含み、
（ｄ）各イベントの前記タイムスタンプに従って、前記イベント・セット内の各イベントを順次に処理するための手段と、
（ｅ）前記処理するための手段（ｄ）に応答して、状態セットを構築するための手段とをさらに有し、
イベントを処理する際に、前記新しい状態ルール・セット内に含まれる新しい状態ルールに従って新しい状態を作成するときは、新しい状態が前記状態セットに追加され、イベントを処理する際に、前記古い状態ルール・セット内に含まれる古い状態ルールに従って古い状態を除去するときは、前記状態セット内の古い状態が除去され、
（ｆ）前記状態セットが空であるときは、否定的な結果をストレージ装置又はディスプレイ装置に出力するための手段と、
（ｇ）全てのイベントが処理され且つ前記状態セットが少なくとも１つの状態を含むときは、肯定的な結果をストレージ装置又はディスプレイ装置に出力するための手段とをさらに有する。
【００１１】
本発明のさらに他の側面は、前記コンピュータ実装方法の各ステップをコンピュータに実行させるためのコンピュータ・プログラムを提供する。
【発明の効果】
【００１２】
本発明は、出力履歴の長さが増大しても、検証ツールの計算要件が過度に増大しないという効果を奏する。
【図面の簡単な説明】
【００１３】
【図１】実施形態に従った、出力履歴を示すテーブルである。
【図２】実施形態に従った、イベントのリストを示すテーブルである。
【図３】正しい動作シーケンスを示すインターバル図である。
【図４】正しくない動作シーケンスを示すインターバル図である。
【図５】実施形態に従った、状態の管理のためのプロセスを示すフローチャートである。
【図６】実施形態に従った、状態定義を示すテーブルである。
【図７】実施形態に従った、状態セットへの挿入開始イベントの追加を示す図である。
【図８】他の実施形態に従った、状態セットへの挿入開始イベントの追加を示す図である。
【図９】実施形態に従った、状態セットへの挿入終了イベントの追加を示す図である。
【図１０】実施形態に従った、状態セットへの除去開始イベントの追加を示す図である。
【図１１】実施形態に従った、状態セットへの除去終了イベントの追加を示す図である。
【図１２】実施形態に従った、図３のサンプル・データを処理するときに状態セットにもたらされる変更を示す図である。
【図１３】実施形態に従った、図４のサンプル・データを処理するときに状態セットにもたらされる変更を示す図である。
【図１４】実施形態に従った、コンピュータ・システムの構成を示すブロック図である。
【発明を実施するための形態】
【００１４】
以下の説明を簡潔化するため、各実施形態は、データ構造である並行式優先キュー（concurrent priority queue）を検証する検証ツールの実装を仮定する。データ構造である並行式優先キューの１つの定義に従えば、最大優先順位の要素だけがこのキューから除去される。かかるデータ構造の使用例は、次に処理すべきタスクを決定するためのスケジューリング・アルゴリズムを含むことがある。しかし、並行式優先キューに関する以下の説明は、本発明の制限事項として解釈されることを意図していない。当業者には明らかなように、他のデータ構造を使用して、他の実施形態を構築することができるからである。
【００１５】
実施形態では、テスト・ラン(test run)中に実行された全ての原子動作のための正しいシーケンシャル順序が識別される。この場合、このテスト・ランは、実行された全ての原子動作の実行トレース（又は「出力履歴」）を生成する。これらの動作はマルチコア・プロセッサ上で実行され、そしてこの出力履歴はこれらの動作のシーケンシャル・リストであるから、この出力履歴を処理するとき、データ構造への並行アクセスは曖昧である。従って、実施形態では、マルチコア・プロセッサ上でテスト・ランを実行する場合の可能な効果をモデル化するために、並行性ルールが定義される。例えば、一方の動作が他方の動作の前に厳密に生じたならば、すなわち他方の動作が開始する前に一方の動作が終了したのであれば、実施形態は、この順序を変更しない。さらに、一方及び他方の動作が並行に生じたならば、すなわち他方の動作が開始した後であって且つ他方の動作が終了する前に、一方の動作が開始したのであれば、任意の順序を仮定することができる。なぜなら、この動作の効果が生じた時間は、曖昧であるからである。従って、本発明は、データ構造の動作に固有の１セットのルールによって定義されるようなデータ構造の特性に適合する、全ての動作のための順序付け（ordering）を検出する。かかる動作シーケンスが検出不能であることは、非特許文献３の著者である Herlihy 等によって定義されるように、データ構造が「直線化可能（linearazible）」でないことを指示する。
【００１６】
出力履歴内に指示される動作の異なる組み合わせを分析するために、実施形態は、実行された動作の有効な全ての順序付けのための全ての可能な状態を記述する、１セットの状態（又は「状態セット」）を管理する。さらに、１つの動作が開始するとすぐに、実施形態は、予め定義された条件が満たされたか否かに依存して、１セットの状態を拡張する。例えば、テスト履歴が、この動作が効果を生ずべき次の動作であるか否かに関して曖昧であるとき、追加の状態が作成される。従って、これらの新しい状態は、動作の異なる可能な実行順序付けを記述する。さらに、この動作が効果を生ずるのであれば、生成された効果は、（以下で詳述するように）他の並行動作の効果時間に影響を及ぼすことがあり、そしてそれは、再び有効な可能性の数を拡張する。全ての可能性を検出するために、実施形態は、イベントの再帰的分析を行うことができる。
【００１７】
実施形態に従って、１つの動作が終了するとき、状態が状態セットから除去される。例えば、この動作が効果を生じなかった全ての状態が、状態セットから除去される。なぜなら、これらの状態は、当該状態について有効な実行時間が検出されなかったならば、正しいはずがないからである。従って、この検証プロセスの終わりにおいて依然として幾つかの有効な状態が存在すれば、テスト・ランによって生成された履歴は、正しい（すなわち、「直線化可能」である）ものとして検証される。代替的に、この検証プロセス中の特定の時点において状態セットが空であれば、テスト・ランの出力履歴の正しいシーケンシャル順序が検出されなかったのであり、従って、この出力履歴は「直線化可能」ではない。
【００１８】
マルチコア・プロセッサによって実行される動作の効果を正しく定義するために、実施形態は、動作ごとにイベントを定義する。１つの動作の開始は、１つのイベントである。１つの動作の終了は、他のイベントである。従って、テスト・ラン中に５個の異なる動作があれば、実施形態に従って、１０個の異なるイベント（すなわち、動作ごとに１つの開始イベント及び１つの終了イベント）が作成されるであろう。さらに、各イベントは、仮想時間内の一意的な時点において起こる（仮想時間とは、仮想時間ゼロで開始し且つ厳密に単調に増加する数値である）。
【００１９】
前述のように、図面及び以下の記述は、データ構造である並行式優先キューのための出力履歴を検証するために適用された、実施形態を説明するものである。以下の記述を簡潔化し且つ本発明の制限事項を意味するものではないことを明確にするため、優先キューは、各除去動作が最大優先順位を有する要素を除去するときに、「正しい」と見なされる。以下の記述をさらに簡潔化するため、実施形態は、最大優先キューを記述する。最大優先キューでは、この優先キュー内に格納された最高値が、このキューから除去される。さらに、以下の記述は、最大優先キューが並行式最大優先キューであると仮定する。すなわち、このキューは、そのデータへの複数のアクセスが並列に（並行して）行われることを許容する。
【００２０】
並行式最大優先キューのテスト・ラン中に、「挿入」及び「除去」動作がランダムに実行され、そしてこれらの動作が出力履歴内に格納される。並行動作をシミュレートするため、実施形態は、各動作の開始時間及び終了時間を指示するように、各動作に一意的なタイムスタンプを割り当てる。この文脈において、各動作の開始時間は、実際の動作が実行を開始する前の時間として定義され、各動作の終了時間は、この動作の成功裏の実行の後の時間として定義される。従って、開始及び終了タイムスタンプを用いて各動作を定義することにより、この動作は、この範囲内で効果を生ずることが保証される。しかし、各動作がこの範囲内でいつ効果を生じるかということに関しては、如何なる仮定もなされない。さらに、各タイムスタンプは、以下の２つの条件を満たさなければならない。
＜第１の条件＞：各タイムスタンプは、一意的でなければならない。
＜第２の条件＞：タイムスタンプは、厳密に単調に増加しなければならない。
従って、実施形態によれば、各イベントは、そのタイムスタンプが他のイベントのタイムスタンプよりも小さい場合にのみ、他のイベントの前に起こると見なされる。さらに、各動作は、その開始時間又はその終了時間の何れかによって、識別することができる。
【００２１】
図１は、４つの動作を有する出力履歴ファイル（又は単に「ログ」ファイル）を例示する。図示のように、各動作は、そのタイプ（例えば、「除去」又は「挿入」）と、そのタイムスタンプ（例えば、開始及び終了時間）と、除去又は挿入される値によって記述される。以下の記述の便宜上、「ログ・エントリＩＤ」は、各動作を全体として記述するために使用される。従って、図１では、リストされた動作ごとに、特定の１つの出力履歴エントリが存在し、そしてこのエントリは、マルチコア・プロセッサによって実行されている動作に関連するパラメータによって一意的に識別することができる。
【００２２】
図２に示すように、実施形態は、図１のログ・エントリからイベントの分類済みリストを構築する。従って、図１のログ内にリストされた各原子動作は、１つの開始イベント及び１つの終了イベントに拡張される。この場合、各イベントのためのタイムスタンプは、図１のそれぞれの列（すなわち、開始時間及び終了時間）から導出される。図２のイベント・リストが構築された後、実施形態は、図２のイベント・リストを探索し且つ各イベントを以下で詳述するように処理するために、このイベント・リストを含むコンピュータ・コードを実装する。従って、実施形態によれば、このイベント・リストは、１回だけ探索され、バックトラック探索を必要としない。バックトラック探索なしで、このイベント・リストを探索すると、効率を向上させることができるばかりか、より短い出力履歴の正しさを検証するための計算要件を著しく超過することなく、長い出力履歴（例えば、数千又は数百万の動作）の正しさを検証することができる。
【００２３】
図３は、図２の最初の数個のイベントのための可能な実行シーケンスを表すインターバル表現である。図３には、時間軸３００及び一連の動作（すなわち、Ｒ０（ｎｕｌｌ）３１０及びＲ３（４）３４０）が示されており、その各動作は時間範囲を有する。さらに、これらの動作は、マルチコア・プロセッサ上で実行されており、順次に実行されるとは仮定されていないから、１つの動作のための時間軸３００上の時間インターバル内の任意の時点において、この動作の効果を生ずることが可能である。従って、１つの動作を実行することができ、そして依然として「直線化可能性」特性に適合するときは、この動作のために定義されたインターバル中に、時間軸３００上に有効な時点があれば、実行シーケンス（例えば、図３の履歴）は、正しい。時間軸３００上の時間０において、最大優先キュー（図示せず）は、空である。従って、Ｒ０（null）３１０動作（すなわち、ＩＤ「０」の「除去」動作）は、この動作が時間０において開始するときは、他の動作に影響することなく、ヌル値を除去することができる。しかし、この時点において、次の  Ｒ３（４）３４０動作（すなわち、ＩＤ「３」の「除去」動作）の正しさは、不確実であることに留意されたい。なぜなら、Ｒ３（４）３４０は、時間軸３００上で２つの「挿入」動作（すなわち、Ｉ１（４）３２０動作及びＩ２（５）３３０動作）とインターリーブしているからである。前述のように、複数のデータ動作がマルチコア・プロセッサ上で並列に実行されるときの固有の曖昧性と、図３に示されるＩ１（４）３２０動作とＲ３（４）３４０動作との間のオーバーラップに起因して、Ｒ３（４）３４０動作が優先キューから「４」要素を除去する時間には、両方の「挿入」動作又は一方の「挿入」動作が効果を生じているか、或いは何れの「挿入」動作も効果を生じていないことがあり得る。従って、図３では、Ｒ３（４）３４０の正しさは、不確実である。この曖昧性の解消については、図３のサンプル・データに対する実施形態の適用に関連して、以下で説明する。
【００２４】
図４は、インターバル表現の他の例であって、正しくないイベント・リストを例示する。すなわち、図４に示すように、図２に示すものとは異なるイベント・リストが、時間軸４００に適用されている。時間軸４００上で時間０において開始する際、最大優先キュー（図示せず）は、空である。挿入動作Ｉ０（９）４１０は、時間０において開始する。従って、挿入された値「９」は、最大優先キュー内で「ピーク」（すなわち、最高値）である。次に、Ｉ１（１０）４２０は、「１０」の値を最大優先キューに挿入し、その値がピークになる。従って、除去動作Ｒ２（９）４３０が開始するとき、キュー内の最大の要素は１０である。さらに、Ｒ２（９）４３０のインターバル中のどの時点においても、キュー内の最大の要素は９にならないであろう。前述のように、最大優先キュー（図示せず）のための並行性ルールに従って、１つの除去動作が有効であるのは、これがキューのための最高値を除去するときだけである。このため、Ｒ２（９）４３０は、有効な動作ではないから、図４のシーケンスは正しくない。しかし、留意すべきは、Ｒ２（９）４３０が図４の履歴内に存在しなかったならば、この履歴は、有効であるだろうということである。なぜなら、除去動作Ｒ４（１０）４４０は、挿入動作Ｉ１（１０）４２０に関連付けられるであろうからである。この結果がどのように得られるかということについては、図４のサンプル・データに対する実施形態の適用に関連して、以下で説明する。
【００２５】
従って、図４に示すように、実施形態は、並行性ルールを定義することによって、１つの除去動作を対応する１つの挿入動作に割り当てる（又はペア化する）ことができず、そして依然として最大優先キュー特性を順守することを決定する。従って、この除去動作を割り当てることができないときは、この履歴は、無効であると見なされ、拒否される。
【００２６】
従って、実施形態によれば、後述するように、イベントに応答して状態を拡張及び崩壊させることができる。例えば、最初の動作の前には、単一の状態だけが存在する。この状態は、データ構造（すなわち、前述の最大優先キュー）が空であり且つ未処理の動作は存在しないことを指示する。この初期化された状態から開始して、イベントは、検証中のデータ構造のために定義された関連するルールに従って、このデータ構造の状態を修正し且つ追加の状態を作成するであろう。
【００２７】
図５は、実施形態に従った、状態の管理（すなわち、状態の拡張及び崩壊）のためのプロセスを示すフローチャートである。ステップ５０５では、テスト・ランを実行して、実行トレース（例えば、図１に示されるもの）を構築する。例えば、このテスト・ランが実行するソフトウェアは、並行にアクセスされるデータ構造（例えば、マルチコア・アーキテクチャ上で実行される最大優先キュー）を使用する。ステップ５１０では、この実行トレースから、イベントの分類済みリストを作成する。前述のように、実施形態では、この実行トレース内の各原子動作は、２つのイベント（１つの開始イベント及び１つの終了イベント）を生成し、各イベントは、１つのタイムスタンプを有する。従って、ステップ５１０で作成したイベントの分類済みリストは、この分類済みリストが（例えば、図２に示すように）厳密に単調に増加することを保証するため、タイムスタンプによって分類されたイベントのリストを含む。
【００２８】
ステップ５１５は、イベント処理ループ（後述）を開始し、ステップ５１０で作成した分類済みリストからの最初の未処理イベントを処理する。ステップ５２０では、ステップ５１５で処理したイベントが開始イベントであるか否かを決定する。もし、このイベントが開始イベントであれば、ステップ５２５では、この開始イベントと一致する動作を各未処理状態に追加する。次のステップ５３０では、可能であれば、現に未処理の状態ごとに、この動作を完了させる新しい状態を追加する。この動作の完了は、データ構造のために定義された１セットの並行性ルール及びステップ５０５のテスト・ラン中に実行されたソリューションに依存する。例えば、前述の最大優先キューについては、ステップ５３０において全ての挿入動作を完了させる１つのルールを定義することができる（というのは、挿入動作は、完了すべき他の動作に依存しないからである）。しかし、ステップ５３０では、除去動作は、完了されないであろう。なぜなら、完了済みの除去動作は、（最大優先キューのために定義されるような）一致する挿入動作が完了していることを必要とするからである。
【００２９】
その後のステップ５３５では、現在の状態セット内に任意の未処理の動作が残っているか否かを決定する。そうでなければ、本プロセスは、ステップ５１５に戻り、ステップ５１０で作成したイベントの分類済みリスト内の次のイベントの処理を開始する。しかし、未処理の動作が状態セット内に残っていれば、ステップ５４０で、これらの未処理の動作を各状態に再帰的に適用することにより、新しい状態を作成して、本プロセスを完了する。
【００３０】
ステップ５２０に戻って、説明を続ける。もし、終了イベントであることを決定すれば、本プロセスは、ステップ５４５において、状態セット内の状態のうちこの動作（ステップ５２０で分類済みイベント・リストから除去された当該終了イベントと一致するもの）が未処理であるような全ての状態を除去する。その後のステップ５５０において、状態セットが空であることを決定すれば、本プロセスは、ステップ５７０で終了し、「履歴は直線化可能ではない」という出力を、例えば、ディスプレイ装置又はストレージ装置に提供する。もし、ステップ５５０において、状態セットが空ではないことを決定すれば、ステップ５６０において、分類済みイベント・リスト内に任意のイベントが残っているか否かを決定する。全てのイベントが処理済みであることを決定すれば、ステップ５６５において、「履歴は直線化可能である」という出力を、例えば、ディスプレイ装置又はストレージ装置に提供する。もし、分類済みイベント・リスト内に未処理のイベントが存在すれば、ステップ５１５に戻って、次のイベントの処理を開始する。
【００３１】
以下、図６〜図１３を参照して、実施形態に従った特定の例を説明する。図６〜図１３の例は、汎用コンピュータ（例えば、コンピュータ可読命令の実行を通して特定の目的を遂行するように適合された、図１４のコンピュータ・システム）上で実装することができる。これらのコンピュータ可読命令は、当分野で公知の任意の手段を使用して、プログラマによって準備することができる。かかる手段の１つの例は、これらの例に関連して後述するような、Ｊａｖａ（登録商標）又はこれと同等のプログラミング言語である。しかし、実施形態は、Ｊａｖａ（登録商標）プログラミング言語に限定されない。
【００３２】
例えば、１つの状態の構成は、図６のテーブルに従って定義することができる。図６のテーブルは、Ｊａｖａ（登録商標）プログラミング言語（例えば、Zakhour et al., The Java Tutorial: A Short Course on theBasics, 4th Edition (2006) を参照）に記述されているような、データ「コレクション」の概念を使用する。すなわち、コレクションのコンテンツは、データ構造に追加すべき値又はデータ構造から除去すべき値を含む（すなわち、並行式最大優先キューに追加される値は、「終了済みの挿入」コレクション内に含まれるであろう）。しかし、Ｊａｖａ（登録商標）コレクションの使用は、１つの実装であるに過ぎず、他のデータ構造を使用することも可能であろう。他の例では、全ての状態によって共有される１つのデータ・コレクションは、「確定ヒープ」コレクションとして定義される。この「確定ヒープ」コレクションは、最大優先キュー内に格納されたコンテンツを、状態セット内の全ての状態によって作用されるものとして記述する。従って、前述の実施形態では、「確定ヒープ」コレクションは、完了済みの挿入動作の全てのログ・エントリを保持する。そうでなければ、これらのログ・エントリは、図６に示すような、全ての状態の「終了済みの挿入」構造内に格納されていたであろう。従って、前述の最大優先キューは、状態ごとに、確定ヒープ内の要素及び「終了済みの挿入」構造内に保持される要素から成る。
【００３３】
図７〜図１３内の表記をさらに簡潔化するため、各ログ・エントリは、動作を指示する記号と、その後に続くログ・エントリＩＤと、括弧内の値によって記述されるものとする。例えば、エントリＩ２（１５）は、値１５の要素を挿入する、ＩＤ「２」の「挿入」動作を表す。さらに、各リストは、ブラケットによって表され、当該リスト内の要素は、コンマによって区切られ、そして各ペアは、括弧によって表されるものとする。さらに、図７〜図１３では、次の状態記述の略語が使用されるものとする。
ｐＲ  ＝「未処理の除去（pending removals）」コレクション
ａＲ  ＝「関連する除去（associated removals）」コレクション
ｐＩ  ＝「未処理の挿入（pending insertions）」コレクション
ｆＩ  ＝「終了済みの挿入（finished insertions）」コレクション
ｄＨ  ＝「確定ヒープ（definite heap）」コレクション
【００３４】
実施形態に従って、１つの並行性ルールが定義される。このルールによれば、挿入動作のための開始イベント（例えば、Ｉ６（５）の開始イベント７１０）は、１つ以上の未処理の挿入動作を暗示する。このため、図７に示すように、対応するログ・エントリＩＤを「未処理の挿入」コレクションに追加することにより、状態セット内の各状態が修正される。図７に示す例では、Ｉ６（５）をｐＩコレクション７２６に追加することにより、状態７２０が修正され、その結果、（ｐＩコレクション７２６内に含まれるＩ６（５）を有する）状態７３０になる。
【００３５】
図８に示すように、他の並行性ルールが定義される。このルールによれば、１つの挿入動作が最大優先キューのピークに等しいか又はこれより大きい値を挿入するような状態ごとに、「未処理の除去」コレクションをチェックすることにより、この値を除去する未処理の除去動作が存在するか否かを決定する。このため、例示的な状態セット８００では、Ｉ６（５）の開始イベント８１０は、状態８２０に影響する。なぜなら、挿入される値は、（ｄＨコレクション８１２によって指示されるような）最大優先キューのピークに等しいからである。従って、この並行性ルールは、対応する除去動作が存在するとき、（図５のステップ５４０に従って）新しい状態８４０を作成することを指令する。この新しい状態８４０は、関連する挿入／除去動作のペアをａＲコレクション８２２に追加し且つ検出された除去動作をｐＲコレクション８４４から除去する。さらに、状態８２０は、状態８３０になるように修正され、そこではＩ６（５）がｐＩコレクション８２６に追加される。
【００３６】
図９は、１つの挿入動作（例えば、Ｉ６（５））が終了するときの状態セット９００を例示する。その終了イベント９１０に到達する際、状態セット９００を探索することにより、終了中の挿入動作（例えば、Ｉ６（５））が、図６に示す「未処理の挿入」コレクション内に依然として存在するか否かを決定する。もし、この挿入動作が未処理でなければ、この挿入動作は、「関連する除去」コレクション内に保持される１つの関連するペアの一部である。もし、この挿入動作が当該関連するペアの第２のコンポーネントであって、同様に完了されるのであれば、この挿入動作は、このリストから除去される。もし、「未処理の挿入」コレクションがこの挿入動作を保持していれば、この挿入動作を「未処理の挿入」コレクションから除去し且つこの挿入動作を「終了済みの挿入」コレクションに追加する。両方の動作は、図９に示されている。状態９２０では、Ｉ６（５）はｐＩコレクション９２６内にあり、Ｉ６（５）の終了イベント９１０を処理する際に、状態９２０は、Ｉ６（５）がｆＩコレクション９２８に追加された状態９４０になる。一方、状態９３０では、Ｉ６（５）はａＲコレクション９２２内にあり、従ってＩ６（５）及び関連する除去動作の両方が終了するとき、状態９３０は９５０になる。図９には示されていないが、他の実施形態によれば、もし、１つの挿入動作（例えば、Ｉ６（５））が全ての状態の「終了済みの挿入」コレクション内に存在すれば、この挿入動作は、状態セット内の全ての状態から除去され且つ「確定ヒープ」コレクションに追加される。
【００３７】
図１０は、１つの除去動作（例えば、Ｒ５（３））に対応する開始イベント１０１０が追加されつつある、状態セット１０００を例示する。除去動作の開始は、可能なイベント（例えば、挿入開始、除去開始、挿入終了及び除去終了）のうち最も複雑なイベントである。前述のように、状態セット内の各状態は、挿入動作のための開始イベントと同様に、この動作を「未処理の除去」コレクション（例えば、状態１０３０内のｐＲコレクション１０３４）に追加することにより修正される。この除去動作が最大優先キューの値に等しいか又はこれより大きい値を除去するとき、実施形態は、「未処理の挿入」コレクション（例えば、状態１０２０内のｐＩコレクション１０２６）を探索し且つ適切な挿入動作で作成可能な（状態１０４０のａＲコレクション１０２２内に示されるような）関連ごとに１つの新しい状態（例えば、状態１０４０））を作成する。さらに、除去された値が最大優先キューのピークに等しければ、１つの新しい状態（例えば、状態１０５０）が作成され、（状態１０５０のａＲコレクション１０２２内に示されるように）最大優先キューのピークと関連付けられる。もし、このピークが「確定ヒープ」コレクション（例えば、ｄＨコレクション１０１２）内に存在すれば、この除去動作のオペランド値は、「確定ヒープ」コレクションから除去され（ｄＨコレクション１０１４を参照）、そして状態セット内の全ての状態（例えば、状態１０３０、１０４０及び１０５０）の「終了済みの挿入」コレクションに追加される。次に、図１０には示されていないが、これらの未処理の除去動作は、他の未処理の挿入動作と再帰的に関連付けられる。というのは、新しいピークは、可能であればより小さい値を以て、確定ヒープ内で定義されるからである。図１０には示されていないが、未処理の除去動作をこの新しいピークと関連付けることも、この再帰なステップの一部である。実施形態では、状態セットを有効に処理するために、複数の組み合わせ方法を適用することができる。
【００３８】
図１１は、１つの除去動作（例えば、Ｒ５（３））が終了するときの状態セット１１００を例示する。この除去動作の終了イベント１１１０は、状態セット１１００の基数を減少させるイベントである。このイベントを処理することによって、状態セットから除去される状態は、無効であると示される。例えば、状態１１２０において、この除去動作は、依然としてｐＲコレクション１１２４内に存在する。従って、参照番号１１１６で示すように、状態１１２０は、状態セット１１００から除去される。なぜなら、この除去動作は、１つの挿入動作と関連付けることができないからである。もし、このイベントが、（例えば、状態セット１１００のｐＲコレクション１１２４内に示されるように）「未処理の除去」コレクション内に存在しない除去動作（例えば、Ｒ５（３））に対応すれば、この除去動作は、「関連する除去」コレクション（例えば、ａＲコレクション１１２２）内に存在するであろう。１つの挿入動作に対するこの終了イベントを処理するのと同様に、実施形態は、関連するペアの一部であるこの挿入動作が同様に完了しているか否かをチェックする。ペア化された挿入動作が完了していないとき、この挿入／除去動作のペアは、ａＲコレクション（例えば、状態１１５０内のａＲコレクション１１２２）内に残存し、その挿入及び除去動作の両方が終了したならば、そのペアが除去される（状態１１６０を参照）。挿入動作のための終了イベントと同様に、実施形態によれば、このイベントの後に如何なる状態も残存していなければ、出力履歴は無効である。
【００３９】
図１１には示されていないが、ヌルの除去（すなわち、オペランドを有しない除去動作）は、特別なケースである。ヌルを除去することができた時点が存在するとすぐに、この動作は直ちに除去され、そしてヌルが後の時点で除去することができたケースを考慮しない。
【００４０】
図１２は、実施形態に従って図３のサンプル・データを検証した場合の、状態変更のシーケンス１２００を例示する。状態セット１２０１は、初期条件を示し、イベント１２１０は処理すべき第１のイベントである。イベント１２１０は、ヌルの除去動作に対応するから、状態セット１２１１内の如何なる状態も変更されない。イベント１２１０は、Ｉ１（４）を状態セット１２２１に追加し（ｐＩコレクション１２２８を参照）、イベント１２３０は、この挿入動作を終了する。イベント１２４０は、第２の挿入動作を開始する。この第２の挿入動作は、Ｉ２（５）を既存の状態に追加するが（ｐＩコレクション１２４８を参照）、イベント１２５０は、Ｉ２（５）が終了する前にＲ３（４）を開始する。従って、状態１２５５及び１２６０が作成され、Ｒ３（４）がｐＲコレクション１２５７及びａＲコレクション１２６１にそれぞれ追加される。次に、イベント１２６５が処理されて、状態１２７０及び１２７５に至り、そこでＩ１（４）がｆＩコレクション１２７４及びａＲコレクション１２７６にそれぞれ追加される。イベント１２８０の間、状態１２７０はｐＲコレクション１２７２内にＲ３（４）を有するから、状態１２７０は無効であると見なされ、参照番号１２８２によって示すように、状態セット１２８１から除去される。しかし、状態１２７５は、１つの挿入／除去ペアをａＲコレクション１２７６から除去して、状態１２８５になる。その後、最後のイベント１２９０が、Ｉ２（５）を終了する。状態セット１２９１は空ではないから、状態１２９５に対応する動作のシーケンスは、正しいと検証される。なお、状態セット１２９１内の全ての状態はＩ２（５）を含むので、ｄＨコレクション１２９２は、Ｉ２（５）を含む。
【００４１】
図１３は、実施形態に従って図４のサンプル・データにおけるエラーを検証した場合の、状態変更のシーケンス１３００を例示する。図１２と同様に、状態セット１３０１は、イベント１３１０を処理する前の状態（例えば、状態１３０５）の条件を示す。イベント１３１０が処理されるとき、状態セット１３０１は、状態セット１３１１に修正される（例えば、状態１３１５はｐＲコレクション１３１７内にＲ２（９）を含む）。次に、イベント１３２０は、第２の除去動作を開始する。ｄＨコレクション１３１２のコンテンツに起因して、イベント１３２０を処理すると、状態１３３０、１３３５及び１３４０が状態セット１３２１に追加される。イベント１３４５の処理中、状態セット１３４６内に示されるように、状態１３３０及び１３４５が、状態セット１３２１から除去される（例えば、参照番号１３４８及び１３４９を参照）。イベント１３５５を処理すると、状態セット１３４６内の状態１３５０が状態セット１３５６内の状態１３６０に修正される。イベント１３６５は、状態セット１３５６から状態１３６０を除去し、その結果、参照番号１３６６に示すように、空の状態セットが得られる。
【００４２】
図１４は、本明細書に開示した検証技術を実装するために使用することができる、実施形態に従った、一般的なコンピュータ環境１４００を示す。コンピュータ環境１４００は、コンピュータ環境の１つの例であるに過ぎず、コンピュータ及びネットワーク・アーキテクチャの使用の範囲又は機能性に関する如何なる制限事項をも示唆することを意図していない。また、コンピュータ環境１４００については、その任意の１つのコンポーネント又は複数のコンポーネントに関係する如何なる依存性又は要件を有するものと解釈すべきではない。
【００４３】
コンピュータ環境１４００は、汎用コンピュータ１４０２を含む。コンピュータ１４０２のコンポーネントは、１つ以上のプロセッサ又は処理ユニット１４０４と、システム・メモリ１４０６と、プロセッサ１４０４を含む種々のシステム・コンポーネントをシステム・メモリ１４０６に結合するシステム・バス１４０８とを含む。
【００４４】
システム・バス１４０８は、幾つかのバス・アーキテクチャのうち任意のものを表し、メモリ・バス又はメモリ・コントローラ、周辺バス、アクセラレイテッド・グラフィック・ポート、及び種々のバス・アーキテクチャのうち任意のものを使用するプロセッサ又はローカル・バスを含む。例えば、かかるアーキテクチャは、業界標準アーキテクチャ（ＩＳＡ）バス、マイクロ・チャンネル・アーキテクチャ（ＭＣＡ）バス、拡張ＩＳＡ（ＥＩＳＡ）バス、ビデオ・エレクトロニクス標準化団体（ＶＥＳＡ）ローカル・バス及びメザニン・バスとして知られている周辺コンポーネント相互接続（ＰＣＩ）バスを含むことができる。
【００４５】
一般に、コンピュータ１４０２は、種々のコンピュータ可読媒体を含む。かかる媒体は、コンピュータ１４０２によってアクセス可能な任意の媒体であって、揮発性及び不揮発性の媒体、取り外し可能及び取り外し不能な媒体を含む。
【００４６】
システム・メモリ１４０６は、ランダム・アクセス・メモリ（ＲＡＭ）１４１４のような揮発性メモリ、及び／又は読み取り専用メモリ（ＲＯＭ）１４１２のような不揮発性メモリの形式を有する、コンピュータ可読媒体を含む。基本入出力システム（ＢＩＯＳ）１４１４は、ＲＯＭ１４１２内に格納される。ＢＩＯＳ １４１４内に保持される基本ルーチンは、起動中のような、コンピュータ１４０２内の要素間の情報を転送するのを支援する。一般に、ＲＡＭ１４１０は、処理ユニット１４０４に直ちにアクセス可能であるか、又は処理ユニット１４０４によって現に操作される、データ及び／又はプログラム・モジュールを保持する。
【００４７】
また、コンピュータ１４０２は、他の取り外し可能／取り外し不能、揮発性／不揮発性のコンピュータ・ストレージ媒体を含むことができる。例えば、図１４には、取り外し不能で不揮発性の磁気媒体（図示せず）を対象とする読み書きを行うためのハードディスク・ドライブ１４１６と、取り外し可能で不揮発性の磁気ディスク１４２０（例えば、フレキシブル・ディスク）を対象とする読み書きを行うための磁気ディスク・ドライブ１４１８と、取り外し可能で不揮発性の光ディスク１４２４（例えば、ＣＤ−ＲＯＭ、ＤＶＤ−ＲＯＭ又は他の光媒体）を対象とする読み書きを行うための光ディスク・ドライブ１４２２が図示されている。ハードディスク・ドライブ１４１６、磁気ディスク・ドライブ１４１８及び光ディスク・ドライブ１４２２の各々は、１つ以上のデータ媒体インタフェース１４２６によって、システム・バス１４０８に接続される。代替的に、ハードディスク・ドライブ１４１６、磁気ディスク・ドライブ１４１８及び光ディスク・ドライブ１４２２は、１つ以上のインタフェース（図示せず）によって、システム・バス１４０８に接続することができる。
【００４８】
これらのディスク・ドライブ及びそれらの関連するコンピュータ可読媒体は、コンピュータ１４０２のためのコンピュータ可読命令、データ構造、プログラム・モジュール及び他のデータの不揮発性ストレージを提供する。図１４には、ハードディスク１４１６、取り外し可能な磁気ディスク１４２０及び取り外し可能な光ディスク１４２４が例示されているが、コンピュータによってアクセス可能なデータを格納するために、他のタイプのコンピュータ可読媒体を使用することができる。これらのコンピュータ可読媒体は、磁気カセット又は他の磁気ストレージ装置、フラッシュ・メモリ・カード、ＣＤ−ＲＯＭ、ＤＶＤ又は他の光ストレージ、ＲＡＭ、ＲＯＭ、電気的消去可能ＲＯＭ（ＥＥＰＲＯＭ）等を含む。
【００４９】
任意の数のプログラム・モジュール（例えば、オペレーティング・システム１４２６、１つ以上のアプリケーション・プログラム１４２８、他のプログラム・モジュール１４３０及びプログラム・データ１４３２）を、ハードディスク１４１６、磁気ディスク１４２０、光ディスク１４２４、ＲＯＭ１４１２及び／又はＲＡＭ １４１０上に格納することができる。かかるオペレーティング・システム１４２６、１つ以上のアプリケーション・プログラム１４２８、他のプログラム・モジュール１４３０及びプログラム・データ１４３２（又はそれらの組み合わせ）の各々は、分散ファイル・システムをサポートする常駐コンポーネントの全部又は一部を実装することができる。
【００５０】
ユーザは、キーボード１４３４及びポインティング装置１４３６（例えば、マウス）のような入力装置を介して、コマンド及び情報をコンピュータ１４０２に入力することができる。他の入力装置１４３８（詳細に図示されていない）は、マイクロホン、ジョイスティック、ゲーム・パッド、衛星放送アンテナ、シリアル・ポート、スキャナ等を含むことができる。これら及び他の入力装置は、システム・バス１４０８に結合された入力／出力インタフェース１４４０を介して処理ユニット１４０４に接続されるが、パラレルポート、ゲーム・ポート又はユニバーサル・シリアル・バス（ＵＳＢ）のような他のインタフェース及びバス構造によっても接続することができる。
【００５１】
また、モニタ１４４２又は他のタイプのディスプレイ装置を、ビデオ・アダプタ１４４４のようなインタフェースを介して、システム・バス１４０８に接続することができる。モニタ１４４２に加えて、他の出力周辺装置は、スピーカ（図示せず）及びプリンタ１４４６のようなコンポーネントを含み、これを入力／出力インタフェース１４４０を介してコンピュータ１４０２に接続することができる。
【００５２】
コンピュータ１４０２は、遠隔コンピュータ１４４８のような１つ以上の遠隔コンピュータへの論理的な接続を使用する、ネットワーク化環境内で動作することができる。例えば、遠隔コンピュータ１４４８は、パーソナル・コンピュータ、ポータブル・コンピュータ、サーバ、ルータ、ネットワーク・コンピュータ、ピア装置又は他の通常のネットワーク・ノード等とすることができる。遠隔コンピュータ１４４８は、ポータブル・コンピュータとして例示され、コンピュータ１４０２に関連して本明細書で説明した要素及び特徴の全部又は一部を含むことができる。
【００５３】
コンピュータ１４０２と遠隔コンピュータ１４４８との間の論理的な接続は、ローカル・エリア・ネットワーク（ＬＡＮ）１４５０及び一般的な広域ネットワーク（ＷＡＮ）１４５２として図示されている。ＬＡＮ及びＷＡＮの両方は、有線通信媒体及び適切な通信プロトコル（例えば、イーサネット（登録商標））又は無線通信媒体及び適切な通信プロトコル（例えば、ＷＩ−ＦＩ）を介して、論理的な接続を形成する。かかるネットワーク環境は、ホーム、オフィス、企業規模のコンピュータ・ネットワーク、イントラネット及びインターネット内で通常のものである。
【００５４】
ＬＡＮネットワーク環境内で実装される場合、コンピュータ１４０２は、ネットワーク・インタフェース又はアダプタ１４５４を介して、ローカル・ネットワーク１４５０に接続される。ＷＡＮネットワーク環境内で実装される場合、コンピュータ１４０２は、広域ネットワーク１４５２上の通信を確立するためのモデム１４５６又は他の手段を含むのが普通である。モデム１４５６（コンピュータ１４０２の内部又は外部に設置可）は、入力／出力インタフェース１４４０又は他の適切な機構を介して、システム・バス１４０８に接続することができる。図示したネットワーク接続は、例示的なものであるに過ぎず、コンピュータ１４０２と遠隔コンピュータ１４４８との間の通信リンクを確立するための他の手段を使用することができる。
【００５５】
コンピュータ環境１４００のようなネットワーク化環境では、コンピュータ１４０２に関連して説明したプログラム・モジュール又はその一部は、遠隔のメモリ・ストレージ装置内に格納することができる。例えば、遠隔アプリケーション・プログラム１４５８は、遠隔コンピュータ１４４８のメモリ装置上に存在する。本明細書では、説明の便宜上、アプリケーション・プログラム及びオペレーティング・システムのような他の実行可能プログラム・コンポーネントは、個別ブロックとして示されているが、かかるプログラム及びコンポーネントは、種々の時間においてコンピュータ１４０２の異なる記憶コンポーネント内に存在し、コンピュータ１４０２の処理ユニット１４０４によって実行される。
【００５６】
１つ以上のコンピュータ又は他の装置によって実行される、プログラム・モジュールのようなコンピュータ実行可能命令の一般的な文脈において、本明細書では、種々のモジュール及び技術を説明することができる。一般に、プログラム・モジュールは、特定のタスクを実行するか又は特定の抽象データ・タイプを実装するための、ルーチン、プログラム、オブジェクト、コンポーネント、データ構造等を含む。一般に、これらのプログラム・モジュールの機能性は、種々の実施形態における要請に応じて、組み合わせるか又は分散させることができる。
【００５７】
これらのモジュール及び技術の実装は、特定の形式を有するコンピュータ可読媒体上に格納するか、又はかかるコンピュータ可読媒体を通して伝送することができる。コンピュータ可読媒体は、コンピュータによってアクセス可能な、任意の媒体とすることができる。例えば、コンピュータ可読媒体は、「コンピュータ・ストレージ媒体」及び「通信媒体」を含むことができる。
【００５８】
「コンピュータ・ストレージ媒体」は、コンピュータ可読命令、データ構造、プログラム・モジュール又は他のデータのような情報を記憶するために、任意の方法又は技術で実装された、揮発性及び不揮発性で、取り外し可能及び取り外し不能な媒体を含む。コンピュータ・ストレージ媒体は、ＲＡＭ、ＲＯＭ、ＥＥＰＲＯＭ、フラッシュ・メモリ若しくは他のメモリ技術、ＣＤ−ＲＯＭ、ＤＶＤ若しくは他の光ストレージ、磁気カセット、磁気テープ、磁気ディスク・ストレージ若しくは他の磁気ストレージ装置、又は所望の情報を格納するために使用可能であり且つコンピュータによってアクセス可能な他の媒体を含む。
【００５９】
一般に、「通信媒体」は、コンピュータ可読命令、データ構造、プログラム・モジュール又は他のデータを、搬送波又は他の移送機構のような変調データ信号の形式で実装する。また、通信媒体は、任意の情報配信媒体を含む。「変調データ信号」という用語は、情報を当該信号内にエンコードするような態様でその１つ以上の特性を設定されるか又は変更される信号を意味する。例えば、通信媒体は、有線ネットワーク又は直接有線接続のような有線媒体と、音響、無線周波数（ＲＦ）、赤外線及び他の無線媒体のような無線媒体とを含む。前述の媒体の任意の組み合わせも、コンピュータ可読媒体の範囲内に含まれる。
【００６０】
本発明は、ハードウェア、ソフトウェア又はハードウェア及びソフトウェアの組み合わせとして具体化することができる。本明細書に開示した方法を実施するのに適していれば、任意の種類のコンピュータ／サーバ装置又は他の装置を使用することができる。ハードウェア及びソフトウェアの代表的な組み合わせは、汎用コンピュータ・システムと、当該システムにロードされ且つ実行されるとき、本明細書に開示した方法を実施するコンピュータ・プログラムとの組み合わせとすることができる。代替的に、本発明の１つ以上の機能的なタスクを実施するための専用ハードウェアを含む、専用コンピュータを使用することができる。
【００６１】
また、本発明又は本発明の側面は、本明細書に開示した方法の実装を可能にする全ての特徴を備え、コンピュータ・システムにロードされるときに、これらの方法を実施することができる、コンピュータ・プログラムとして具体化することができる。この文脈上、コンピュータ・プログラム、ソフトウェア・プログラム、プログラム又はソフトウェアは、任意の言語における１セットの命令の任意の表現、コード又は表記であって、情報処理能力を有するシステムに特定の機能を直接に、又は（ａ）他の言語、コード又は記法への変換及び／又は（ｂ）異なる資料形式における複製の後に、実行させるものを意味する。
【００６２】
本発明が前述の目的を達成するように工夫されていることは明らかであるが、当業者には明らかなように、種々の修正及び変更を行うことができる。従って、各請求項の記載は、かかる全ての修正及び変更が本発明の精神及び範囲に属するものとして、これを包含することを意図している。
【図１】
2010186476.tif 000003
【図２】
2010186476.tif 000004
【図３】
2010186476.tif 000005
【図４】
2010186476.tif 000006
【図５】
2010186476.tif 000007
【図６】
2010186476.tif 000008
【図７】
2010186476.tif 000009
【図８】
2010186476.tif 000010
【図９】
2010186476.tif 000011
【図１０】
2010186476.tif 000012
【図１１】
2010186476.tif 000013
【図１２】
2010186476.tif 000014
【図１３】
2010186476.tif 000015
【図１４】
2010186476.tif 000016