Timsort アルゴリズムと Yutu 月面探査車のバグを見つけるにはどうすればよいでしょうか?

0×00 背景

形式手法は、私たちのほとんどにとっては非常に高度なものです。せいぜい授業で聞いたことがある程度で、実際の仕事でそれを使用する人はほとんどいません。

[[131154]]

少し前、Reddit の投稿により、人気のない形式手法が話題になりました。その内容は、海外の技術チームが Java のいくつかのソート アルゴリズムの正しさを形式手法で検証したのですが、Timsort ソート アルゴリズムの検証中にバグを発見したというものです。その後、彼らはそのバグを Java オープンソース コミュニティに報告し、形式手法で検証された修復ソリューションを提供しました。ハッピーエンドになるはずだったが、Java オープンソース コミュニティは修正を採用せず、別の汚い解決策を採用した... (私はとても意地悪なので、あなたの言うことは聞きません。同意しないなら噛み付いてきてください)

バグ自体に戻って、形式手法がどのように使用されるかを見てみましょう。

0×01 ティムソートとは

ソートといえば、バブル ソート、選択ソート、挿入ソート、そしてもちろん魔法のクイック ソートの方が馴染み深いでしょう。では、ティムソートとはいったい何なのでしょうか?

Timsort アルゴリズムは、2002 年に Tim Peters 氏によって提案されたソート アルゴリズム (彼自身の名にちなんで命名されました) であり、他のソート アルゴリズムと比較して注目されています。ソートアルゴリズムの品質はさまざまな側面から評価します。次の図をご覧ください。

他の面倒なソートアルゴリズムについては見ません (私も理解していません…)、馴染みのあるソートアルゴリズムを見てみましょう。クイックソートの平均時間計算量は非常に優れていますが、最適および最悪の時間計算量とアルゴリズムの安定性の点では、Timsort ほど優れていません。

そのため、Timsort は Python の組み込みソート アルゴリズムとなり、その後、Java SE 7、Android、GNU Octave ではすべて Timsort ソート アルゴリズムが導入されました。

では、なぜこのような優れたアルゴリズムにバグがあるのでしょうか? もちろん、これは Timsort アルゴリズムの問​​題ではなく、プログラマーのミスです。その理由は、Timsort が (他のアルゴリズムと比較して) 複雑すぎることと、プログラマーがうっかり特別な状況を見落としたことです...

このバグの原因を理解するために、まず Timsort アルゴリズムの原理を見てみましょう。

0×02 ティムソート原理

簡単に言えば、Timsort はマージ ソートと挿入ソートを組み合わせたハイブリッド アルゴリズムです。これは、現実のほとんどのデータが部分的に順序付けられている (昇順または降順) という単純な事実に基づいています。

ティムソートソートアルゴリズムは、配列内の順序付けられたフラグメントをランとして定義し、各ランは単調増加または厳密に単調減少である必要があります（アルゴリズムの安定性を確保するため）。次の図を参照してください。

いくつかの詳細はさておき、Timsort ソート アルゴリズムは次の 2 つのステップに要約できます。

最初のステップは、ソートする配列をランに分割することです。もちろん、ランは短すぎてはなりません。長さが minrun しきい値よりも短い場合は、挿入ソートを使用して拡張されます。

2番目のステップは、ランをスタックにプッシュすることです。スタックの一番上のランの長さが以下の制約のいずれにも当てはまらない場合、

1. 実行長さ[n-2] > 実行長さ[n-1] + 実行長さ[n]
2. 実行長さ[n-1] > 実行長さ[n]

次に、マージ ソートを使用して 2 つの最短実行を新しい実行にマージし、スタックが空になったときにソートが完了します。

以下は、これを説明するための例です。この例では、minrun=4 を設定しています。これは、実行の最小長さが 4 未満になることができないことを意味します。実行が分割されるたびに、次の図に示すようにスタックにプッシュされます。

この時点では、スタックの一番上の実行は、runLen[0] < runLen[1] であるため制約条件を満たしていないため、2 つの実行をマージする必要があることに注意してください。もちろん、このプロセスではマージ ソートが使用されます。

順序付けられたセグメントの長さがminrunより短い場合は、次の図に示すようにパディングする必要があります。

#p#

スタックの最上位の実行は、この時点で制約 (10 > 5 + 4、5 > 4) を満たしているため、マージは不要であることに注意してください。

最後に、配列要素の数が minrun より少ないため、run としてのみ使用できます。

