experiment の設計

設計目標

ベンチマークは、同じものを計算するはずの実装同士を比較します。experiment は「同じ」が何を意味するかを定め(オラクル)、失敗をデバッグできるほど小さくし(縮小)、サイズに依存する優位性がデプロイの規則になるほど強いのはいつかを判断します(クロスオーバー分析)。すべては明示的な入力の純粋関数です。

数学的背景

関係としてのオラクル

入力 xx とステップ kk について、参照オラクルは期待される結果 ek(x)e_k(x) と、実際の結果 aa に対する判定 V(x,k,e,a)∈ValidationStatusV(x, k, e, a) \in \text{ValidationStatus} を定義します。等価性は V=Valid  ⟺  a=eV = \text{Valid} \iff a = e という特別な場合です。浮動小数点のコードには通常許容誤差 ∣a−e∣≤ϵ\lvert a - e\rvert \le \epsilon が必要で、IEEE を考慮したコードはフラグも比較します。

関係オラクルは実装のペア R(x,k,a(i),a(j))R(x, k, a^{(i)}, a^{(j)}) を判定します。参照は不要ですが、検出できるのは不一致だけです。すべての実装が同じバグを共有していれば、関係は成り立ってしまいます。ランナーは mm 個の実装の順序なしペア (m2)\binom{m}{2} 個をすべて検査します。関係が同値関係(例えば結果の完全一致)である場合、ペアは冗長ですが安価であり、1 つだけ逸脱した実装は m−1m-1 個のペアに現れるため、容易に特定できます。

貪欲な降下としての縮小

C(x)C(x) を xx の候補、PP を失敗の述語とします。shrink は次を計算します

x0=x,xj+1=first y∈C(xj) with P(y),x_0 = x, \qquad x_{j+1} = \text{first } y \in C(x_j) \text{ with } P(y),

そして、PP を満たす候補がなくなるか、PP を max_steps 回評価した時点で止まります。

  • 停止性。 内側のループの各反復は PP を 1 回評価してカウンタを増やします。外側のループは、カウンタが max_steps に達するか、ある反復で何も受理されなかったときに止まります。CC が巡回していても、評価は最大 max_steps 回です。
  • 不変条件。 P(x0)P(x_0) が成り立つなら、受理されたすべての xjx_j について P(xj)P(x_j) が成り立ちます。候補は PP が成り立つ場合にのみ受理されるからです。したがって結果はなお失敗する入力です。(shrink は x0x_0 自体は検査しません。)
  • 局所最小性。 失敗する候補がなくなったためにループが止まった場合、結果は局所最小です。C(result)C(\text{result}) のどの要素も PP を満たしません。予算のために止まった場合は、そうとは限りません。

C(n)=[⌊n/2⌋,n−1]C(n) = [\lfloor n/2\rfloor, n-1] と閾値の述語 P(n)=(n≥t)P(n) = (n \ge t) では、降下は可能な限り半分にし、その後 1 ずつ下がり、O(log⁡n+t)O(\log n + t) 回の受理ステップでちょうど tt に到達します。

クロスオーバーの検出

s1<s2<⋯<sNs_1 < s_2 < \dots < s_N をソート済みのスケール、ℓi∈{A,B,Unknown}\ell_i \in \{A, B, \text{Unknown}\} を sis_i における判定とします。遷移の数は次のとおりです

T=∣{ i∈{2,…,N}:ℓi−1≠ℓi, ℓi−1≠Unknown, ℓi≠Unknown }∣.T = \bigl\lvert\{\, i \in \{2, \dots, N\} : \ell_{i-1} \ne \ell_i,\ \ell_{i-1} \ne \text{Unknown},\ \ell_i \ne \text{Unknown} \,\}\bigr\rvert .

