しかし、2015年に遡ります。 KeYと呼ばれる正式な検証ツールを使用して、 カウントソートとビットごとのソート （ J. Autom。Reasoning 53（2）、129-139 ）のJava実装を正常に検証した後、調査する新しいオブジェクトを検索しました。 Timsortは非常に洗練されており、広く使用されているため、良い候補のように見えました。 残念ながら、その正確性を証明できませんでした。 この理由は、よく調べてみると簡単でした。ティムソートの実装にはバグがあります。 私たちの理論的研究は、エラーを探す場所を示しました（エラーが既にPython実装にあったのは不思議です）。 この記事では、これをどのように達成したかについて説明します。
より完全な分析を含む記事、およびいくつかのテストプログラムは、 当社のWebサイトで入手できます。
内容
- Android、Java、PythonでのTimsortの実装のバグ
1.1ティムソートのバグをJavaで再現します
1.2ティムソートは原則としてどのように機能しますか？
1.3ティムソートのバグのステップバイステップ - ティムソートの証明（In）
2.1 KeY検証システム
2.2修正とその正式な仕様
2.3 KeYの結果の分析 - PythonおよびAndroid / JavaでのTimsort実装のバグ修正案
3.1無効なmerge_collapse関数（Python）
3.2修正された関数merge_collapse（Python）
3.3無効なmergeCollapse関数（Java / Android）
3.4 mergeCollapse関数の修正（Java / Android） - 結論：次の結論のどれが続きますか？
1. Android、Java、PythonでのTimsortの実装のバグ
それで、バグは何ですか？ そして、なぜ自分でそれを再現してみませんか？
1.1ティムソートのバグをJavaで再現します
git clone https://github.com/abstools/java-timsort-bug.git cd java-timsort-bug javac *.java java TestTimSort 67108864
バグが存在する場合、この結果が表示されます
Exception in thread "main" java.lang.ArrayIndexOutOfBoundsException: 40 at java.util.TimSort.pushRun(TimSort.java:413) at java.util.TimSort.sort(TimSort.java:240) at java.util.Arrays.sort(Arrays.java:1438) at TestTimSort.main(TestTimSort.java:18)
エラー再生ビデオ録画
1.2ティムソートは原則としてどのように機能しますか
Timsortは、挿入ソートとマージソートを使用するハイブリッドアルゴリズムです。
このアルゴリズムは、入力配列を左から右に並べ替え、連続する（重複しない）ソートされたセグメント（「シリーズ」または実行）を見つけます。 シリーズが特定の最小長より短い場合、後続の要素によって補完され、挿入によってソートされます。 作成されたシリーズの長さは、 runLen配列の最後に追加されます。 runLenに新しいシリーズが追加されると、mergeCollapseメソッドは、runLenの最後の3つの要素が「 不変式 」と呼ばれる次の条件のペアを満たすまでシリーズをマージします。
- runLen [n-2]> runLen [n-1] + runLen [n]
- runLen [n-1]> runLen [n]
ここで、nはrunLenの最後のシリーズのインデックスです。 考え方は、最後の3つのシリーズについてこの不変式をチェックすることで、シリーズの連続するすべてのトリプルがそれを満たしていることを保証することでした。 最後に、すべての系列がマージされ、入力配列が完全にソートされます。
効率上の理由から、 runLenではできるだけ少ないメモリを割り当てることをお勧めしますが、すべてのシリーズがそれに収まるのに十分なはずです。 不変式がすべてのシリーズに当てはまる場合、シリーズの長さは指数関数的に増加します（フィボナッチ数よりも高速です。各シリーズの長さは、次の2つの長さの合計よりも厳密に大きくなります）。 シリーズはオーバーラップしないため、巨大な入力配列を完全にソートするのにそれほど多くは必要ありません。
1.3ティムソートのバグのステップバイステップ
次のコードスニペットは、mergeCollapse実装がrunLenの最後の3つのシリーズの不変式をチェックすることを示しています。
private void mergeCollapse() { while (stackSize > 1) { int n = stackSize - 2; if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1]) { if (runLen[n - 1] < runLen[n + 1]) n--; mergeAt(n); } else if (runLen[n] <= runLen[n + 1]) { mergeAt(n); } else { break; // } } }
残念ながら、これはすべてのシリーズが不変量を満たすのに十分ではありません。 mergeCollapse（n = 4）を実行する前に、 runLenにこのような長さのセットが含まれているとします。
120, 80, 25, 20, 30
whileループの最初のパスで、長さ25と20のシリーズが結合されます（25 <20 + 30と25 <30のため）：
120, 80, 45, 30
サイクルの2番目のパス（現在n = 3）では、80> 45 + 30および45> 30であるため、不変量が最後の3つのシリーズに設定されていると判断し、mergeCollapseが作業を完了します。 ただし、mergeCollapseは配列全体の不変式を復元しませんでした。120<80 + 45であるため、最初の3つの不変式に違反しています。
このサイトのテストジェネレーターを使用すると、この問題を特定できます。 多くの短い系列を持つ入力配列を作成しますが、それらの長さは不変量を満たさないため、ティムソートの崩壊につながります。 エラーの本当の原因は、不変量の違反により、系列の長さが予想よりもゆっくりと成長し、その結果、その数がrunLen.lengthを超え、これによりArrayOutOfBoundsExceptionが発生することです。
2.ティムソートの（中の）正当性の証明
Timsortを正式に検証しようとすると、mergeCollapse不変式が壊れていることがわかりました。 幸いにも、それを修正する方法を見つけました。 その結果、修正されたバージョンを検証することさえできました。このバージョンでは、不変式が実際に観察されます。 しかし、急いではいけません。 まず、正式な検証とは何か、どのように実行されるかを理解します。
2.1 KeY検証システム
KeYは、シングルスレッドJavaおよびJavaCardプログラムの演ductive的検証プラットフォームです。 特定の仕様に対するプログラムの正確性を証明できます。 大まかに言うと、仕様は前提条件 （KeYの観点から- が必要 ）と事後条件 （KeYの観点から-が保証 ）で構成されます。 仕様は、それらを実装するメソッドの前に指定されます（たとえば、前述のmergeCollapse（）の前）。 メソッドの仕様は、そのコントラクトとも呼ばれます。
ソートの場合、前提条件は単に空でない配列が入力に提供されることを示し、事後条件は結果の配列がソートされることを要求し、入力の順列です。 KeYシステムは、検証済みのメソッドが前提条件を満たす入力データで呼び出された場合、メソッドが正常に終了し、結果の状態が事後条件を満たすことを証明します。 これは、メソッドの正常な完了が証明されるため、 完全な正確性とも呼ばれます。 前述のように、OpenJDKのjava.util.Arrays.sort（）メソッドはこの契約に準拠していません。特定の入力データについては例外で終了するためです。
さらに、クラスとオブジェクトの不変式は、フィールド値の一般的な制限を示すために使用されます。 通常、データの整合性または境界条件がチェックされます。
/*@ private invariant @ runBase.length == runLen.length && runBase != runLen; @*/
この不変式は、runBase配列とrunLen配列の長さは同じでなければならないが、同時に2つの異なる配列でなければならないことを示しています。 不変条件のセマンティクスは、各出力メソッドがその契約の事後条件を提供するだけでなく、独自の「this」オブジェクトの不変条件も提供することを意味します。
KeYはJavaモデリング言語 （JML）を仕様言語として使用します 。 その中の式は通常のJava言語で書かれているため、Javaプログラマーは簡単に習得できます。 主なJML拡張機能は、数量詞（ \ forall T x-任意のTに対して、 \存在する T x-存在するT）およびもちろん、契約の特別なキーワードです。 JML仕様は、関連するコードの前のJavaファイルのコメントで提供されます。 以下は、JML仕様のJavaメソッドの簡単な例です。
/*@ private normal_behavior @ requires @ n >= MIN_MERGE; @ ensures @ \result >= MIN_MERGE/2; @*/ private static int /*@ pure @*/ minRunLength(int n) { assert n >= 0; int r = 0; // 1 /*@ loop_invariant n >= MIN_MERGE/2 && r >=0 && r<=1; @ decreases n; @ assignable \nothing; @*/ while (n >= MIN_MERGE) { r |= (n & 1); n >>= 1; } return n + r; }
minRunLength（）コントラクトには1つの前提条件が含まれます。入力パラメーターはMIN_MERGE以上でなければなりません。 この場合（そしてこの場合のみ）、メソッドは正常に完了し（ループして例外をスローしない）、MIN_MERGE / 2以上の値を返すことを約束します。 さらに、メソッドはpureとしてマークされます。 これは、メソッドがヒープを変更しないことを意味します。
重要な点は、KeYシステムが任意の入力パラメーターに対して同様のメソッドのコントラクトを静的に証明できることです。 これはどのように可能ですか？ KeYは、検証されたメソッドのシンボリック実行を実行します。つまり、シンボリック値を使用して実行されるため、可能なすべての実行パスが考慮されます。 しかし、これは十分ではありません。反復の回数に制限のないループ（stackCsizeの値がわからないmergeCollapse（）のループなど）のシンボリック実行が終了しないためです。 サイクルのシンボリック実行が有限になるために、不変式の論理が使用されます。 たとえば、上記のminRunLength（）メソッドには、仕様がループ不変式で表されるループが含まれています。 不変式は、各反復の後、条件
n >= MIN_MERGE/2 && r >= 0 && r <= 1
が満たされ、これからメソッド全体の事後条件を証明できると主張します。 抽象的減少 （減少）は、サイクルの完了を証明するために使用されます。 値が負ではなく、厳密に縮小された式を示します。 割り当て可能な構造は、ループで変更できるヒープオブジェクトをリストします。 \ nothingキーワードは、ヒープが変更できないことを意味します。 実際、ループはローカル変数rと引数nのみを変更します。
一般に、方式の契約には正式な契約では十分ではありません。 サイクルの不変量を与えることも必要です。 サイクルで観測される不変式を見つけるのが非常に困難であると同時に、それからメソッドの事後条件を推測するのに十分な強さがある場合があります。 自動化された定理の証明のための機器によるサポートと技術がなければ、自明でないプログラムで正しいサイクル不変量を構成することはほとんど不可能です。 実際、ティムソートのクリエイターの間違いはここにあります。 特定の条件下で、mergeCollapseのループは、次のTimsortクラスの不変条件に違反します（セクション1.3 Timsortのバグの手順を参照）。
/*@ private invariant @ (\forall int i; 0<=i && i<stackSize-4; @ runLen[i] > runLen[i+1] + runLen[i+2])) @*/
この不変式は、stackSize-4より小さい負でないiに対して、runLen [i]は次の2つの要素の合計よりも大きくなければならないことを示しています。 不変式はサイクルの後でも復元されないため、mergeCollapseメソッド全体はクラス不変式を保持しません。 したがって、ループ不変条件は、開発者が想定したほど厳密ではありません。 これは、TimsortをKeYで検証しようとしたときに発見したものです。 特別なツールがなければ、検出することはほとんど不可能です。
JMLはJavaに非常に似ていますが、Javaプログラムの完全な機能検証に適した本格的な契約プログラミング言語です。
2.2修正とその正式な仕様
著者によると、mergeCollapseで遵守すべき契約の簡略版を以下に示します。
/*@ requires @ stackSize > 0 && @ runLen[stackSize-4] > runLen[stackSize-3]+runLen[stackSize-2] @ && runLen[stackSize-3] > runLen[stackSize-2]; @ ensures @ (\forall int i; 0<=i && i<stackSize-2; @ runLen[i] > runLen[i+1] + runLen[i+2]) @ && runLen[stackSize-2] > runLen[stackSize-1] @*/ private void mergeCollapse()
の2つの式は、mergeCollapseが完了すると、 すべての系列がセクション1.2で指定された不変式を満たすことを意味します。 このコントラクトは、現在のmergeCollapse実装（ セクション1.3 ）で実行されないことをすでに見てきました。 次に、契約を尊重する改訂版を提供します。
private void newMergeCollapse() { while (stackSize > 1) { int n = stackSize - 2; if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1] || n-1 > 0 && runLen[n-2] <= runLen[n] + runLen[n-1]) { if (runLen[n - 1] < runLen[n + 1]) n--; } else if (n<0 || runLen[n] > runLen[n + 1]) { break; // } mergeAt(n); } }
このバージョンの主なアイデアは、 3つではなくrunLenの最後の4つのシリーズで不変式が観測されることを確認することです。 以下で説明するように、これは、mergeCollapseの完了後にすべての系列の長さが不変式を満たすことを保証するのに十分です。
mergeCollapseの固定バージョンのコントラクトを証明する最初のステップは、適切なループ不変式を見つけることです。 以下はその簡略版です。
/*@ loop_invariant @ (\forall int i; 0<=i && i<stackSize-4; @ runLen[i] > runLen[i+1] + runLen[i+2]) @ && runLen[stackSize-4] > runLen[stackSize-3]) @*/
直観的に、サイクル不変式は、最後の4つを除くすべてのシリーズが条件を満たしていることを示します。 同時に、最後の4つのシリーズも満たす場合にのみ、（breakステートメントによって）サイクルが終了することに注意してください。 したがって、すべての系列が不変式を満たすことが保証されます。
2.3 KeYの結果の分析
修正されたバージョンのmergeCollapseをコントラクトとループ不変条件とともにKeYに送信すると、システムはループのシンボリック実行を実行し、検証条件を生成します：式。その結果、mergeCollapseコントラクトが実行されます。 次の（簡略化された）式は、KeYによって生成されたmergeCollapseの正確性を証明するための主な条件を示しています。
この式は、サイクルの終了後に真になる括弧内の条件の後に、条件後のmergeCollapseが続く必要があることを示しています。 かっこ内の式がどこから来たかは明らかです。ループを終了するbreakステートメントは、それらがすべて真である場合にのみ実行されます。 KeYを半自動モードで使用して、この式（および他のすべての検証条件）を正式に証明しました。 以下は証拠のスケッチです。
証明 。 事後条件mergeCollapseからの式runLen [stackSize-2]> runLen [stackSize-1]は、 n> = 0 ==> runLen [n]> runLen [n + 1]から直接続きます。
次の式を証明しましょう。
\ forall int i; 0 <= i && i <stackSize-2; runLen [i]> runLen [i + 1] + runLen [i + 2]
iの値には次のオプションが可能です。
- i <stackSize-4：ループ不変量に対応
- i = stackSize-4：n> 1 ==> runLen [n-2]> runLen [n-1] + runLen [n]から続きます
- i = stackSize-3：n> 0 ==> runLen [n-1]> runLen [n] + runLen [n + 1]から続きます
この証明は、 すべての系列が不変式を満たす場合にのみ、 mergeCollapseの新しいバージョンが完了することを示しています。
3. PythonおよびAndroid / JavaでのTimsort実装のバグ修正案
エラー分析（ mergeCollapse修正を含む）が提出され、レビューされ、 Javaバグトラッカーに受け入れられました。
このバグは、少なくともAndroid、OpenJDK、およびOracleJDKのJavaバージョンに存在します。すべて同じTimsortコードを使用しています。 バグもPythonに存在します。 次のセクションでは、元のバージョンと改訂版を提供します。
上記のように、修正のアイデアは非常に単純です。不変量が3つだけでなく、runLenの最後の4つのシリーズに対して有効であることを確認します。
3.1無効なmerge_collapse関数（Python）
Python用のTimsort（Python APIを使用してCで作成）は、subversionリポジトリで利用可能です -アルゴリズムもここで説明されています 。
Java用のTimsortバージョンはCPythonに移植されました。 CPythonバージョンには、最大2 64要素までの配列をサポートするように設計されたエラーが含まれており、エラーも含まれています。 ただし、現代のマシンでは配列オーバーフローエラーを引き起こすことは不可能です：アルゴリズムはrunLenに85個の要素を割り当て、これは2 49個以下の要素を含む配列に対して十分です（この記事の記事全体で示されているように）。 比較のために、今日の最も強力なスーパーコンピューターTianhe-2には2 50バイトのメモリーがあります。
/* The maximum number of entries in a MergeState's * pending-runs stack. * This is enough to sort arrays of size up to about * 32 * phi ** MAX_MERGE_PENDING * where phi ~= 1.618. 85 is ridiculously large enough, * good for an array with 2**64 elements. */ #define MAX_MERGE_PENDING 85 merge_collapse(MergeState *ms) { struct s_slice *p = ms->pending; assert(ms); while (ms->n > 1) { Py_ssize_t n = ms->n - 2; if (n > 0 && p[n-1].len <= p[n].len + p[n+1].len) { if (p[n-1].len < p[n+1].len) --n; if (merge_at(ms, n) < 0) return -1; } else if (p[n].len <= p[n+1].len) { if (merge_at(ms, n) < 0) return -1; } else break; } return 0; }
3.2修正された関数merge_collapse（Python）
merge_collapse(MergeState *ms) { struct s_slice *p = ms->pending; assert(ms); while (ms->n > 1) { Py_ssize_t n = ms->n - 2; if ( n > 0 && p[n-1].len <= p[n].len + p[n+1].len || (n-1 > 0 && p[n-2].len <= p[n].len + p[n-1].len)) { if (p[n-1].len < p[n+1].len) --n; if (merge_at(ms, n) < 0) return -1; } else if (p[n].len <= p[n+1].len) { if (merge_at(ms, n) < 0) return -1; } else break; } return 0; }
3.3無効なmergeCollapse関数（Java / Android）
このエラーは、Pythonのエラーとまったく同じです。
private void mergeCollapse() { while (stackSize > 1) { int n = stackSize - 2; if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1]) { if (runLen[n - 1] < runLen[n + 1]) n--; mergeAt(n); } else if (runLen[n] <= runLen[n + 1]) { mergeAt(n); } else { break; // } } }
3.4 mergeCollapse関数の修正（Java / Android）
修正は、Pythonの上記と同様です。
[更新26/2：記事の元のバージョンと比較してコードを変更しました。 古いコードは同等でしたが、冗長なチェックが含まれ、スタイルが異なりました。 注意してくれたみんなに感謝します！]
private void newMergeCollapse() { while (stackSize > 1) { int n = stackSize - 2; if ( (n >= 1 && runLen[n-1] <= runLen[n] + runLen[n+1]) || (n >= 2 && runLen[n-2] <= runLen[n] + runLen[n-1])) { if (runLen[n - 1] < runLen[n + 1]) n--; } else if (runLen[n] > runLen[n + 1]) { break; // } mergeAt(n); } }
4.結論：これからどの結論が続きますか？
ティムソートを検証しようとしたとき、ソートオブジェクトの不変式を確立できませんでした。 失敗の原因を分析することで、特定の入力に対してArrayOutOfBoundsExceptionをスローするTimsort実装にエラーが見つかりました。 誤りのあるメソッドの修正（パフォーマンスの顕著な低下なし）を提案し、修正が正しく、エラーがないことを正式に証明しました。
このストーリーから、実際に見つかったエラーに加えて、いくつかの観察を行うことができます。
- 多くの場合、プログラマーは、公式の方法が非現実的であるか、現実世界のタスクから遠く離れていることを発見します。 これはそうではありません。数十億人のユーザーが毎日使用するソフトウェアのバグを見つけて修正しました。 私たちの分析が示したように、正式な分析および検証ツールなしでは、そのようなバグを見つけて修正することは事実上不可能です。 このエラーは、JavaおよびPython言語の標準ライブラリに長年存在していました。 その兆候は以前に気づかれており、修正されたとさえ考えていましたが、実際には、エラーの発生頻度が少なくなったことだけを達成しました。
- このようなエラーが偶然に発生することはまずありませんが、攻撃にどのように使用できるかは容易に想像できます。 おそらく、一般的なプログラミング言語の標準ライブラリには、他の未検出エラーがあります。 彼らが危害を加えたり、侵入者に使用される前にそれらを調べる価値があるのでしょうか？
- このレポートに対するJava開発者の反応は、いくつかの点でがっかりです。 mergeCollapse（）の修正（および検証済み）バージョンを使用する代わりに、選択したrunLenサイズを「十分な」サイズに増やすことを選択しました。 すでに示したように、そうする必要はまったくありませんでした。 しかし、今ではjava.utils.Collection.sort（）を使用するすべての人は、より多くのメモリを使用することを余儀なくされます。 そのような基本機能を使用する天文学的なプログラムの数を考えると、これは顕著な追加のエネルギーコストにつながります。 決定が下されなかった理由を推測することしかできません。おそらく、JDK開発者はレポートを完全に読むことを気にせず、したがって修正の本質を理解せず、それに依存しないことに決めました。 最終的に、OpenJDKは、あまり時間がないボランティアで主に構成されるコミュニティを開発しています。
これからどの結論が導かれますか？ 正式な手法の研究者とオープンソフトウェアプラットフォームの開発者との緊密な相互作用の出発点として、私たちの仕事が役立っていれば幸いです。 正式な方法はすでにAmazonとFacebookで正常に適用されています。 最新の形式仕様言語と形式検証ツールは、それほど複雑ではなく 、学ぶのに非常に複雑ではありません 。 ユーザビリティと自動化は常に改善されています。 しかし、私たちのツールを試し、テストし、使用する人がもっと必要です。 はい、正式な仕様の記述とコードの検証を開始するには多少の努力が必要ですが、これは、たとえば、コンパイラまたはプロジェクトビルダーの使用方法を理解することほど難しくありません。 しかし、私たちは数ヶ月または数年ではなく、数日または数週間について話している。 さて、どのように挑戦を受け入れますか？
よろしく
スタインデゴーブ 、 ジュリアンロス 、 フランクデボーア 、 リチャードブーベル 、 レイナーヘンレ 。
謝辞
この作業は、欧州連合FP7-610582 ENVISAGE： Engineering Virtualized Servicesの第7フレームワークプログラムのプロジェクトによって部分的にサポートされていました。
この記事は、 Amund Tweitのサポートと丁寧なリマインダーなしでは書かれなかったでしょう！ また、エラーを示すビデオを提供してくれたBeruza Nobactに感謝します。