この時点で、スタックの一番上の実行は制約 5 < 4 + 2 を満たさなくなったため、マージする必要があります。その後のプロセスは下の図の通りです。

これでソート処理は完了です。なぜこのような奇妙な制約があるのか​​と疑問に思う生徒もいるかもしれません。スタックに何かをプッシュするたびに、マージしてソートするだけではだめなのでしょうか。これは主にマージ ソートの効率によるもので、長いシーケンスと短いシーケンスをマージしてソートするのは、効率とコストの観点から費用対効果が高くないためです。長さのバランスが取れた 2 つのシーケンスをマージしてソートする方が合理的で効率的です。

もちろん、ここでは minrun の長さの計算や、挿入ソートとマージソートの特定の実装におけるいくつかのテクニックなど、多くの詳細を無視しました。 Timsortソートアルゴリズムの詳細については、OpenJDKのソースコードTimSortを参照してください。

0×03 ティムソートのバグ

Timsort アルゴリズムのプロセスと原理を理解すると、論理的な問題はないように思えます。では、このバグは正確にはどこにあるのでしょうか?

このバグはまさにその制約で発生します。なぜなら、Timsort アルゴリズムは、マージ ソート中に 2 つのサブシーケンスの長さが均等になるようにこの制約を設定するからです。暗黙の意味は、スタック内のすべての実行がこの制約を満たす必要があるということです (スタックの先頭でなくても)。つまり、2 <= i <= StackSize-1 も満たされる必要があります。

1. runLen[i-2] > runLen[i-1] + runLen[i]
2. 実行長さ[i-1] > 実行長さ[i]

JDKソースコード内のコメントでもこのことが説明されている。

/**
 * マージ待ちの実行スタックを調べ、隣接する実行をマージします
 * スタック不変条件が再確立されるまで:
 *
 * 1. runLen[i - 3] > runLen[i - 2] + runLen[i - 1]
 * 2. runLen[i - 2] > runLen[i - 1]
 *
 * このメソッドは、新しい実行がスタックにプッシュされるたびに呼び出されます。
 * したがって、不変条件はi < stackSizeの場合に成立することが保証されます。
 * メソッドへのエントリ。
 */
プライベートボイドマージコラプス() {
  スタックサイズが1より大きい場合
    int n = スタックサイズ - 2;
    (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1]) の場合 {
      （実行長さ[n - 1] < 実行長さ[n + 1]）の場合
         n--;
      マージAt(n);
    } そうでない場合 (runLen[n] <= runLen[n + 1]) {
      マージAt(n);
    } それ以外 {
      break; // 不変条件が確立される
    }
  }
}

ほとんどの場合、スタックの上位 3 つの実行のみがこの制約を満たしているかどうかを確認するだけで、スタック全体のすべての実行がこの制約を満たしていることを確認できます。しかし、次のスタック（スタックの一番上が右側にある）のような特殊なケースでは機能しません。

120、80、25、20、30

上記のソースコードによれば、25 < 20 + 30、25 < 30なので、2つの実行25と20がマージされ、スタック内の状況は次のようになります。

120、80、45、30

80 > 45 + 30、45 > 30 なので制約条件が満たされ、マージは終了します。しかし、スタック内の他の実行、120 < 80 + 45 に注意してください。これは制約を満たしていません。スタックの一番上の実行のみを判断するため、ここには「隠れた危険」があります。

ほとんどの場合、この問題は大きな問題ではなく、通常のソート操作には影響しません。これは、それほど多くのデータがなく、上記の状況が大量に発生することはないためです。しかし、この海外の技術チームは配列を慎重に構築し、Timsort アルゴリズムに java.lang.ArrayIndexOutOfBoundsException エラーを報告させることに成功しました。このエラーを再現するコードもGitHubに掲載されています。こちらをクリックしてください。

なぜこのような奇妙なエラーが発生するのでしょうか? これは、Timsort アルゴリズムの Java 実装で要求されるスタック領域のサイズに関係しています。元のコードを見てみましょう。

int スタック長さ = (長さ < 120 ? 5 :
                長さ < 1542 ? 10 :
                長さ < 119151 ? 19 : 40);
runBase = 新しいint[stackLen];
runLen = 新しいint[stackLen];

ここで、len は入力配列の長さを表し、stackLen は要求されたスタックのサイズを表します。では、上記の境界条件と奇妙な数値はどのように計算されるのでしょうか?#p#

