(57)【要約】  制約を発生して解くための方法及び装置が開示される。一実施形態において、この方法は、解かれない変数を有する１つ以上のダイナミックアノテーションを挿入することによりプログラムコードを変更するステップと、ベリファイアを使用して前記１つ以上のダイナミックアノテーションに基づいて１つ以上の制約を発生するステップと、前記１つ以上の発生された制約を解くステップと、解かれない変数を含むアノテーションに代わってダイナミックアノテーションを挿入することにより前記プログラムコードを変更するステップと、を備える。【選択図】図１Ｂ
2008519365.tif 000002
【特許請求の範囲】
【請求項１】
解かれない変数を有する１つ以上のダイナミックアノテーションを挿入することによりプログラムコードを変更するステップと、
ベリファイアを使用して前記１つ以上のダイナミックアノテーションに基づき１つ以上の制約を発生するステップと、
前記１つ以上の発生された制約を解くステップと、
解かれない変数を含むアノテーションに代わってダイナミックアノテーションを挿入することにより前記プログラムコードを変更するステップと、
を備える方法。
【請求項２】
前記ダイナミックアノテーションは、前記プログラムコードへのダイナミックコールを含む、請求項１に記載の方法。
【請求項３】
前記プログラムコードを変更する前記ステップは、チェックのセマンティックスを保存する間に行われる、請求項１に記載の方法。
【請求項４】
前記プログラムコードに対するリソース使用制約を発生するステップと、
前記プログラムコードのリソース使用を評価する間に発生される制約を解くステップと、
を更に備える請求項１に記載の方法。
【請求項５】
制約を解くことからの結果に基づいてプログラムリソース使用の安全性を高めるようにプログラムにアノテーションを自動的に挿入するステップを更に備える、請求項１に記載の方法。
【請求項６】
前記プログラムコードを評価する間に１つ以上のリソース制約を識別するステップと、
前記識別された制約に基づいて前記プログラムコードに１つ以上のアノテーションを挿入することにより前記プログラムコードにアノテーション付けするステップと、
を更に備える請求項１に記載の方法。
【請求項７】
前記プログラムコードに入れられた制約を評価するステップと、
前記制約に関する情報をダイナミックにフィードバックするステップと、
前記フィードバック情報に応答して１つ以上のダイナミックタスクを挿入することにより前記コンピュータプログラムにアノテーション付けして、前記プログラムコードを安全な仕方で実行させるステップと、
を更に備える請求項１に記載の方法。
【請求項８】
制約を規範的形態で解くことにより、前記プログラムコードを実行する前に、前記プログラムコードに対してスタティック分析を遂行するステップと、
１つ以上の解かれない項を有する１つ以上の制約を識別するステップと、
次のことを繰り返すステップであって、
排除することで１つ以上の制約を最大限度簡単化するところの前記解かれない項のうちの１つの項を識別し、そして
前記プログラムコードにおけるダイナミックオペレーションのスタティック尺度をダイナミックオペレーションに置き換えることで前記１つの項を排除する、
ことを繰り返すステップと、
を更に備えた請求項１に記載の方法。
【請求項９】
前記ダイナミックオペレーションは、前記プログラムコードのランタイム中に呼び出される前記プログラムコードへのダイナミックエバルエータに対するコールである、請求項８に記載の方法。
【請求項１０】
システムにより実行されるときに、該システムが、
解かれない変数を有する１つ以上のダイナミックアノテーションを挿入することによりプログラムコードを変更するステップと、
ベリファイアを使用して前記１つ以上のダイナミックアノテーションに基づいて１つ以上の制約を発生するステップと、
前記１つ以上の発生された制約を解くステップと、
解かれない変数を含むアノテーションに代わってダイナミックアノテーションを挿入することにより前記プログラムコードを変更するステップと、
を備える方法を遂行するようにさせるインストラクションを記憶する１つ以上の記録可能な媒体を有する製造物品。
【請求項１１】
前記方法は、更に、
前記プログラムコードに対するリソース使用制約を発生するステップと、
前記プログラムコードのリソース使用を評価する間に発生される制約を解くステップと、
を備える請求項１０に記載の製造物品。
【請求項１２】
前記方法は、更に、
前記プログラムコードに入れられた制約を評価するステップと、
前記制約に関する情報をダイナミックにフィードバックするステップと、
前記フィードバック情報に応答して１つ以上のダイナミックタスクを挿入することにより前記コンピュータプログラムにアノテーション付けして、前記プログラムコードを安全な仕方で実行させるステップと、
を備える請求項１０に記載の製造物品。
【請求項１３】
前記ダイナミックアノテーションはリソース使用を捕獲する、請求項１に記載の方法。
【請求項１４】
解かれない変数を有する１つ以上のダイナミックアノテーションを挿入することによりプログラムコードを変更する前記ステップは、リソース使用に関連したプログラムの始めに１つのアノテーションのみを挿入し、次いで、これを使用して、前記プログラムコードに対するリソース使用を推定することを含む、請求項１に記載の方法。
【請求項１５】
メモリと、
メモリに結合されたプロセッサであって、
解かれない変数を有する１つ以上のダイナミックアノテーションを挿入することによりプログラムコードを変更するステップと、
ベリファイアを使用して前記１つ以上のダイナミックアノテーションに基づいて１つ以上の制約を発生するステップと、
前記１つ以上の発生された制約を解くステップと、
解かれない変数を含むアノテーションに代わってダイナミックアノテーションを挿入することにより前記プログラムコードを変更するステップと、
を備える方法を遂行するために前記メモリに記憶されたインストラクションを実行するプロセッサと、
を備える装置。
【請求項１６】
コンピュータプログラムコードのリソース使用を評価するステップと、
前記コンピュータプログラムコードのリソース使用の評価結果に基づいてリソース使用の安全性のために前記コンピュータプログラムコードに１つ以上のオペレーションを挿入することによりコンピュータプログラムにアノテーション付けするステップと、
を備える方法。
【請求項１７】
前記コンピュータプログラムコードのリソース使用の評価結果に基づいてリソース使用の安全性のために１つ以上のリソース消費制約を除去するように前記コンピュータプログラムコードに１つ以上のオペレーションを挿入するステップを更に備える、請求項１６に記載の方法。
【請求項１８】
１つ以上の解かれない項を有する１つ以上の制約を識別するステップと、
前記コンピュータプログラムコードによるリソース使用の評価結果に応答して、前記コンピュータプログラムコードに１つ以上の取得オペレーションを挿入し、解かれない項に対応する１つ以上のリソース消費制約を所定値にセットして、リソース使用の安全性を達成するステップと、
を更に備える請求項１６に記載の方法。
【請求項１９】
前記所定値はゼロである、請求項１８に記載の方法。
【請求項２０】
アノテーションを伴う前記コンピュータプログラムコードはサウンドである、請求項１６に記載の方法。
【請求項２１】
アノテーションを伴う前記コンピュータプログラムコードは、リソース使用の安全性のためのスタティックベリファイアをパスする、請求項１６に記載の方法。
【請求項２２】
システムにより実行されたときに、該システムが、
コンピュータプログラムコードのリソース使用を評価するステップと、
前記コンピュータプログラムコードのリソース使用の評価結果に基づいてリソース使用の安全性のために前記コンピュータプログラムコードに１つ以上のオペレーションを挿入することによりコンピュータプログラムにアノテーション付けするステップと、
を備える方法を遂行するようにさせるインストラクションを記憶した１つ以上の記録可能な媒体を有する製造物品。
【請求項２３】
前記方法は、更に、前記コンピュータプログラムコードのリソース使用の評価結果に基づいてリソース使用の安全性のために１つ以上のリソース消費制約を除去するように前記コンピュータプログラムコードに１つ以上のオペレーションを挿入するステップを備える、請求項２２に記載の製造物品。
【請求項２４】
前記方法は、更に、１つ以上の解かれない項を有する１つ以上の制約を識別するステップと、前記コンピュータプログラムコードによるリソース使用の評価結果に応答して、前記コンピュータプログラムコードに１つ以上の取得オペレーションを挿入し、解かれない項に対応する１つ以上のリソース消費制約を所定値にセットして、リソース使用の安全性を達成するステップとを備える、請求項２２に記載の製造物品。
【請求項２５】
前記所定値はゼロである、請求項２４に記載の製造物品。
【請求項２６】
アノテーションを伴う前記コンピュータプログラムコードはサウンドである、請求項２２に記載の製造物品。
【請求項２７】
アノテーションを伴う前記コンピュータプログラムコードは、リソース使用の安全性のためのスタティックベリファイアをパスする、請求項２２に記載の製造物品。
【請求項２８】
メモリと、
メモリに結合されたプロセッサであって、
コンピュータプログラムコードのリソース使用を評価するステップと、
前記コンピュータプログラムコードのリソース使用の評価結果に基づいてリソース使用の安全性のために前記コンピュータプログラムコードに１つ以上のオペレーションを挿入することによりコンピュータプログラムにアノテーション付けするステップと、
を備える方法を遂行するために前記メモリに記憶されたインストラクションを実行するプロセッサと、
を備える装置。
【発明の詳細な説明】
【優先権】
【０００１】
[0001]本特許出願は、２００４年１１月８日に出願された“Methodand Apparatus for Analyzing and Limiting Resource Use of Sequential ComputerPrograms”と題する対応する米国特許仮出願第６０／６２６，１６６号に対する優先権を請求するものである。
【関連出願】
【０００２】
[0002]本出願は、本発明の法人譲受人に譲渡された２００３年１２月２３日出願の“Flexible and Efficient Method for Limiting the Resource Usage ofComputer Programs”と題する出願中の特許出願である米国特許出願第６０／５３２，３５９号に関連している。
【発明の分野】
【０００３】
[0003]本発明は、コンピュータプログラムをチェックする分野に係り、より詳細には、コンピュータプログラムのスタティック及びダイナミックの両チェックを遂行することに係る。
【発明の背景】
【０００４】
[0004]プログラムは、ここでコードプロデューサと称される個人により製作されて、ここでコードコンシューマと称される個人により実行される。コードコンシューマは、コードプロデューサにより製作された信頼性のないプログラムを実行することを望まない。というのは、プログラムは、ネットワークやファイルのようなリソースにアクセスする機能を与えるランタイムライブラリーを経てコードコンシューマのコンピュータと通信するからである。コードコンシューマは、プログラムの安全性が確保されることを希望し、これは、プログラムがユーザのデータを壊さず、プライベートデータを外部ソースへエクスポートせず、且つシステムリソースを悪用しないことを意味する。
【０００５】
[0005]コンピュータプログラムの安全性を確保するための方法は、多数存在する。これらは、ダイナミックチェック及びスタティックチェックを含む。ダイナミックチェックとは、潜在的に安全でない各々のオペレーションを、それが生じる直前にチェックするプロセスを指す。例えば、安全性ポリシーが特定のディレクトリーへのアクセスを禁止する場合には、ランタイム（ＲＴ）ライブラリー又はＲＴモニタが各ファイルアクセスをチェックしなければならない。ダイナミックチェックは、効果がある。第１に、それは正確である。即ち、プログラムが実際に犯そうとしている安全性違反だけを検出する。チェッカーが違反を検出する場合には、ユーザがチェッカーをターンオフすると、プログラムが実際に違反を犯すことになる。第２に、それは簡単である。全チェッカーは、適当なルーチンと一緒にランタイムライブラリーに入れられる簡単なチェックより成る。しかしながら、ダイナミックチェックは、欠点もある。第１に、考えられる最後の瞬間にエラーを検出するので遅い。遅いことは、警報なしにプログラムを終了して、ユーザを驚かせ又は混乱させ、或いはユーザが貴重なデータを失うことにもなるので、問題である。又、プログラムを終了するときには、プログラムが割り当てたオペレーティングシステム（ＯＳ）リソースを回復することが困難であり、これは、他の実行中プログラムの性能に悪影響を及ぼすことがある。第２に、ダイナミックチェックは、非効率的である。各オペレーションが実行前にチェックを遂行するので、これらチェックは、ＣＰＵ時間の相当の部分を占める。
【０００６】
[0006]スタティックチェックでは、全プログラムが実行の前に分析され、安全であるかどうか調べられる。スタティックチェックは、効果がある。第１に、スタティックチェックは、実行を開始する前に全ての欠陥を検出するという点で早い。従って、チェッカーがプログラムを検証する場合には、ランタイムエラーが生じることはなく、従って、ユーザがデータを失うことがなく、ＯＳがプログラムを終了しなければならないこともない。第２に、スタティックチェックは、効率的である。全てのチェックは、プログラムテキストに基づいて行われ、従って、ランタイムチェックは、何であれ、行われず、プログラムは、完全に信頼性のあるプログラムと同じ速度で実行することができる。又、スタティックチェックにも欠点がある。第１に、スタティックチェックは、複雑である。というのは、プログラムの振舞いについて推論しなければならず、これが複雑だからである。第２に、スタティックチェックは、幾つかの安全なプログラムを拒絶するという意味で不完全である。この不正確さは、２つの原因から生じる。第１に、プログラムが複雑である。チェッカーは、多数の簡単なプログラムを取り扱うことができるが、実際に関心のある多数のプログラムプロパティを決定できないので、幾つかの安全なプログラムが検証できないことになる。第２に、スタティックチェッカーは、プログラムは知っているが、その入力を知らないという点で、不完全な情報で実行する。スタティックチェックで得ることのできる最良の結果は、ある入力が非安全なアクションを生じるかどうか決定することである。この入力が実際に生じるかどうか決定することはできない。
【０００７】
[0007]リソース使用の面では、ダイナミックチェックは、プログラムの実行中にリソースマネージャーがチェックを遂行するプロセスを指し、一方、スタティックチェックは、プログラムの実行前にリソースマネージャーがチェックを実行するプロセスを指す。ダイナミックチェックは、融通性があるが、非効率的であり、一方、スタティックチェックは、効率的であるが、融通性がない。
【０００８】
[0008]プログラムにおいてリソース使用を推定することは、逐次コンピュータプログラムの実行時間を推定する問題と考えてもよい。実行時間それ自体は、各インストラクションの基本的消費が１であるリソースと考えることができる。これに対して、コンピュータプログラムのリソース使用は、プログラムの変数によりしばしばパラメータ化される。例えば、次のコード断片について考える。
for(i=0; i<n; ++i) {
//Write i bytes to file
file.write (buffer, i);
}
【０００９】
[0009]このコードに対する実行時間の問題は、トップレベルの“for”構成しか見ず、和
【数１】
2008519365.tif 000003
を分析しなければならない。これに対して、このプログラムのリソース使用を評価するために、和
【数２】
2008519365.tif 000004
が分析される。従って、実行時間の問題は、リソース使用問題の特殊なケースである。
【００１０】
[0010]スタティックリソースアカウンティングの更なる情報については、A. Ermedahl及びJ. Gustafsson著のDeriving Annotation for Tight Calculation of Execution Time、In Proceedings of Euro-Par’97、Vol. 1300 of Lecture Notesin Computer Science、第１２９８−１３０７ページ、１９９９年８月を参照されたい。
【００１１】
[0011]ダイナミックな解決策については、ダイナミックリソースモニタを使用して、全てのリソース使用を追跡するが、これは、非常に非効率的である。ダイナミックリソースアカウンティングの更なる情報については、C. Park及びA. Shaw著のExperiments with a Program Timing Tool Based on Source-level TimingSchema、IEEETransactions on Computers、２４：４８−５７、１９９１年５月を参照されたい。
【発明の概要】
【００１２】
[0012]制約を発生して解く方法及び装置がここに開示される。一実施形態では、この方法は、解かれない変数を有する１つ以上のダイナミックアノテーションを挿入することによりプログラムコードを変更するステップと、ベリファイアを使用してこの１つ以上のダイナミックアノテーションに基づき１つ以上の制約を発生するステップと、その１つ以上の発生された制約を解くステップと、解かれない変数を含むアノテーションに代わってダイナミックアノテーションを挿入することによりプログラムコードを変更するステップとを備えている。
【００１３】
[0013]本発明は、本発明の種々の実施形態についての以下の詳細な説明及び添付図面から更に完全に理解されるであろうが、本発明は、これら特定の実施形態に限定されるものではなく、これらは、単なる例示に過ぎない。
【本発明の詳細な説明】
【００１４】
[0030]安全でないコンピュータプログラムから安全なコンピュータプログラムを製作する方法及び装置を説明する。説明上、安全なプログラムとは、その振舞いが安全性ポリシーにより制約されたものである。安全性ポリシーとは、ダイナミックチェックを使用して実現できるポリシー、例えば、プログラムがランタイムライブラリーをいかに使用するかを制約するものである。本発明の実施形態は、多数の主たる効果を有する。第１に、１つ以上の実施形態は、他の解決策より効率的に安全なプログラムを製作する。第２に、１つ以上の実施形態は、多数の異なる安全性ポリシーを取り扱う。第３に、それが正しいことを証明するのが容易である。この方法は、コンピュータプログラムのリソース使用の安全性を保証すると共に、コンピュータプログラムのリソース使用を推定するために適用できる。
【００１５】
[0031]一実施形態において、プログラムは、プログラムにアノテーションを追加することにより安全なプログラムへと変更される。アノテーションは、スタティック及びダイナミックの両コンポーネントを有する分析の結果として追加される。
【００１６】
[0032]一実施形態では、ここに述べる技術は、４つのコンポーネント、即ちチェックインサータ、制約ジェネレータ、制約ソルバー及びチェックインスタンチエータを使用して実施される。チェックインサータは、安全でないプログラムを受け取り、そのプログラムにダイナミックチェックを追加する。これらのチェックは、まだ決定されていない変数を含む。制約ジェネレータは、チェックが追加されたプログラムを受け取り、チェックインサータにより追加された変数に基づいて１組の安全性制約を発生する。これらの制約は、プログラムの安全性にとって必要で且つ充分なものである。即ち、一実施形態では、プログラムは、制約が解ける場合及びその場合のみ安全である。制約ソルバーは、１組の安全性制約を受け容れ、チェックインサータにより生成された変数に対する値を決定する。チェックインスタンチエータは、制約ソルバーにより形成された解を受け入れて、それをプログラムのダイナミックチェックへ代入し、変数をもたない最終的な安全プログラムを作成する。この新たなプログラムは、セキュリティポリシーに違反する前に停止することを除いて、入力プログラムと同様である。従って、一実施形態では、プログラムの異なる部分に対する制約は、プログラムの計算構造を使用してスタティックに発生され、次いで、これらの制約を解いて、ダイナミックアノテーションをどこに入れるか決定する。
【００１７】
[0033]ここに述べる分析フレームワークは、多数のアプリケーションを有する。例えば、以下に述べるように、分析フレームワークは、リソース使用を推定し且つリソース使用の安全性を保証するために直接適用されるコンピュータプログラム用のアノテーションを決定することができる。このため、本発明の１つの実施形態は、ソース使用の推定に対して１つと、リソース使用の安全性に対して１つの、２つのアプリケーションプログラミングインターフェイス（ＡＰＩ）を備えている。一実施形態では、プラットホームの当該リソースが、プログラムインストラクションと実際の使用との間のマップであるリソースアカウンティングポリシーにより捕獲される。
【００１８】
[0034]又、分析のセマンティックスを保存する仕方でプログラムを変更することによりスタティックな分析を簡単化する技術も開示する。この技術は、ダイナミックアノテーション（例えば、ダイナミックチェック）をプログラムに追加する。一実施形態では、プログラムを評価する間に解かれる制約に基づいてプログラムにダイナミックチェックが追加される。解かれた制約は、アノテーションを挿入してプログラムを安全なものにすることができる。スタティックに解けない制約は、ダイナミックコールにより簡単化される。
【００１９】
[0035]以下の説明では、本発明をより完全に説明するために多数の細部について述べる。しかしながら、当業者であれば、これらの特定の細部を伴わずに本発明を実施できることが明らかであろう。他の例では、本発明を不明瞭にしないために、良く知られた構造及び装置は、詳細ではなく、ブロック図の形態で示す。
【００２０】
[0036]以下の詳細な説明のある部分は、コンピュータメモリ内のデータビットに対するオペレーションのアルゴリズム及び記号表示で表現する。これらのアルゴリズム記述及び表示は、データ処理技術の当事者が、それらの仕事の実体を他の当業者に最も効率的に伝達するために使用する手段である。アルゴリズムは、ここでは、一般的に、希望の結果を導くステップの自己一貫性のシーケンスであると考えられる。これらのステップは、物理量の物理的操作を要求するものである。通常、必ずしもそうでないが、これらの量は、記憶、転送、結合、比較、及びその他操作することのできる電気的又は磁気的信号の形態をとる。時々は、主として、共通使用の理由で、これらの信号を、ビット、値、エレメント、記号、キャラクタ、項、数字、等で示すのが便利であると分かっている。
【００２１】
[0037]しかしながら、これら及び同様の用語は、全て、適当な物理量に関連付けられるべきもので、且つそれらの量に適用される単なる便利な表示に過ぎないことを銘記されたい。特に指示のない限り、以下の説明から明らかなように、この説明全体にわたり、「処理」又は「コンピューティング」又は「計算」又は「決定」又は「表示」等の用語を使用する検討は、コンピュータシステムのアクション及び処理、或いは同様の電子的コンピューティング装置であって、コンピュータシステムのレジスタ及びメモリ内の物理的（電子的）量として表わされたデータを、コンピュータシステムのメモリ又はレジスタ、或いは他のこのような情報記憶、送信又は表示装置内の物理的量として同様に表わされる他のデータへと操作及び変換するものを指すことが明らかであろう。
【００２２】
[0038]又、本発明は、ここに述べるオペレーションを遂行するための装置にも係る。この装置は、要求される目的に対して特別に構成されてもよいし、或いはコンピュータに記憶されるコンピュータプログラムにより選択的にアクチベートされ又はコンフィギュレーションされる汎用コンピュータを備えてもよい。このようなコンピュータプログラムは、コンピュータ読み取り可能な記憶媒体、例えば、これに限定されないが、フロッピーディスク、光学ディスク、ＣＤ−ＲＯＭ、及び磁気−光学ディスクを含む任意の形式のディスク、リードオンリメモリ（ＲＯＭ）、ランダムアクセスメモリ（ＲＡＭ）、ＥＰＲＯＭ、ＥＥＰＲＯＭ、磁気又は光学カード、或いは電子的インストラクションを記憶するのに適していて、コンピュータシステムバスに各々結合される任意の形式の媒体に記憶されてもよい。
【００２３】
[0039]ここに述べるアルゴリズム及びディスプレイは、特定のコンピュータ又は他の装置に固有に関連したものではない。種々の汎用システムが、ここに述べる教示に基づくプログラムと共に使用されてもよく、又は必要な方法ステップを実行するために更に特殊な装置を構成するのが便利であると分かった。種々のこれらシステムに必要な構造は、以下の説明から明らかであろう。更に、本発明は、特定のプログラミング言語を参照して説明しない。ここに述べる本発明の教示を実施するのに種々のプログラミング言語を使用できることが明らかであろう。
【００２４】
[0040]マシン読み取り可能な媒体は、マシン（例えば、コンピュータ）で読み取り可能な形態で情報を記憶し又は送信するためのメカニズムを含む。例えば、マシン読み取り可能な媒体は、リードオンリメモリ（ＲＯＭ）、ランダムアクセスメモリ（ＲＡＭ）、磁気ディスク記憶媒体、光学記憶媒体、フラッシュメモリ装置、電気的、光学的、音響的又は他の形態の伝播信号（例えば、搬送波、赤外線信号、デジタル信号等）、等々を含む。
【００２５】
概略
[0041]例えば、安全性を確保する目的でプログラムにアノテーションを設けるためのここに述べる技術は、リソース使用、特に、リソース使用の推定に適用して以下に述べる。これらの技術は、他のアプリケーションにも適用できることが明らかであろう。
【００２６】
リソース使用の推定
[0042]一実施形態では、アノテーションフレームワークをリソース推定に適用するために、プログラムの異なる部分により消費されるリソースに対する制約が、プログラムの構造に対する誘導性を使用してスタティックに発生される。このプロセスは、コンピュータプログラムコードの一部分に対するリソース使用に適用する１つ以上のオペレーションを追加するためにコンピュータプログラムコードにアノテーションを設け、次いで、コンピュータプログラムコードのリソース消費を指示する１つ以上のオペレーションに基づいてコンピュータプログラムのリソース使用を決定することを含む。一実施形態では、コンピュータプログラムコードのリソース使用は、コンピュータプログラムコードの一部分のリソース消費を、コンピュータプログラムコードの一部分のコンポーネントのリソース消費に関連付ける１組の制約として決定される。又、このプロセスは、コンピュータプログラムコードの部分により消費されるリソースに対する制約を発生し、次いで、それら制約を解いて、コンピュータプログラムコードによるリソース使用を、コンピュータプログラムコードのリソース使用の決定の一部分として決定することも含む。一実施形態では、制約を解くことは、制約を規範的形態へと変換し、次いで、制約を知識ベースにおける１つ以上のエントリーに対して一致させることを含む。
【００２７】
[0043]一実施形態において、分析方法は、消費条件ジェネレータを使用して、任意の逐次コンピュータプログラムのリソース使用を決定する。一実施形態において、消費条件ジェネレータは、相互手順式の全プログラム計算を制約発生プロセスとして遂行して、制約を発生し、これら制約は、次いで、リソース使用を決定するために解かれる。より詳細には、消費条件ジェネレータは、プログラムにおける１組のスタティックアノテーションに対して動作し、スタティックアノテーションを自動的に計算する。スタティックアノテーションは、プログラマーにより与えられてもよい。
【００２８】
[0044]一実施形態において、基本的消費と、合成消費との２種類のアノテーションが使用される。基本的消費のアノテーションは、プログラムコマンドを、それらが使用するリソースへとマップする。合成消費のアノテーションは、ブロック、ループ、メソッドコール、及び他の複合プログラム構成に関連付けることができると共に、対応するプログラム構成に対するリソース使用表現である。一実施形態では、合成消費のアノテーションは、各コマンドのリソース使用を、コマンドに生じるローカル及びグローバル変数に関して表現する。消費条件ジェネレータは、プログラム構成に対する合成消費がそのコンポーネントの基本的消費の和を境界定めするところのプロパティを捕獲する。消費条件ジェネレータにより発生された制約は、全プログラム、或いは当該ブロック、メソッド、ループ又は複合コマンドに対する合成消費表現について解くのに使用される。更に、一実施形態では、消費条件ジェネレータにより発生された制約を満足するリソース使用表現は、プログラムのリソースニーズを満足することが保証される。
【００２９】
[0045]制約発生プロセスは、ダイナミックアノテーションを配置する望ましい粒度について適用することができる。一実施形態では、これらの制約は、規範的形態への簡単化を使用すると共に、（制約、解）テンプレート対の知識ベースに対して一致させることで、解かれる。
【００３０】
[0046]リソース使用推定のための技術は、多数の形式のリソースに適用されてもよく、そして例えば、メモリ、ディスク、スレッド等の明示的リソース、及び例えば、実行時間及びエネルギー（例えば、ＣＰＵインストラクションカウントに基づく）のような暗示的リソースに対してインスタンス生成することができる。
【００３１】
[0047]ここに述べるリソースアカウンティングプロセスは、プログラムのリソース使用を推定することが有用な全てのエリアにアプリケーションを有する。それらは、例えば、リアルタイムプログラムスケジューリング及び推定（生の）、並びに任意コードのリソース使用安全性を含むが、それらに限定されない。
【００３２】
スタティック分析の簡単化
[0048]スタティック分析は、解けない制約に代わってダイナミックチェックを追加することにより簡単化されてもよい。一実施形態では、簡単化されたスタティック分析は、１つ以上のアノテーションを有するプログラムコードを受け取り、次いで、解かれない制約に対応するアノテーションに代わってダイナミックアノテーションを挿入することでプログラムコードを変更することを含む。ダイナミックアノテーションは、プログラムコードへのダイナミックコールを含んでもよい。この変更は、チェックのセマンティックを保存しながら行われる。一実施形態では、アノテーションは、プログラムコードのリソース使用を評価するときに制約を解くことからの結果に基づいてプログラムリソース使用の安全性を高めるためにプログラムコードに挿入される。このプロセスは、繰り返し実行することができる。
【００３３】
[0049]より詳細には、プログラムを評価しながら制約を解くよう試みた後に、１つ以上の解けない制約を識別してもよい。例えば、プログラムのリソース使用を評価するときに、解けない制約が識別されてもよい。このようなケースでは、それらの制約がダイナミックチェックに置き換えられる。このように、スタティック及びダイナミックコンポーネントが一緒に結合される。従って、一実施形態では、困難なスタティック問題は、それらをダイナミックエバリュエータへ委ねることにより排除されてもよい。
【００３４】
[0050]一実施形態では、この方法は、所与のプログラムが、決められたリソース使用表現により境界定めされたことを検証するのに使用される。一実施形態では、フィードバックチャンネルを分析に使用して、スタティックに解けない制約を指示する。これらの制約は、ダイナミックを使用して簡単化されて、解くことのできるより簡単な制約となる。
【００３５】
リソース使用の安全性に対する自動アノテーション
[0051]一実施形態では、リソース使用の安全性のためにプログラムに自動的にアノテーションを設けることができる。これは、任意の逐次コンピュータプログラムにおいてリソース使用安全性のスタティック検証を許すＡＰＩを使用してダイナミックアノテーションを追加することで行うことができる。このような場合には、上述したリソース推定及びスタティック分析簡単化のための分析方法を使用して、安全性が直接暗示されるリソース推定の適切さを保証するリソース使用ＡＰＩでプログラムに自動的にアノテーションを設けることができる。従って、自動アノテータが健全であり、即ち自動的にアノテーション付けされたプログラムがリソース使用の安全性についてスタティックベリファイアをパスする。一実施形態では、この自動アノテーションプロセスは、コンピュータプログラムコードのリソース使用を評価し、そしてコンピュータプログラムコードのリソース使用の評価結果に基づいてリソース使用安全性のためにコンピュータプログラムコードに１つ以上のオペレーションを挿入することによりコンピュータプログラムにアノテーション付けすることを含む。一実施形態では、コンピュータプログラムコードに１つ以上のオペレーションを挿入することは、コンピュータプログラムコードのリソース使用の評価結果に基づいてリソース使用安全性のために１つ以上のリソース消費制約を除去することを含む。これらのオペレーションは、解かれない制約（項）に対応する１つ以上のリソース消費制約を所定値（例えば、ゼロ）にセットして、リソース使用の安全性を達成する消費オペレーションでよい。
【００３６】
アーキテクチャーの概略
[0052]リソース使用に適用されるアーキテクチャーの実施形態を以下に説明する。ここに述べる技術の他のアプリケーションも存在することに注意されたい。
【００３７】
[0053]図１Ａは、安全でないプログラムを受け容れて、安全なプログラムを発生するトップレベルアーキテクチャーの一実施形態を示すブロック図である。上述したように、安全なプログラムとは、その振舞いが安全性ポリシーにより制約を受けるものである。このポリシーは、プログラムが使用するリソースに対する限界を指定する。これらのリソースは、例えば、ネットワーク、ディスク、及びＣＰＵを含むことができると共に、プロセス、スレッド及びハンドルのような他の仮想リソースも含むことができる。又、このポリシーは、プログラムがライブラリーファンクション（又はメソッド）をコールできるところの条件も指定する。これらの条件は、関数の引数、及びコールが生じるときのプログラムの状態の両方を含んでもよい。例えば、プログラムは、ある方向にファイルをオープンすることはできるが、他の方向にはオープンできず、又、Ｉ／Ｏライブラリーが初期化された場合しかオープンできなくてよい。
【００３８】
[0054]図１Ａのシステムは、安全でないプログラムから安全なプログラムを作成することができる。図１Ａを参照すれば、このシステムは、制約ジェネレータ１０２及び制約ソルバー１０３の２つのサブシステムを備えている。安全でないプログラム１０１は、制約ジェネレータ１０２へ入力される。制約ジェネレータ１０２は、安全でないプログラム１０１に対する制約を発生する。制約ソルバー１０３は、制約を解き、安全なプログラム１０４を作成する。
【００３９】
[0055]図１Ｂは、図１Ａのシステムにより遂行されるプロセスの一実施形態を示すフローチャートである。このプロセスは、ハードウェア（例えば、回路、専用ロジック、等）、ソフトウェア（汎用コンピュータシステム又は専用マシンで実行されるような）、又はその両方の組み合せを含む処理ロジックにより遂行することができる。
【００４０】
[0056]図１Ｂを参照すれば、プロセスは、コンピュータプログラムの部分のリソース使用に関連した１つ以上のオペレーションでコンピュータプログラムにアノテーション付けすることにより開始される（処理ブロック１３１）。プログラムにアノテーション付けした後に、処理ロジックは、コンピュータプログラムに対するリソース使用制約を発生する（処理ブロック１３２）。リソース使用を評価した後に、プロセスは、１つ以上の解かれない項を有する１つ以上の制約を識別する（処理ブロック１３３）。次いで、処理ロジックは、コンピュータプログラムによるリソース使用の評価結果に応答して１つ以上の取得オペレーションをコンピュータプログラムに挿入し、解かれない項に対応する１つ以上のリソース消費制約を、リソース使用安全性を達成するようにセットする（処理ブロック１３４）。
【００４１】
[0057]図２は、安全でないプログラムを受け容れて、安全なプログラムを発生する安全プログラムジェネレータの一実施形態を示すブロック図である。図２を参照すれば、プログラム及び安全性制約がシステムにより受け取られる。一実施形態では、発生される制約は、プログラムの安全性にとって必要で且つ充分なものであり、即ちプログラムは、制約を解ける場合及びその場合にのみ安全である。一実施形態では、制約が変数を含み、そして制約を満足させる変数の値が存在する場合及びその場合にのみ、制約を解くことができる。この状態は、ｘ２≦１０のような代数式を解くことに類似している。
【００４２】
[0058]安全性制約を伴うプログラムは、アノテータにより発生することができる。一実施形態では、アノテータは、２段階で動作する。第１段階では、アノテータは、各関数ｆのリソース消費に対する整数変数ｆｃ、ｆがコールされる条件に対するブール変数ｆ＿ｐｒｅ、及びｆが復帰する条件に対するブール変数ｆ＿ｐｏｓｔを生成する。これら変数は、全て、ｆに対する引数及びプログラム状態に依存し得るので、説明上、次のように書き表される。
【数３】
2008519365.tif 000005
第２段階では、アノテータは、ｆがコールされるときにｆ＿ｐｒｅが真であり、ｆが復帰するときにｆ＿ｐｏｓｔが真であり、且つｆは、ｆｃ以下のリソースを使用しそしてそれらを抽象的リソース使用アノテーションとして追加することを示す各関数の前(pre)及び後(post)条件を生成する。次いで、検証条件ジェネレータ（ＶＣＧ）は、変数ｆ＿ｐｒｅ、ｆ＿ｐｏｓｔ及びｆｃに関する制約を発生する。従って、ＶＣＧは、その解が安全な値を含む制約を発見する。
【００４３】
[0059]制約ソルバー２０４は、プログラムにおける制約を解く。チェックインスタンチエータ２０５は、抽象的リソースアノテーションを、変数を伴わない具体的アノテーションに置き換える。チェックインスタンチエータ２０５の出力は、安全なプログラム２０６である。
【００４４】
[0060]図３は、制約ソルバーにより遂行されるプロセスの一実施形態を示すフローチャートである。図３を参照すれば、制約ソルバーは、プログラム及び１組の安全性制約３０１を受け容れ、そして制約違反を回避することを除いて古いプログラムに非常に良く似た新たな安全なプログラム３０６を作成する。一実施形態において、これは、先のものを停止し、そして「制約違反を回避するためにストップする」等のエラーメッセージを発行することにより達成される。エラーメッセージは、プログラムが続く場合に、おそらく安全性制約の１つに違反し得ることを信号することができる。このようなケースでは、プログラムの実行は、このエラーを発生しない場合には続行であるが、エラーを発生する場合にはフェイルする。プログラムの実行が続く場合には、入力制約の違反が生じないことが保証される。しかしながら、フェイルの場合にも、実際に違反した制約がないことが考えられる。即ち、制約ソルバーは、保守的であって、たとえ違反が実際に生じなくてもストップすることが許される。一実施形態では、振舞いが保守的である。というのは、違反が生じる正確な条件を決定することが非常に困難なことがあり、且つ最大セットの実行を許すより違反を防止する方が重要だからである。
【００４５】
[0061]図３を参照すれば、制約ソルバーの処理ロジックは、プログラム及び安全制約３０１の制約が解けるときを決定する（処理ブロック３０２）。次いで、制約ソルバーの処理ロジックは、プログラム及び１組の制約の両方を変更する（処理ブロック３０３）。一実施形態では、処理ロジックは、制約を簡単化して解き易くするようにプログラムを変更する。より詳細には、処理ロジックは、制約を検査することによりプログラムをどのように変更するか決定し、制約が解ける場合には、制約ソルバーの処理ロジックは、制約を解き（処理ブロック３０４）、そしてプログラムの変数をインスタンス生成する（処理ブロック３０５）。これにより、安全なプログラム３０６が得られる。
【００４６】
[0062]ある制約は、プログラムの振舞いが任意に複雑になり得るので、解くことが非常に困難なことがある。一実施形態では、制約ソルバーは、複雑な振舞いを除外することで制約を簡単化する。
【００４７】
[0063]一実施形態では、プログラムは、あるライブラリー関数のコール慣習に違反した場合及びその場合にのみ安全でない。即ち、プログラムは、関数の前条件に違反するか、或いは不充分なリソースでライブラリー関数をコールする。一実施形態では、制約ソルバーは、ライブラリー関数への各コールの直前にダイナミックチェックを入れる。このような制約ソルバーは、最大セットの安全な実行を許す。というのは、安全でない実行を正確にストップするからである。
【００４８】
[0064]一実施形態では、この制約ソルバーは、ライブラリー関数への各コールの前に、又は少なくとも、セキュリティポリシーにより制約を受けたライブラリー関数への各コールの前に、ダイナミックチェックを導入する。別の実施形態では、制約ソルバーは、方程式を解くのにより多くのインテリジェンスを使用できる場合には、より少数のダイナミックチェックを導入する。例えば、制約ソルバーは、ある前条件が全ての実行において満足され、実際にチェックが必要とされないことを実現してもよい。
【００４９】
例示的自動リソースアカウンティングアーキテクチャー
[0065]図４Ａは、リソース使用推定のためのプロセスの一実施形態を示すフローチャートである。このプロセスは、ハードウェア（例えば、回路、専用ロジック、等）、ソフトウェア（汎用コンピュータシステム又は専用マシンで実行されるような）、又はその両方の組み合せを含む処理ロジックにより遂行することができる。
【００５０】
[0066]図４Ａを参照すれば、このプロセスは、コンピュータプログラムの一部分に対するリソース使用に関連した１つ以上のオペレーションを追加するようにコンピュータプログラムにアノテーション付けする処理を行うことにより開始される（処理ブロック４３１）。アノテーション付けの後に、処理ロジックは、１組の制約を１つ以上の不等式として発生し、そのプログラムによるリソース消費をコンピュータプログラムの関連部分の消費に関連付ける（処理ブロック４３２）。これら制約に伴い、処理ロジックは、それら制約を規範的形態へ変換し、知識ベースにおける１つ以上のエントリーに対してそれら制約を一致させることで、コンピュータプログラムによるリソース使用を決定するように１組の制約を解く（処理ブロック４３３）。次いで、処理ロジックは、１組の制約の規範的形態における１つ以上の解かれない制約に対応するコンピュータプログラムにおける１つ以上のアノテーションを排除する（処理ブロック４３４）。
【００５１】
[0067]図４Ｂは、リソース使用推定のためのプロセスの一実施形態を示す詳細なフローチャートである。このプロセスは、ハードウェア（例えば、回路、専用ロジック、等）、ソフトウェア（汎用コンピュータシステム又は専用マシンで実行されるような）、又はその両方の組み合せを含む処理ロジックにより遂行することができる。
【００５２】
[0068]図４Ｂを参照すれば、アノテーションインサータ４０１は、プログラム４１０（例えば、ソース、２進）及びリソースアカウンティングポリシー４１１を受け取り、そしてそれに応答して、アノテーション付けされたプログラム４１２を発生する。同じプログラムのリソース消費は、それが実行されているプラットホームに依存してもよく、この依存性は、リソースアカウンティングポリシー４１１を使用して捕獲される。一実施形態では、リソースアカウンティングポリシー４１１は、コマンドの消費が明示的となるように、アカウンティングＡＰＩを使用してプログラム４１０に最初にアノテーション付けするのに使用される。従って、このようなケースでは、アノテーションインサータ４０１は、ポリシーベースのアノテーションを遂行する。
【００５３】
[0069]制約ジェネレータ４０２は、アノテーションプログラム４１２を受け取り、プログラムのリソース消費を１組の制約４１３として捕獲し、これら制約は、アノテーション付けされたプログラム４１２におけるブロック又はメソッドの消費を、他の関数又はブロックを含み得るそのコンポーネントの消費に関連付けるものである。この解決策を使用してループも取り扱うことができる。というのは、ループの消費は、ループの１つの非ローリングの消費を、そこから反復を生じるループの消費に追加したものとして表現できるからである。一実施形態では、これら制約の形態は、等式でも不等式でもよい。等式は、リソース消費関数の変数のドメインにおける異なる範囲に対してリソース消費を正確に捕獲することができる。不等式は、リソース消費に対する緊密な上限を与え、条件付きのケースのように単一の表現を伴う複数の経路にわたる消費を近似する上で助けとなる。
【００５４】
[0070]制約キャノニカライザー(canonicalizer)４０５は、制約ジェネレータ４０２により発生された１組の等式を受け取り、これら等式は、解かねばならないメソッド、ブロック及びループ消費に対応する項を含む。一実施形態では、特定の項を解くために、その特定の項に関連した最小組の等式が得られるように全ての等式が制約キャノニカライザー４０３により編成される。このプロセスは、規範化(canonicalization)と称され、一実施形態では、標準的な固定点スタイルの消費を含む。制約キャノニカライザー４０３は、１組の規範的制約４０４を出力する。
【００５５】
[0071]一実施形態では、制約ソルバー４０４は、キャノニカライザー４０３から出力された１組の規範的制約４０４を、解知識ベース４１５からの入力と共に受け取り、それに応答して、１組の規範的等式４１４における反復を識別すると共に、それらを１組のヒューリスティックに対して一致させる。一実施形態では、ヒューリスティックは、特定クラスの反復に対して考えられる最も一般的な形態で指定され、従って、ターゲットプログラムに対する特定インスタンスでヒューリスティックをインスタンス生成するために単一化が必要とされる。一致オペレーションの結果は、解かれる項に対する閉じた形態の解であり、これは、関数、ブロック、ループ又は全プログラムのリソース消費となり得る。制約ソルバー４０４の出力は、解かれた／部分的に解かれた制約４１６と、解かれない制約４１７である。
【００５６】
[0072]アノテーションエリミネータ４０５は、解かれた／部分的に解かれた制約４１６に基づいてアノテーション付きプログラム４１２のアノテーション排除を遂行する。より詳細には、制約の解は、プログラムの異なる領域に対応する異なるコマンドのリソース使用のスタティックな推定を完全に又は部分的に容易にする。アノテーションエリミネータ４０５は、解かれないコア制約と、それに対応するプログラムの領域とを識別して、プログラムのそれら部分から消費アノテーションを排除する。その結果、アノテーションエリミネータ４０５は、部分的に評価されたプログラム４１８を出力する。一実施形態では、部分的に評価されたプログラム４１８は、最小数のダイナミック消費アノテーションを含む。
【００５７】
[0073]部分的に評価されたプログラム４１８は、リソースをカウントすることにより部分的に評価されたプログラム４１８のリソース使用４３０を決定するダイナミックリソースカウンタ４０７により受け取られる。
【００５８】
[0074]一実施形態では、制約シンプリファイア４０６は、解かれない制約４１７を再使用すると共に、ダイナミックコストを使用して、スタティック分析の結果を簡単化する。一実施形態では、スタティック分析は、知識ベースにおいて得られる制約の解により制限される。発生される制約は、プログラムに入れられるダイナミックアノテーションの引数に関連する。特定のダイナミックアノテーションに対して発生される制約が解けない場合には、コードの対応部分に実際のダイナミックコールを挿入することにより制約を弱めることも考えてもよい。この弱められた制約は、スタティックな知識ベース４１５における制約／解の対に対して一致させて、制約に代わってプログラムに挿入すべきダイナミックコール（アノテーション）を得、簡単化された全組の制約を生じさせてもよい。一実施形態では、このフィードバックプロセスは、もはや制約が残らなくなるまで繰り返される。このプロセスは、解かれない全ての制約がダイナミックアノテーションの挿入により排除されるために終了することに注意されたい。
【００５９】
例示的言語及びポリシー使用
[0075]一実施形態では、リソースアカウンティング手順を説明するために、簡単な必須のプログラミング言語を使用して、整数値での計算を遂行する。ある任意の単位で量を測定する１つの当該リソースがあると仮定すれば、コマンドｃｏｎｓｕｍｅ  Ｅを使用して、Ｅ単位のリソースをダイナミックに使用するオペレーションがモデリングされ、ここで、Ｅは、言語での表現である。一実施形態では、リソースアカウンティングは、関数コールのレベルで遂行され、コマンドｒｕｎ＿ｃｏｎｓＥｆ（→ｘ）を使用して、ｆ（→ｘ）内のリソース使用のスタティック評価がモデリングされ、ここで、Ｅは、一般に、→ｘに依存する。
【００６０】
[0076]図５は、全言語定義を標準的なバッカス−ナール記法で示す。変数ｘが整数値しかとらないと仮定すれば、表現ｃｏｎｄ（ｂ、ｅ１、ｅ２）は、ブール表現ｂが値真を有する場合には値ｅ１を有し、さもなければ、値ｅ２を有する。命題接続∧、∀、⇒は、良く知られた意味を有する（任意の入門テキストに見られるような）。コマンドｃａｌｌ  ｆ（→ｘ）は、引数→ｘで関数ｆへのコールを捕獲する。関数は、次の仕様で定義される。
ｄｅｆ  ｆ（→ｘ）  ｂｅｇｉｎ  ｃ  ｅｎｄ  ｒｕｎ＿ｃｏｎｓ（ｅ）
【００６１】
[0077]この言語では、スタティックアカウンティングＡＰＩ、ｒｕｎ＿ｃｏｎｓ、は、関数にアノテーションを付けるためにのみ使用されることに注意されたい。手でアノテーションが付けられたプログラムは、ｒｕｎ＿ｃｏｎｓを非制約形態で使用してもよいが、位置実施形態の自動アカウンティング手順は、それを関数定義ポイントに導入するだけである。アカウンティング手順により発生される制約は、ｒｕｎ＿ｃｏｎｓアノテーションがプログラムのどこに存在するかに依存する。１つの目標は、全プログラムの消費を解くことであるから、これらのアノテーションは、一実施形態では、関数境界にしかない。
【００６２】
[0078]同じプログラムに対するリソースの使用は、プラットホームに依存してもよく、この依存性は、均一な仕方で指定されてもよい。一実施形態では、所与のプログラムを実行するエージェントに対するリソースアカウンティングポリシー（ＲＡＰ）は、基本的コマンドと当該リソースの単位との間のマップを指定する。一般に、ＲＡＰは、コマンドに対するリソース表現を指定し、これは、コマンドにおける自由変数を指してもよい。我々の言語に対する基本的コマンドは、スキップ、割り当て、及び関数コールを含む。図６は、読み取りディスクリソースに対するリソースアカウンティングポリシーの一実施例を示す。
【００６３】
[0079]リソースアカウンティング手順における第１ステップは、非アノテーション付きプログラムを取り上げ、そしてリソースアカウンティングポリシーを使用してそれを変換することである。変換されたプログラムは、各コマンドに対する既知の基本的消費アノテーションと、各関数定義に対する（まだ知られていない）スタティック合成消費とを含む。一実施形態では、変換は、次のルールに基づいて遂行され、そしてコマンドの構造に対して誘導的に遂行される。又、メインプログラムを含む全ての関数の本体に対してアノテーションが遂行されることにも注意されたい。
第１に、基本的なケースでは、単純なコマンド（スキップ、割り当て、関数コール）の前に、リソースアカウンティングポリシーにより指定される消費ｅステートメントがある。第２に、各合成コマンド（シーケンシング、条件付き、間に(while)、及び関数定義）は、合成コマンドのコンポーネントコマンドに変換を順次に適用することにより繰り返し処理される。コマンドｃ１；ｃ２ and if ｂthen ｃ１ else ｃ２の場合には、コンポーネントコマンドがｃ１及びｃ２であり、そしてコマンドwhile ｂ do ｃ and run_cons ｅｆ（→ｘ）begin ｃ endの場合には、コンポーネントコマンドがｃである。
【００６４】
[0080]アノテーションインサータの一実施形態を、図７のフローチャートを参照して説明する。リソースアカウンティングポリシーは、コマンドとリソース表現との間のマップｐとして表わされることに注意されたい。
【００６５】
[0081]リソースアカウンティングポリシー及び初期アノテーションプロセスは、両方とも、プログラム内で定義される関数に対して消費アノテーションを含むように拡張できることに注意されたい。このケースにおいて、一実施形態では、これら関数の定義がアノテーションプロセスから省略され、それらの使用は、ＲＡＰで与えられる情報を使用して基本的消費アノテーションでアノテーション付けされる。
【００６６】
例示的消費制約ジェネレータ
[0082]アノテーションを遂行した後に、アノテーション付きプログラムから制約が発生される。図８及び９は、消費条件ジェネレータ（ｃｃｇ）の一実施形態を示す。多くのケースでは、関数がコード及びフローチャートの両方の形態で表わされる。全てのケースにおいて、２つの形態は同等である。
【００６７】
[0083]消費条件ジェネレータ（ｃｃｇ）は、コマンドのシンタックスにおいて反復することで定義される。コマンドｃ、プログラム状態ｓ、及び１組の制約Ｔが与えられると、ｃｃｇ（ｃ、ｓ、Ｔ）は、状態ｓでスタートしたときにコマンドｃにより消費されるリソースに関する新たな制約を生成する。初期状態ｓ０でスタートする全プログラムの使用を決定するために、オリジナルプログラムがトップレベルのメイン関数内にラップされ、ｃｃｇ（メイン、ｓ０）により発生される制約をスタティックに解く。
【００６８】
[0084]状態ｓでスタートしたときにコマンドｃにより消費されるリソースの量は、Ｃ（ｃ、ｓ）で表わされる。ｃｃｇは、プログラムの異なるコマンドに対してマップＣの値についての制約を発生する。Ｃコマンドは、スタティックに完全に定義できるので、制約は、Ｃ（ｃ、ｓ）のできるだけ多数のインスタンスについて解かれ、そしてそれらをメソッドに対するスタティックなｒｕｎ＿ｃｏｎｓアノテーションに含む。
【００６９】
制約の簡単化
[0085]制約発生プロセスの一実施形態の目標は、全プログラムに対してｒｕｎ＿ｃｏｎｓをスタティックに評価することである。このプロセスの第１ステップは、初期状態を与えたプログラムの制御流路に実際に存在するコマンドｃに対してＣ（ｃ、ｓ）だけが解かれるように１組の制約を簡単化することである。一実施形態では、このプロセスに対してスタティック排除及び置き換えの２つの部分がある。
【００７０】
[0086]スタティック排除では、例えば、ブールテストの値をスタティックに決定し、そして採用されない岐路により発生される制約を排除することができてもよい。
【００７１】
[0087]置き換えでは、ｃｃｇにより発生される制約が、方向付けリライトシステムとして編成される。ｃｃｇにより発生される各制約は、左から右へと方向付けされ、基本的コマンドに関するコマンドの消費を表現する。トップレベルの制約は、全プログラムの消費を記述する。ｘに対する制約がｙに関して与えられると、ｙに対する制約が変数ｚしか指さない場合に、ｘは、ｚに関して直接的に表現される。このプロセスは、トップレベルの制約に対して行うべき置き換えがもはやなくなるまで、繰り返される。
【００７２】
[0088]図１０Ａは、制約を簡単化するプロセスの一実施形態のフローチャートである。図１０Ａのプロセスは、ハードウェア（例えば、回路、専用ロジック、等）、ソフトウェア（汎用コンピュータシステム又は専用マシンで実行されるような）、又はその両方の組み合せを含む処理ロジックにより遂行することができる。
【００７３】
[0089]図１０Ａを参照すれば、このプロセスは、コンピュータプログラムによるリソース使用を表わす規範的形態のリソース制約を解くことにより、コンピュータプログラムを実行する前にコンピュータプログラムに対してスタティック分析を遂行することで、処理ロジックにより開始される（処理ブロック１０３１）。次いで、処理ロジックは、１つ以上の解かれない項を有する１つ以上の制約を識別する（処理ブロック１０３２）。１つ以上の解かれない項を有する１つ以上の制約を使用して、処理ロジックは、排除することで１つ以上の制約を最大限簡単化するところの解かれない項のうちの１つの項を識別する（処理ブロック１０３３）。この識別プロセスの後に、処理ロジックは、コンピュータプログラムにおけるダイナミックオペレーションのスタティック尺度を、リソース使用に対応するダイナミックオペレーションに置き換えることで、１つの項を排除する（処理ブロック１０３４）。
【００７４】
[0090]図１０Ｂは、制約を規範的形態へと簡単化するプロセスの一実施形態を示すフローチャートである。図１０Ｂのプロセスは、ハードウェア（例えば、回路、専用ロジック、等）、ソフトウェア（汎用コンピュータシステム又は専用マシンで実行されるような）、又はその両方の組み合せを含む処理ロジックにより遂行することができる。図１０Ｂを参照すれば、プロセスは、処理ロジックが制約マップを発生することで開始する（処理ブロック１００１）。制約マップ１００１を使用して、処理ロジックは、解かれた制約があるかどうかテストする（処理ブロック１００２）。解かれた制約がある場合には、処理ロジックは、解かれない制約に代入することで解かれた制約を排除し（処理ブロック１００３）、次いで、プロセスは、処理ブロック１００４へ移行する。
【００７５】
[0091]プロセスは、解かれない制約があるかどうか処理ロジックが決定することで継続する（処理ブロック１００４）。もしなければ、処理ロジックは、解かれた制約を出力する（処理ブロック１００５）。解かれない制約がある場合には、処理ロジックは、アウトデグリー(outdegree)１をもつノードがあるかどうかテストする（処理ブロック１００６）。これらのノードについては、簡単な代入により子ノードを親ノードへ折り返すことができる。このようなノードがある場合には、処理ロジックは、親への代入によりこのようなノードを排除する（処理ブロック１００７）。もしそうでなければ、処理ロジックは、規範化された制約を出力する（処理ブロック１００８）。
【００７６】
制約を解く
[0092]代入及び排除により発生される制約は、解かれた制約を生じさせるか、又は制約における異なる変数間に反復のシステムを生じさせる。発生される反復の複雑さは、オリジナルプログラムの制御流に依存し、特定の形態であると仮定することができない。従って、これらの反復は、反復等式に対する一般解形態のライブラリーに対して一致させることにより解かれる。クライアントは、任意のサイズの解ライブラリーを選択することができる。多数の異なるプログラムテンプレートを捕獲するライブラリーは、プログラムにおけるリソース消費の良好なスタティック推定を許す。一例として、ｗｈｉｌｅコマンドを以下に考える。
i：＝0；
while（i＜10）do
consume（i）；
i：＝i＋1
【００７７】
[0093]前記コマンドから発生された簡単化された制約は、この全コマンド（例えば、ｃ）の消費をｗｈｉｌｅループｃｗの消費に関して記述する（Ｃ(ｉ：＝ｉ＋１)＝０）であることを想起されたい）。
Ｃ(ｃ、ｉ)＝Ｃ(ｃｗ、ｉ)
Ｃ(ｃｗ、ｉ)＝cond(ｉ＿１０、０、ｉ＋０＋Ｃ(ｃｗ、ｉ＋１))
【００７８】
[0094]ｗｈｉｌｅループに対する消費表現は反復性であり、ライブラリーがそれに対して一般的な表現を含むと仮定することに注意されたい。この表現が次のループの消費に対応すると仮定する。
while(i<c) do
consume (a.i + b);
i：＝c.i＋d
【００７９】
[0095]前記ループから発生される制約は、次の通りである。
Ｃ(ｃ０ｗ、ｉ)＝cond(ｉ＿ｃ、０、ａ．ｉ＋ｂ＋Ｃ(ｃｗ、ｃ．ｉ＋ｄ))
【００８０】
[0096]この制約に対する解は、最も一般的な形態でＣ(ｃ０ｗ、ｉ)＝Ｓ(ｉ、ｃ、ａ、ｂ、ｃ、ｄ)として指定される。２つの制約を一致させるために、セット単一化に対して標準的なアルゴリズムを使用し、次いで、解を制約としてオリジナルセットに追加する。
【００８１】
[0097]このプロセスは、１組の制約における全ての反復に対して繰り返される。いずれのパターンに対しても一致し得ない反復は、手をつけないままとされる。このプロセスの終りに、若干の解かれないＣ(s、ｃ)が残され、これらは、ダイナミックリソースカウンティングに対応する。
【００８２】
[0098]図１１は、制約を解くためのプロセスの一実施形態のフローチャートである。このプロセスは、ハードウェア（例えば、回路、専用ロジック、等）、ソフトウェア（汎用コンピュータシステム又は専用マシンで実行されるような）、又はその両方の組み合せを含む処理ロジックにより遂行することができる。図１１を参照すれば、このプロセスは、処理ロジックが規範化された制約を受け取ることで開始する（処理ブロック１１０１）。規範化された制約を使用して、処理ロジックは、残される前に試みられなかった解かれない制約の変数があるかどうかテストする（処理ブロック１１０２）。残される前に試みられなかった解かれない制約の変数がある場合には、処理ロジックは、変数が現われる制約を収集し（処理ブロック１１０３）、次いで、制約セットが既知のベースと一致するかどうかテストする（処理ブロック１１０４）。もしそうでなければ、制約は、知識ベースに一致するメソッドを使用して解くことができず、プロセスが退出となる。もしそうであれば、処理ロジックは、知識ベースの解に一致代入を適用し（処理ブロック１１０５）、そして制約変数に対する解を使用して残りの制約を規範化する（処理ブロック１１０６）。その後、処理は、処理ブロック１１０２へ移行し、プロセスが繰り返される。
【００８３】
ダイナミック消費オペレーションの排除
[0099]このプロセスにおける次のステップは、初期アノテーションに導入されてスタティック計算によりカバーされた全てのダイナミック消費を排除する。制約における解かれないＣ(ｃ、ｓ)は、プログラムの一部分（最終的にはプログラム全体）であるコマンドをリソース消費に対してスタティックに解けないようにする。しかしながら、リソース消費が決定されたシンタックスツリーの部分を、各メソッドにおいてｒｕｎ＿ｃｏｎｓスタティックアノテーションへ収集する。従って、次のことが遂行される。
１．簡単化された制約に対応する方向グラフからスタートして、解かれた制約に対応するノードが解の表現に置き換えられる。
２．これらの表現は、より高いレベルのノードへの繰り返し代入のプロセスにより折り重ねられる。
３．制約に対する解を伴う最終的なグラフが与えられると、最低レベルのノードが選択される。これらのノードに対応するコマンドは、ダイナミックに決定されるコストを有する。次いで、前記コマンド内に現われるものを除いて、全ての消費コマンドがプログラムから排除される。
【００８４】
[00100]図１２は、リソースアカウンティングがスタティックに遂行されたアノテーションを排除するためのプロセスの一実施形態を示すフローチャートである。このプロセスは、ハードウェア（例えば、回路、専用ロジック、等）、ソフトウェア（汎用コンピュータシステム又は専用マシンで実行されるような）、又はその両方の組み合せを含む処理ロジックにより遂行することができる。図１２を参照すれば、このプロセスは、処理ロジックが解かれない制約マップを受け取ることで開始する（処理ブロック１２０１）。解かれない制約グラフを使用して、処理ロジックは、解かれない制約グラフにリーフノードのリストを生成する（処理ロジック１２０２）。次いで、処理ロジックは、未処理のリーフノードが更にあるかどうかテストする（処理ブロック１２０３）。もしなければ、処理が終了となる。もしあれば、処理ロジックは、このノードに関連したプログラムの領域をマークし（処理ブロック１２０４）、次いで、そのマークされたコード領域に対する消費アノテーションを排除し（処理ブロック１２０５）、そしてプロセスは、処理ブロック１２０３へ移行し、処理が繰り返される。
【００８５】
制約シンプリファイア
[00101]次いで、制約簡単化の一実施形態が遂行される。一実施形態において、使用するプロセスは、次の通りである。第１に、各々の解かれない制約は、ダイナミックアノテーションに関連した項を含む表現を右手側に有する。サブ項のセットを排除するために排除命令が選択される。例えば、１つの排除命令は、単一のサブ項を最初に探索し、次いで、サイズ２のサブ項セットを探索し、等々、とすることができる。第２に、各排除されるサブ項セットに対して、得られた制約が知識ベースに対して一致される。一致がない場合には、プロセスは、次の候補排除に対する排除命令を使用して続けられる。一致がある場合には、排除されるサブ項セットが、発生された解と同様に記録される。第３に、首尾良い一致の中で、最も多項式的複雑さの解が選択される。これは、排除できた最も困難なサブ項に対応する。第４に、排除されたサブ項は、アノテーションエリミネータへ送られ、簡単化された制約は、制約ソルバーへ返送される。次いで、フィードバックループが同じ手順を繰り返す。
【００８６】
[00102]この一般的スタティック分析簡単化技術は、ダイナミックオペレーションがスタティック分析の結果をキャッシュ記憶できるＡＰＩに適用可能である。更に、ダイナミックオペレーションは、自己組み合せの方法を受け容れ、即ち特定のダイナミックオペレーションが２つ以上のダイナミックオペレーションの組み合せと同等であることをスタティックに保証することができる。
【００８７】
[00103]従って、リソース使用安全性のためにプログラムにアノテーション付けする技術が開示された。以下の効果の１つ以上は、本発明の実施形態に関連している。プログラムに対して示されるリソース境界は、効率的に検証することができる。この技術は、アノテーション付けされたコード及びアノテーション付けされないコードの両方に作用し、プログラムのリソース使用を指定する上でプログラマーに融通性を与える。一実施形態では、消費定数ジェネレータにより発生される制約は、条件の異なる岐路のようなプログラムの異なる部分における使用を結合し易くする不等式の形態である。更に、ここに導入するアノテーションは、性能を著しく損なうことなくリソース使用推定の精度を与えるためにスタティック分析及びダイナミックリソース監視の結合を許す。加えて、ここに述べるスタティック分析は、ループにおけるリソース使用の緊密な上限を推測する。更に、一実施形態では、これら技術は、逐次コンピュータプログラムにおける制御構造に関して定義され、従って、バイトコードからソースまでの言語のスペクトルにわたって適用することができる。又、一部分として実行される分析は、相互手順式であり、そして発生されるリソース表現は、最も一般的な形態、即ち関連するグローバル、ローカル及び関数パラメータに関するものである。
【００８８】
例示的コンピュータシステム
[00104]図１３は、ここに述べる１つ以上のオペレーションを遂行することのできる例示的コンピュータシステムのブロック図である。図１３を参照すれば、コンピュータシステム１３００は、例示的クライアント又はサーバーコンピュータシステムを含むことができる。コンピュータシステム１３００は、情報を通信するための通信メカニズム又はバス１３１１と、情報を処理するためにバス１３１１に結合されたプロセッサ１３１２とを備えている。プロセッサ１３１２は、マイクロプロセッサを含み、これは、例えば、Ｐｅｎｔｉｕｍ（登録商標）、ＰｏｗｅｒＰＣ（登録商標）、Ａｌｐｈａ（登録商標）、等のマイクロプロセッサであるが、これに限定されない。
【００８９】
[00105]システム１３００は、更に、プロセッサ１３１２により実行されるべきインストラクション及び情報を記憶するためにバス１３１１に結合されたランダムアクセスメモリ（ＲＡＭ）又は他のダイナミック記憶装置１３０４（メインメモリと称される）を備えている。このメインメモリ１３０４は、プロセッサ１３１２によるインストラクションの実行中に一時的変数又は他の中間情報を記憶するのに使用されてもよい。
【００９０】
[00106]又、コンピュータシステム１３００は、プロセッサ１３１２のインストラクション及びスタティック情報を記憶するためにバス１３１１に結合されたリードオンリメモリ（ＲＯＭ）及び／又は他のスタティック記憶装置１３０６と、磁気ディスク又は光学ディスク及びそれに対応するディスクドライブのようなデータ記憶装置１３０７も備えている。このデータ記憶装置１３０７は、情報及びインストラクションを記憶するためにバス１３１１に結合される。
【００９１】
[00107]更に、コンピュータシステム１３００は、コンピュータユーザに情報を表示するためにバス１３１１に結合された陰極線管（ＣＲＴ）又は液晶ディスプレイ（ＬＣＤ）のようなディスプレイ装置１３２１に結合されてもよい。又、プロセッサ１３１２へ情報及びコマンド選択を通信するために、アルファニューメリック及び他のキーを含むアルファニューメリック入力装置１３２２をバス１３１１に結合してもよい。付加的なユーザ入力装置は、方向情報及びコマンド選択をプロセッサ１３１２へ通信すると共に、ディスプレイ１３２１上のカーソル移動を制御するためにバス１３１１に結合されたマウス、トラックボール、トラックパッド、スタイラス、又はカーソル方向キーのようなカーソル制御器１３２３である。
【００９２】
[00108]バス１３１１に結合できる別の装置は、インストラクション、データ又は他の情報を、ペーパー、フィルムのような媒体、又は同様の形式の媒体にプリントするのに使用できるハードコピー装置１３２４である。更に、スピーカ及び／又はマイクロホンのような音響記録及び再生装置を、コンピュータシステム１３００との音響インターフェイスのためにバス１３１１に任意に結合することができる。バス１３１１に結合できる別の装置は、電話又はハンドヘルドパルム装置に通信するためのワイヤード／ワイヤレス通信能力１３２５である。
【００９３】
[00109]システム１３００及び関連ハードウェアのコンポーネントのいずれか又は全部を本発明に使用できることに注意されたい。しかしながら、コンピュータシステムの他の構成では幾つか又は全ての装置を含んでもよいことが明らかであろう。
【００９４】
[00110]当業者であれば、以上の説明を読んだ後に、本発明の多数の変更や修正が疑いなく明らかとなろうが、図示して説明した特定の実施形態は、本発明を何らそれに限定するものではないことを理解されたい。それ故、種々の実施形態の細部にわたる言及は、本発明の本質と考えられる特徴のみを記載した特許請求の範囲を限定するものではない。
【図面の簡単な説明】
【００９５】
【図１Ａ】安全なプログラムを安全でないものから製作できるシステムを示す図である。
【図１Ｂ】図１Ａのシステムにより遂行される処理の一実施形態を示すフローチャートである。
【図２】安全でないプログラムを受け入れて、安全なプログラムを製作するシステムの一実施形態を示すブロック図である。
【図３】制約ソルバーの一実施形態のフローチャートである。
【図４Ａ】リソース使用推定のためのプロセスの一実施形態を示すフローチャートである。
【図４Ｂ】リソース使用推定のためのプロセスの一実施形態を示す詳細なフローチャートである。
【図５】例示的な全言語定義をバッカス−ナール記法で示す図である。
【図６】読み取りディスクリソースのためのリソースアカウンティングポリシーの一実施例を示す図である。
【図７】アノテーション挿入プロセスの一実施形態を示すフローチャートである。
【図８】消費制約発生のための例示的コードを示す図である。
【図９】消費制約発生を遂行するためのプロセスの一実施形態を示すフローチャートである。
【図１０Ａ】制約を規範的形態へ簡単化するための一般的プロセスの一実施形態を示すフローチャートである。
【図１０Ｂ】制約を規範的形態へ簡単化するためのプロセスの一実施形態を示すフローチャートである。
【図１１】制約を解くためのプロセスの一実施形態を示すフローチャートである。
【図１２】リソースアカウンティングがスタティックに実行されたアノテーションを排除するためのプロセスの一実施形態を示すフローチャートである。
【図１３】ここに述べる１つ以上のオペレーションを遂行できる例示的コンピュータシステムのブロック図である。
【符号の説明】
【００９６】
１０１・・・安全でないプログラム、１０２・・・制約ジェネレータ、１０３・・・制約ソルバー、１０４・・・安全なプログラム、１３０４・・・メインメモリ、１３０６・・・スタティック記憶装置、１３０７・・・データ記憶装置、１３１２・・・プロセッサ、１３１１・・・バス、１３２１・・・ディスプレイ装置、１３２２・・・アルファニューメリック入力装置、１３２３・・・カーソル制御装置、１３２４・・・ハードコピー装置、１３２５・・・通信能力
【図１Ａ】
2008519365.tif 000006
【図１Ｂ】
2008519365.tif 000007
【図２】
2008519365.tif 000008
【図３】
2008519365.tif 000009
【図４Ａ】
2008519365.tif 000010
【図４Ｂ】
2008519365.tif 000011
【図５】
2008519365.tif 000012
【図６】
2008519365.tif 000013
【図７】
2008519365.tif 000014
【図８】
2008519365.tif 000015
【図９】
2008519365.tif 000016
【図１０Ａ】
2008519365.tif 000017
【図１０Ｂ】
2008519365.tif 000018
【図１１】
2008519365.tif 000019
【図１２】
2008519365.tif 000020
【図１３】
2008519365.tif 000021
【国際調査報告】
2008519365.tif 000022
2008519365.tif 000023
2008519365.tif 000024