testfloat_expr_cli の設計

設計目標

1 つの TestFloat ベクタファイルを、それが生成されたときとまったく同じ構成で 1 プロセスごとに実行します。これによりツールは、何億ものベクタを有限サイズのファイルと並列プロセスに流し込めます。

数学的背景

TestFloat のタスクは組(形式、演算、丸め、極小性、厳密性、レベル、シード)です。そのベクタは testfloat_expr の設計の合格規則で検査されます。タスクのベクタストリームをチャンク V1,V2,…V_1, V_2, \dots に分け、各チャンクをさらにシャードに分けることはベクタの分割であり、各ベクタの判定は他と独立しているため、タスクのカウンタはチャンクとシャードにわたる和になります。

設計上の判断

構成はオプションで、ベクタはそのまま

関数、丸め、極小性、厳密性は、testfloat_gen 自身のフラグに対応するコマンドラインオプションです。ベクタファイルは TestFloat の形式のまま保たれるため、生成器の出力をファイルにパイプし、変換なしで実行できます。

呼び出しごとに 1 ファイル

1 つのプロセスが 1 つのチャンクを処理します。Python のドライバ(tools/run_binfloat_interpreter.py)は生成器のストリームをチャンクファイルに書き出し、各ファイルに対してランナーを実行し、報告された FUNCTION:LINE の id にチャンクのオフセットを加えます。チャンクのサイズを有界にすることで、最大の mulAdd タスクでもメモリ使用量が一定に保たれます。

JSON とシャードの共有オプション

--json とシャードオプションは internal/runner_cli に由来するため、GDA ランナーとまったく同じように動作します。

正しさ/不変条件

  • 選択されたベクタがどれも失敗しなかったとき、かつそのときに限り終了コードは 0 です。selectedCases = passedCases + failedCases。
  • 仕様のエラー(TestFloatSpec::parse)または解析エラーの場合は、どのベクタも実行される前に 2 で終了します。

却下した代替案

  • 構成をベクタファイルに符号化する。 TestFloat の出力を書き換える必要が生じます。
  • MoonBit から testfloat_gen を実行する。 プロセス管理はツール側の責務です。ランナーは移植可能かつテスト可能なままにします。

境界

  • ベクタの生成、チャンク分割、id の再マッピングは行いません(Python ツール)。
  • 形式と演算は frontend/testfloat_expr のものです。