実は、とても簡単です。次の質問を考えてみましょう。各要素がティムソートアルゴリズムの制約を満たすようなシーケンスを構築するにはどうすればよいでしょうか。シーケンスの要素をE(n)とします。E(n) = E(n-1) + E(n-2) + 1が満たされている限り、問題ありません。これはフィボナッチ数列と非常によく似ています。プログラムで実装してみましょう。

# -*- コーディング: utf-8 -*-
# スタックの一番上に補助的な空の実行を追加し、スタックの一番上の実行の長さを minrun=16 に設定します。
既知 = {0: 0, 1: 16}
def fib(n):
    nが既知の場合:
        既知を返す[n]
    res = fib(n - 1) + fib(n - 2) + 1
    既知[n] = res
    戻り値
ns = [5,10,19,39,40]
n が ns の場合:
    フィブサム = 0
    iが範囲(n)内にある場合:
        フィブサム += フィブ(i)
    "n={0},sum={1}"を出力します。format(n,fibsum)
# 出力 # n=5,sum=119
# n=10、合計=1541
# n=19、合計=119150
# n=39、合計=1802926565
# n=40、合計=2917196495
# ps: Java の int の最大値は 2147483648 です。1802926565 < 2147483648 < 2917196495

では、なぜ 4 つの間隔だけが選択されるのでしょうか。なぜ minrun=16 が選択されるのでしょうか。個人的には、十分なスタック スペースがある限り、トラブルを回避するためだと思います。

ただし、これは理想的な条件下であるため、スタック内のすべての実行がこの制約を満たす必要があることに注意してください。先ほど反例を示しました。反例が発生すると、使用されるスタック サイズは予想よりも大きくなります。

この外国の技術チームは論文の中で最悪のスタックサイズを計算し、表を作成した。

2 行目は最悪の場合に必要なスタックのサイズを示し、3 行目は Timsort アルゴリズムによって実際に与えられたスタック サイズを示します (上記の JDK ソース コードを参照)。興味深いことに、配列の長さが 65536 の場合、Java の Timsort は最初にスタックの長さを 19 に設定しましたが、後で誰かがバグを報告しました。つまり、このバグは実際に発生したことになります。しかし、Javaオープンソースコミュニティのプログラマーはこのバグの根本原因を突き止めることができなかったため、表面的に問題を解決するしかありませんでした。その後のアップデートで、スタックサイズは24に変更されました...（ただし、問題は解決しました）しかし、隠れた危険性はまだ存在しています。配列の長さが67108864の場合、最悪の場合に使用されるスタックサイズは41であり、JavaでTimsortによって設定された長さは40であることがわかります。したがって、配列が慎重に構築されている限り、このバグがトリガーされる可能性があります。しかし、この記事の冒頭で述べたように、Java オープンソース コミュニティのプログラマーは依然としてこの問題を根本的に解決しておらず、スタック サイズを増やすという古い方法を使い続けています... (私にはこのスキルしかありません。同意できないなら、私に噛み付いてきてください)

0×04 このバグを発見する方法

このバグは非常にわかりにくく、非常に創造的な思考を持たない限り、コードから問題を解明できる人はほとんどいません。テストはどうでしょうか? 実現可能ではないようです。自動生成されたテスト セットに頼って、このバグをトリガーできる配列を生成するのは難しいようです (特に配列が長い場合)。チームは、このバグに関する詳細な調査に基づいて、バグをトリガーできる配列も構築しました。ここで、古い疑問に戻ります。プログラムの正しさをどのように証明するか。プログラムを 10,000 回または 100 万回エラーなしで実行しても、プログラムに問題がないということではありません (さまざまな種類の脆弱性を参照してください)。テスト セットでは、すべての実行パスがカバーされていることを保証できないためです。プログラムの正しさを証明するには、他の手段を使用する必要があります。

これには形式手法の使用が必要です。実際、プログラムの正しさの証明に関する研究は、チューリングとフォン・ノイマンの時代から始まっています。もちろん、この理論を本当にマスターするには、論理と計算に関する膨大な知識が必要です（プログラム仕様、事前アサーション、事後アサーション、とにかく、私にはわかりません）...この海外の技術チームが形式ツール KeY を使用して Timsort アルゴリズムを検証する方法を見てみましょう。

KeYはJavaプラットフォーム用に設計されたプログラムの正当性証明ツールです。Javaモデリング言語(JML)を使用して、プログラムに次のようなアサーションを追加します。

/*@ プライベート normal_behavior
  @ 必要
  @ n >= MIN_MERGE;
  @保証します
  @ \結果 >= MIN_MERGE/2;
  @*/
