JavaのTimSortにバグ | NurseAngelの日記

NurseAngelの日記： JavaのTimSortにバグ 0

日記 by NurseAngel 2015年02月27日 2時58分

TimSort fails with ArrayIndexOutOfBoundsException on worst case long arrays

Pythonで実装され、その後Javaにも移植されたソートアルゴリズムであるTimSortが盛大にバグっていることが発見されました。
通常の利用では想定しえない場所でArrayIndexOutOfBoundsExceptionが発生します。

java.util.Arrays#sortを呼出すと発生する。例えば、以下のAPIも間接的に当該APIを呼出す
java.util.List#sort
java.util.Collections#sort

要素数が67108864件以上で発生する
もっと少ない件数で発生するケースがあるかもしれません。

TimSortにとって都合の悪い並び順だと発生する
要素数が多くてもTimSortにとって都合の悪い並び順でなければ発生しない

この件が本当に面白いのはKeYという形式手法をサポートするツールによってバグが発見されたことなのですけども、僕にはそれを適切に説明する能力が無いのです…。

そもそもそんな件数をソートする時点でまともに動作するんだろうか？

TimSortは、高速な安定ソートで、Python(>=2.3)やJava SE 7、およびAndroidでの標準ソートアルゴリズムとして採用されているそうです。
TimSortとは一言で言うと、"STLのIntroSortのマージソート版"です。

IntroSortとは、クイックソートの改良です。
Introソートではそれに対処するため、再帰の深さが要素数の対数を超えるとヒープソートに切り替えます。これにより最悪計算量をO(nlogn)に抑えつつ、平均的なデータではクイックソートに匹敵する性能を達成しています。

TimSortは通常のマージソートとは異なり、予めある程度のサイズのソート済み列（runと呼ぶ）に分割して、それからマージを行います。

クイックソートのように最悪計算量が問題になることがないので、これを標準に採用するのはセキュリティーの観点から利点があるでしょう。

よくわかりません。

形式手法とは、1970年代から始められたプログラム開発手法の1つで、論理学や離散数学などが基礎になっています。プログラムの正しさに関する数学的な証明体系として整理された理論をベースとし、形式仕様記述やモデル検査へと研究対象を発展させてきています。

矛盾がなく論理的に正しい仕様を作成するために考案されたのが形式仕様記述です。

形式検証は、プログラムの状態をモデル化することで仕様が正しいことを検証する方法です。通信や並行処理システムにおける複雑な状態を検証する方法として、レビューだけで検証するよりも、ツールによるモデルの自動検証は有効な手段です。

まったくわかりません。