Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

第38章. キャリブレートされたWCETとコストモデル

この章の目的

この章を読み終える頃には、ワーストケース実行時間がどう計上されるか、そしてホストが自分のハードウェアにキャリブレートされた数字をどう得るかが分かるようになります。この章を読み終える頃には、ワーストケース実行時間がどう計上されるか、そしてホストが自分のハードウェアにキャリブレートされた数字をどう得るかが分かるようになります。

コストモデル

第20章のWCET解析は、2つのyieldの間の最も長いパスでの仕事量を数えます。命令の数をサイクル数に変えるには、コストモデルを参照します — 各オペコードにパイプライン化サイクルのコストを割り当てる表と、値スロットのサイズです。第20章のWCET解析は、2つのyieldの間の最も長いパスでの仕事量を数えます。命令の数をサイクル数に変えるには、コストモデルを参照します — 各オペコードにパイプライン化サイクルのコストを割り当てる表と、値スロットのサイズです。

ランタイムはNOMINAL_COST_MODELを提供しています。そのコストは推定値であって、測定値ではありません — データの移動に1サイクル、算術に2、除算に3、複合構築に5、関数呼び出しに10、です。名目モデルは1つのプラットフォーム上で2つのプログラムを比較するには健全ですが、その数字は特定のプロセッサのサイクル数ではありません。ランタイムはNOMINAL_COST_MODELを提供しています。そのコストは推定値であって、測定値ではありません — データの移動に1サイクル、算術に2、除算に3、複合構築に5、関数呼び出しに10、です。名目モデルは1つのプラットフォーム上で2つのプログラムを比較するには健全ですが、その数字は特定のプロセッサのサイクル数ではありません。

測定されたモデル

本物のデプロイメントプロセッサにキャリブレートされたWCETの数字が必要なホストは、測定されたコストモデルを使います。ワークスペースメンバーのkeleusma-benchは、各オペコードをターゲット上でベンチマークし、生成されたMEASURED_COST_MODEL断片を出力します。ホストは自分のターゲット用の断片をインクルードし、WCET APIの_with_cost_modelバリアントにモデルを渡します。本物のデプロイメントプロセッサにキャリブレートされたWCETの数字が必要なホストは、測定されたコストモデルを使います。ワークスペースメンバーのkeleusma-benchは、各オペコードをターゲット上でベンチマークし、生成されたMEASURED_COST_MODEL断片を出力します。ホストは自分のターゲット用の断片をインクルードし、WCET APIの_with_cost_modelバリアントにモデルを渡します。

#![allow(unused)]
fn main() {
include!(concat!(env!("CARGO_MANIFEST_DIR"),
    "/measured_cost_models/aarch64_apple_darwin.rs"));

use keleusma::verify::wcet_stream_iteration_with_cost_model;

let cycles = wcet_stream_iteration_with_cost_model(chunk, &MEASURED_COST_MODEL, &[])?;
}

keleusma-benchクレートは、新しいターゲット用の断片を生成するキャプチャワークフローを文書化しています。keleusma-benchクレートは、新しいターゲット用の断片を生成するキャプチャワークフローを文書化しています。

ネイティブ関数の計上

WCETとWCMU解析は、デフォルトではネイティブ関数呼び出しのコストをゼロとして計上します。検証器はホストのRustコードの中を見られないからです。健全な境界が必要なホストは、解析が走る前にネイティブごとのコストを宣言します。WCETとWCMU解析は、デフォルトではネイティブ関数呼び出しのコストをゼロとして計上します。検証器はホストのRustコードの中を見られないからです。健全な境界が必要なホストは、解析が走る前にネイティブごとのコストを宣言します。

#![allow(unused)]
fn main() {
vm.set_native_bounds("math::sin", 25, 0)?;
vm.set_native_bounds("text::upper", 100, 256)?;
}

最初の数字はネイティブのワーストケースパイプライン化サイクルコスト、2番目はそのワーストケースのアリーナヒープ割り当て、バイト単位です。これらはホストの誓いです。検証器は宣言された値を独立に測定せずに受け入れるので、ホストがその正確さに責任を負います。測定するか、ネイティブの有界解析を行うか、です。最初の数字はネイティブのワーストケースパイプライン化サイクルコスト、2番目はそのワーストケースのアリーナヒープ割り当て、バイト単位です。これらはホストの誓いです。検証器は宣言された値を独立に測定せずに受け入れるので、ホストがその正確さに責任を負います。測定するか、ネイティブの有界解析を行うか、です。

その数字の意味

解析が出す境界はパイプライン化サイクル単位、仕事量の単位です。それをデプロイメントプラットフォーム上の実時間秒数に変換するには、キャッシュとパイプラインのストールとクロック周期を勘案する、プラットフォーム特有の係数が必要です。言語はパイプライン化サイクル境界を保証します。ホストは自分のハードウェアに対する変換係数を誓います。この責任の分割は第20章で説明したのと同じもので、ここではホスト側から見ています。解析が出す境界はパイプライン化サイクル単位、仕事量の単位です。それをデプロイメントプラットフォーム上の実時間秒数に変換するには、キャッシュとパイプラインのストールとクロック周期を勘案する、プラットフォーム特有の係数が必要です。言語はパイプライン化サイクル境界を保証します。ホストは自分のハードウェアに対する変換係数を誓います。この責任の分割は第20章で説明したのと同じもので、ここではホスト側から見ています。

この章のまとめ

  • コストモデルはオペコードにパイプライン化サイクルコストを割り当て、解析はそれを使ってWCETの数字を生みます。コストモデルはオペコードにパイプライン化サイクルコストを割り当て、解析はそれを使ってWCETの数字を生みます。
  • NOMINAL_COST_MODELは未測定で相対比較に良く、keleusma-benchから得るMEASURED_COST_MODELはターゲットにキャリブレートされています。NOMINAL_COST_MODELは未測定で相対比較に良く、keleusma-benchから得るMEASURED_COST_MODELはターゲットにキャリブレートされています。
  • set_native_boundsはネイティブ関数のコストを誓うので、解析が計上できます。set_native_boundsはネイティブ関数のコストを誓うので、解析が計上できます。
  • 境界はパイプライン化サイクル単位です。実時間に変換するのはホストの責任です。境界はパイプライン化サイクル単位です。実時間に変換するのはホストの責任です。

次の章では完全なホストを最初から最後まで歩きます。