волшебно

[thedeemon]

Некие люди занимались верификацией всякого кода на Джаве и столкнулись с трудностями при доказательстве корректности TimSort'a - алгоритма сортировки, издавна используемого в Питоне и Джаве. Оказалось, что он некорректен, на некоторых данных не работает вообще.

Proving that Android’s, Java’s and Python’s sorting algorithm is broken (and showing how to fix it)

Кому вообще нужны эти теорем-пруверы? Питон, тесты, махание руками!

Comments

[deni-ok.livejournal.com]

"The reaction of the Java developer community to our report is somewhat disappointing"

[worm-ii.livejournal.com]

Дык, если мне память не изменяет, только-только 32-разрядный quick sort пофиксили на массивах длиной более 2^31, чего ж Вы хотите от более сложных алгоритмов?

Ай, память подвела-таки, двоичный поиск же, не quick sort:
http://habrahabr.ru/post/91605/

[juan-gandhi.livejournal.com]

Фигасе. А им так гордились...

[aruslan.livejournal.com]

Блеск. И нищета.

[urod.livejournal.com]

Похихикал.

Там ссылка и на баг с бинарным поиском.

[sorhed.livejournal.com]

Кем, тимсортом? Это ж хак. Не то что бы в этом было что-то плохое...

[sorhed.livejournal.com]

Раз за столько лет в продакшне не вылезало (при всей широте применения) — значит, minor issue. Так-то, конечно, теоретически интересно, но не более того.

[nivanych.livejournal.com]

Я ещё понимаю реакцию на "broken".
Но на
> (and showing how to fix it)
надо ж радоваться полчаса!

[sassa-nf.livejournal.com]

да нет, пофиксили же, но топорным увеличением runLen.

[thedeemon.livejournal.com]

Так правильное решение, вероятно, медленнее, потому джавщики предпочли просто размер буфера увеличить, авось проканает. Вон в питоне буфер побольше, там канает, хоть и ошибка в логике.

[nivanych.livejournal.com]

Эпично, эпично.
Надеюсь, расползётся и побольше народу узнает.
Например, средствами чОрного пеара —
"Воон там какие-то придурки со своей математикой припёрлись и чо оно получили? Малозначительную issue нашли. Всё бы им в своей ерунде ковыряться, а не работать!" ;-)
Можно гораздо красочнее расписать, если чуть постараться ;-)

[http://users.livejournal.com/_winnie/]

Быстро пробежался глазами, не увидел proof of concept демонстрации бага. Стоит ли читать внимательно? Какого минимального размера должны быть данные для некорректной работы алгоритма?

[gegmopo4.livejournal.com]

Более 2⁴⁹ элементов. Наиболее мощный на сегодня суперкомпьютер имеет память размером только 2⁵⁰ байт.

[gegmopo4.livejournal.com]

Да, в предлагаемом решении на одно условие в цикле больше.

[thedeemon.livejournal.com]

Пункты 1.1 и 1.3, не?

[thedeemon.livejournal.com]

В примере, на котором джава падает, 67 миллионов элементов всего.

[juan-gandhi.livejournal.com]

Ну, во-первых, это красиво.

[gegmopo4.livejournal.com]

Не повезло.

[sleepy-drago.livejournal.com]

практики как хардкодили константы так и хардкодят. Не то что я не сочувствую этим донкихотам от верификации, но как то не существенно оно пока.

[http://users.livejournal.com/_winnie/]

Да, спасибо, проглядел.
Массивы в 67'000'000 элементов вполне встречаются (как раз тот размер, который ещё можно локально обрабатывать без mapreduce)

git clone https://github.com/abstools/java-timsort-bug.git
cd java-timsort-bug
javac *.java
java TestTimSort 67108864

[theiced.livejournal.com]

пфф... вот у людей проблемы (https://bugs.php.net/bug.php?id=50916 и
https://bugs.php.net/bug.php?id=61095) так проблемы, а вы тут с иногда неработающей сортировкой лезете :)

[thedeemon.livejournal.com]

Там это не проблемы, это норма. :)