プライベート静的int /*@ 純粋 @*/ minRunLength(int n) {
  n >= 0 であると主張します。
  int r = 0; // 1 ビットがシフトオフされると 1 になります
  /*@ loop_invariant n >= MIN_MERGE/2 && r >=0 && r<=1;
    @ は n を減少させます。
    @ 割り当て可能 \nothing;
    @*/
  (n >= MIN_MERGE) の場合
    r |= (n & 1);
    1 より大きい
  }
  n + r を返します。
}

前に奇妙な @ 記号が付いているものはアサーションです。実際には、入力が満たす必要がある条件と出力が満たす必要がある条件を定義しているだけです。たとえば、ソート アルゴリズムの場合、入力アサーションは空でない配列であり、出力アサーションは入力と同じ要素セットを持つ順序付けられた配列である必要があります。

これでプログラムの正確さが保証されると言う人もいます。ソフトウェア テストではできないのに、なぜ KeY はすべての実行パスをカバーできるのでしょうか。それは、KeY は実際のテスト データ セットを生成するのではなく、プログラムを記号化し、記号ロジックと計算を通じてすべての可能な実行パスを考慮できるためです。 （ここでは1万語省略します...）

もちろん、プログラムの正しさを証明するために KeY を使用するだけでも、まだかなりの作業が必要です。元の Timsort.java ファイルは約 900 行で、JML を追加すると約 1,400 行になります... ほぼすべての関数、ループ、条件文の前に、大量のアサーションを追加する必要があります。もちろん、これは無駄ではありません。少なくとも、このアンチプログラマーのバグを発見しました。

もちろん、業界の良心であるKeYが検証した正しいソリューションも提供。実感してください。

