JavaのTimSortがバグってる件について | さにあらず

Python で実装され、その後 Java にも移植されたソートアルゴリズムである TimSort が盛大にバグっていることが発見されました。 このバグがどのようにして発生するのかについては、以下のドキュメントを精査して下さい。 TimSort fails with ArrayIndexOutOfBoundsException on worst case long arrays OpenJDK’s java.utils.Collection.sort() is broken: The good, the bad and the worst case どんなことが起こるのか​ 通常の利用では想定しえない場所でArrayIndexOutOfBoundsExceptionが発生します。 例えば、以下のようなスタックトレースになります。 Exception in thread "main" jav

[Dryad]

『この件が本当に面白いのはKeYという形式手法をサポートするツールによってバグが発見されたことなのですけども』

[YaSuYuKi]

これか https://github.com/IKEGAMIDaisuke/Blogs/blob/master/20141224-IntroductionToKeYProver/README.md ＞形式手法をサポートするツール

[terazzo]

形式手法で既存のライブラリの不具合が発見されるの、前もCCS InjectionをCoqで見つけたとかあったし今後も増えそう。

[t-wada]

"この件が本当に面白いのはKeYという形式手法をサポートするツールによってバグが発見されたこと" CCS Injection 脆弱性と同じく、形式手法が不具合を検出した例か http://ccsinjection.lepidum.co.jp/blog/2014-06-05/CCS-Injection/index.html

[tengo1985]

こんな件数をソートすることはあんまりないから影響なさそうだけど怖い。ソースの@authorはJoshua Blochだった気がするけどちがったかな。

[hush_in]

形式手法すごい

[naga_sawa]

Arrays#sort が ArrayIndexOutOfBoundsException 出すバグ/もしかしたらぶつかることがあるかもしれないので念のため

[taku-o]

ｱｲｪｪｪ "Androidは標準のソートアルゴリズムがTimSortです" ／こういう問題に当たった時はどういう対応をすべきなのかな？／"要素数が67108864件以上"なので、そんなにぶち当たらない問題ではある

[mas-higa]

"この件が本当に面白いのは" kwsk

[higedice]

＜Pythonの実装では4096TBという巨大なメモリを使う場合に発生＞＜Javaの実装ではそれ程巨大な要素数を必要としません…64MB程度のメモリでも発生＞

[mumincacao]

すごい特殊な発動条件とはいえ踏んじゃったらなんでそんなとこで例外飛んでくるのか原因不明で悩みそうだなぁ・・・ （・ω・；【みかん

[aodifaud09]

「より少ない件数で発生するかもしれません」「Androidは標準のソートアルゴリズムがTimSortです」「Androidの場合ワークアラウンドはありません」駄目やん！やばいやん！どうすんのこれ！もう今日は仕事しない！

[airj12]

形式手法よくわかんない

[a2ikm]

"この件が本当に面白いのはKeYという形式手法をサポートするツールによってバグが発見されたことなのですけども"

[tinsep19]

この件が本当に面白いのはKeYという形式手法をサポートするツールによってバグが発見されたこと

[windish]

67108864個のリストなんて作らないけど、経絡秘孔をついちゃう場合があるのかー。

[knjname]

"JavaのTimSortがバグってる件について — さにあらず"

[vanbraam]

"この件が本当に面白いのはKeYという形式手法をサポートするツールによってバグが発見されたこと"<-面白そう;実装がバグってたのか,アルゴリズム自体に問題があったのか,どっちだろう?<-論文斜め読んだが実装の様だ

[decoy2004]

『形式手法を用いたツール (KeY) によりソートのバグを発見。』

[Nkzn]

67108864個もソートしないから一応大丈夫だけどねえ

[houyhnhm]

Pythonも影響するの？

[kiri3]

JavaのTimSortがバグってる件について — さにあらず

[morita_non]

KeYってなんぞ？

[miyakawa_taku]

形式手法を用いたツール (KeY) によりソートのバグを発見。

[yujiorama]

Oracle JDK 1.7.0_75-b13 でも再現するので怖くなってる

[fa11enprince]

ほげー

[sona-zip]

形式手法だとモデルさえ正しく作成すれば実運用では見つけづらいエラー系も発見できることがいいよね 言語や基本ライブラリ命の関わるコードでは積極的に採用していくべき Keyは簡単に使える？

[bobbyjam99]

JavaのTimSortがバグってる件について — さにあらず :

[raimon49]

java.util.Arrays.useLegacyMergeSort=true

[hiroshi_revolution]

JavaのTimSortがバグってる件について — さにあらず

[yamadamn]

JavaのTimSortがバグってる件について — さにあらず