相対差 r(s)r(s) がスケールについて単調であれば、ラベル label(r(si))\text{label}(r(s_i)) は単調な系列 A…A U…U B…BA \dots A\, U \dots U\, B \dots B(またはその逆)をなすため、素直な優位性には遷移が高々 1 つしかありません。T=1T = 1 なら唯一の遷移の境界 (si−1,si)(s_{i-1}, s_i) が得られます。T>1T > 1 は優位性が 2 回以上反転し、1 つの閾値では表現できないことを意味します。T=0T = 0 は、確定的で互いに異なるラベルの隣接ペアがないことを意味します。

comparator_label(r, t) は stats と同じ閾値規則で相対差をラベルに写します。r≤−tr \le -t なら AA、r≥tr \ge t なら BB、それ以外は Unknown です。幅 2t2t の Unknown 帯により、r=0r = 0 付近のノイズが見かけ上の遷移を生むことを防ぎます。

設計上の決定

オラクルは値である

問題。 各ケースには独自の正しさの概念が必要です。選択。 オラクルは ID を持つ関数のレコードです。理由。 許容誤差やコンテキストを捕捉でき、すべての検証イベントで名前が示され、その場で構築できます。

オラクルに届くのは値だけでなく結果

オラクルは ExecutionOutcome を受け取るため、文書化された ExpectedDifference を受け入れたり、発生したフラグを比較したり、両側がトラップすることを要求したりできます。ランナーはオラクルを呼び出す前に、ワーカーのクラッシュ、タイムアウト、デコードエラー、Unsupported を事前に分類するため、オラクルは本物の結果だけを判定します。

貪欲で最初に改善したものを採る縮小

選択肢。 失敗する最小の入力の全探索、デルタデバッギング、貪欲な降下。選択。 明示的な候補関数と評価予算を伴う貪欲な降下。理由。 各評価は操作系列全体を実行しうるため、コストを抑えるのは予算です。候補関数により、ユーザーは入力の構造(サイズを半分にする、要素を取り除く)を表現できます。受理されたパスは記録されるため、読み手は反例にどうたどり着いたかを確認できます。

保守的なクロスオーバー

問題。 クロスオーバーは、一度も計測されていない入力にも適用されるデプロイの規則(DeploymentPolicy::Piecewise)になります。選択。 遷移がちょうど 1 つの場合にのみ境界を受け入れ、それ以外は NonMonotonic を報告してポリシーはユーザーに委ねます。理由。 ノイズが多く反転する優位性から作った規則は、ノイズを符号化することになるからです。

正しさと不変条件

  • shrink は述語を最大 max_steps 回評価し、最初の入力が述語を満たすなら、必ず述語を満たす入力を返します。
  • crossover_from_labels は遷移がちょうど 1 つの場合にのみ Found を返し、その境界はその遷移の隣り合う 2 つのスケールからなります。
  • ReferenceOracle::equal は、比較関数が受け入れた 2 つの Value 結果に対してのみ Valid を返します。
  • comparator_label は t>0t > 0 のとき、実数直線を (−∞,−t](-\infty, -t]、(−t,t)(-t, t)、[t,∞)[t, \infty) に分割します。

採用しなかった代替案

  • 生の計時値に対する統計的な変化点検出。 ノイズモデルが必要です。実用的な閾値に基づくラベルは説明可能です。
  • 境界を補間する。 計測された 2 つのスケールの間のスケールは計測されていません。代わりに、結果は計測された 2 つのスケールを示します。
  • デルタデバッギング。 系列に対しては強力ですが、固定された入力表現が必要です。候補関数の方がより汎用的です。

境界

  • crossover_from_labels はドメインをソートせず、ScaleDomain.compare も使いません。ソート済みの値を渡してください。
  • Unknown ラベルをまたぐ遷移(A, Unknown, B)は数えられないため、そのような系列は NoCrossover を報告します。
  • オラクルはここでは実行されず、ランナーが実行します。ReferenceOracle.sequence_length はランナーでは使われません。
  • shrink は最初の入力が失敗することを検査しません。