/*@ プライベート normal_behavior
@ 必要
@ \dl_elemInv(runLen, (\bigint)stackSize-4, MIN_MERGE/2)
@ && \dl_elemBiggerThanNext(runLen, (\bigint)stackSize-3)
@&& スタックサイズ > 0;
@保証します
@ (\forall \bigint i; 0<=i && i<(\bigint)stackSize-2;
@ \dl_elemInv(runLen, i, MIN_MERGE/2))
@ && \dl_elemBiggerThanNext(runLen, (\bigint)stackSize-2)
@ && ( (\sum int i; 0<=i && i

当初は、スタックの上位 3 つの実行のみを判断していました。現在は、スタックの上位 4 つの実行を判断しています。この変更により、スタック内のすべての実行が制約を満たしていることを確認できます。形式手法によって検証されているため、遠慮なく大胆に使用してください。~#p#

0×05 玉兔月面探査車のバグ

形式手法は非常に複雑で、小さなバグを見つけるために多大な労力を費やしたにもかかわらず、他の人はまったくそれを受け入れません。投資とリターンは少し釣り合いが取れていません... はい、形式手法は時々とても報われないことがあり、通常、プログラマーは自分のプログラムを検証するために形式手法を使用することはありません。では、形式手法を使っているのは誰でしょうか? 現時点では、Amazon や Facebook などの大規模で裕福な企業、または、以下で説明する玉兔月面探査車のような裕福な国家エンジニアリング プロジェクトです。

航空宇宙技術は、常に国の総合力を示す重要な分野であり、誰もがコストを気にせず資金を注ぎ込んでいます...もちろん、航空宇宙技術はリスクが高いことでも知られています。小さな部品の故障が深刻な結果を招く可能性があります。チャレンジャー号は、Oリングの故障による連鎖反応で打ち上げ後に爆発しました。12億ドルのスペースシャトルは一瞬で消え、乗組員7人が死亡しました...リスクが高いからこそ、もう少しお金をかけて安全性を1％高める価値があります。

そのため、形式手法にとって非常に重要な市場は航空宇宙分野です。昨年シンガポールで開催された第19回形式手法に関する国際シンポジウムでは、中国から2つのチームが発表を行いました。偶然にも、発表のトピックはどちらも玉兔月面車に関するもので、1つは月面軟着陸制御に関するもので、もう1つは玉兔月面車の制御システムに関するものでした。別の機会に形式手法を用いてYutu制御システムを検証したチームの報告を聞く機会があり、形式手法の威力と複雑さを実感しました。

次の図は、Yutu月面探査車の制御システムの簡略版です（実際のシステムには30以上のアプリケーションタスクがありますが、ここではそのうち6つだけを示します）。

図の左側には主にいくつかのタスクが表示され、中央はメッセージ キュー (送信キューと受信キューを含む)、右側は制御コマンドとセンサー データが送信される CAN バスです。具体的な意味は次の表の通りです。

Task1 から Task6 の優先度は順に減少していることに注意してください。Task1 の優先度は 6 で、Task6 の優先度は 1 です。

タスク5は定期的にデータを要求するタスクです。次の図に示すように、4ms以内に完全なテレメトリデータを受信することが期待されます。

通常の状況では、1 フレームのデータが送信され、6 フレームのデータが受信されます。このプロセスには、1×0.192(Task3Send)+0.5(IMU 応答時間)+6×0.192(Task5)=1.844ms かかります。事前設定された 4ms の待機時間は十分です。しかし、数年にわたる開発とテストの間に、開発者は偶然にいくつかの「テレメトリ タイムアウト エラー」を観察しました。4 ミリ秒以内に完了すると予想されていたタスク 5 がタイムアウトし、完全なデータを取得できませんでした。

このシステムは非常に複雑であり、オペレーティングシステムのタスクスケジューリングはランダムであるため、マルチタスクシステムの特定の実行を再現することは困難であり、リアルタイムオペレーティングシステムによるタスクのスケジューリングを観察することは非常に困難です。さらに重要なのは、このエラーが発生するのは非常にまれで、おそらく 1 年に 1 回程度であり、エラーが発生する条件を要約することが難しいことです。

次に形式手法が登場します。次の図をご覧ください。

これらの図についてはあまり詳しくは言いたくありません (ここでは 10,000 語は省略します...)。これらはオートマトンではないと言う人もいますが、その通りです。オートマトンは形式手法の非常に重要な部分です。最初の図は、タスク 1 に対応するプリエンプティブ タスクの時間オートマトン モデルです。2 番目の図は、タスク 2、タスク 5、およびタスク 6 に対応する周期タスクの時間オートマトン モデルです。3 番目の図は、タスク 3 およびタスク 4 に対応する散発タスクの時間オートマトン モデルです。

チームの女性医師によると、これらの絵を描くのに半年かかり、道具の助けも借りて描いたそうです。

もちろん、問題の原因は最終的に見つかりました。時刻 T に、次の条件が満たされたときにテレメトリ エラーが発生しました。

1. タスク6は時刻Tに準備完了、タスク2とタスク5は8ms後に準備完了。2. T+7ms後に地上コマンド（タスク1）がある。

この場合、Task1とTask2はTask5よりも優先度が高いため、それぞれ4フレームと8フレームのデータをSendQueueに書き込みます。その後、Task5は1フレームのデータをSendQueueに書き込むようにスケジュールされます。この時点で、SendQueueには13フレームのデータが蓄積されており、消費時間は13×0.192+0.5+6×0.192=4.148msとなり、4msを超えるためタイムアウトエラーが発生します。解決策も非常に簡単です。タスク 3 の優先度を上げて、このようなエラーを回避するために、データを時間内に送信できるようにします。

これを軽く話しているとは思わないでください。この問題は何年もエンジニアを悩ませてきました。形式手法を使用して検証するのに半年以上かかり、プロセスのうち6つだけが形式的に検証されました。30プロセスすべての正しさを検証するとしたら、その絵は私にとっては見るのが惜しいほど美しいでしょう...

0×06 要約

実は、これを書いていると少し話が逸れてしまった気がします。この記事では形式手法そのものについてはあまり触れていません...。個人的な見解ですが、私たちのような一般人がわざわざ勉強する必要はまったくありませんが、理解しておくことは必要です。解決できない不思議な問題に遭遇して絶望感を覚えたときは、形式手法を研究している専門家を探したほうがいいかもしれません。もしかしたら転機が訪れるかもしれません。

現状では、形式手法の敷居が高すぎて、大規模に適用することが困難です。しかし、脆弱性マイニングやインターネット セキュリティなどの分野で形式手法が普及すれば、コンピューター セキュリティの分野全体に大きな波紋が広がることは間違いないと考えられます。

0×07 参考文献

1. Android、Java、Python のソートアルゴリズムが壊れていることを証明する（そしてそれを修正する方法を示す）

2. OpenJDK の java.utils.Collection.sort() が壊れている: 良い点、悪い点、最悪のケース

3. UPPAAL を使用した月面探査車制御ソフトウェアの形式検証

4. サイバーフィジカル融合システムの制御ソフトウェアの統計モデル検証

5. OpenJDK ソースコードを読む TimSort