Доказательство некорректности алгоритма сортировки Android, Java и Python
- понедельник, 2 марта 2015 г. в 02:10:41
python
http://habrahabr.ru/post/251751/
Тим Петерс разработал гибридный алгоритм сортировки Timsort в 2002 году. Алгоритм представляет собой искусную комбинацию идей сортировки слиянием и сортировки вставками и заточен на эффективную работу с реальными данными. Впервые Timsort был разработан для Python, но затем Джошуа Блох (создатель коллекций Java, именно он, кстати, отметил, что большинство алгоритмов двоичного поиска содержит ошибку) портировал его на Java (методы java.util.Collections.sort и java.util.Arrays.sort). Сегодня Timsort является стандартным алгоритмом сортировки в Android SDK, Oracle JDK и OpenJDK. Учитывая популярность этих платформ, можно сделать вывод, что счёт компьютеров, облачных сервисов и мобильных устройств, использующих Timsort для сортировки, идёт на миллиарды.
Но вернёмся в 2015-й год. После того как мы успешно верифицировали Java-реализации сортировки подсчётом и поразрядной сортировки (J. Autom. Reasoning 53(2), 129-139) нашим инструментом формальной верификации под названием KeY, мы искали новый объект для изучения. Timsort казался подходящей кандидатурой, потому что он довольно сложный и широко используется. К сожалению, мы не смогли доказать его корректность. Причина этого при детальном рассмотрении оказалась проста: в реализации Timsort есть баг. Наши теоретические исследования указали нам, где искать ошибку (любопытно, что ошибка была уже в питоновской реализации). В данной статье рассказывается, как мы этого добились.
Статья с более полным анализом, а также несколько тестовых программ доступны на нашем сайте.
Содержание
Так в чём же заключается баг? И почему бы вам не попробовать воспроизвести его самим?
Если баг присутствует, вы увидите такой результат
Видеозапись воспроизведения ошибки
Тimsort — это гибридный алгоритм, который использует сортировку вставкой и сортировку слиянием.
Алгоритм переупорядочивает входной массив слева направо, находя в нём последовательные (неперекрывающиеся) сортированные сегменты («серии», или runs). Если серия короче определённой минимальной длины, она дополняется последующими элементами и сортируется вставкой. Длины созданных серий добавляются в конец массива runLen. Когда новая серия добавляется в runLen, метод mergeCollapse сливает серии, пока три последних элемента в runLen не будут удовлетворять следующей паре условий, которая называется «инвариантом»:
Здесь n — это индекс последней серии в runLen. Идея была в том, что проверка этого инварианта для последних трёх серий гарантирует, что все последовательные тройки серий будут ему удовлетворять. В конце сливаются все серии, что даёт в результате полностью отсортированный входной массив.
Из соображений эффективности желательно выделить как можно меньше памяти под runLen, но её должно быть достаточно, чтобы туда заведомо поместились все серии. Если инвариант выполняется для всех серий, длина серий будет расти экспоненциально (даже быстрее, чем числа Фибоначчи: длина каждой серии строго больше суммы длин двух последующих). Так как серии не перекрываются, их потребуется не так много, чтобы полностью отсортировать даже огромный входной массив.
Из следующего фрагмента кода видно, что реализация mergeCollapse проверяет инвариант для последних трёх серий в runLen:
К сожалению, этого не достаточно, чтобы все серии удовлетворяли инварианту. Предположим, что runLen содержит такой набор длин перед выполнением mergeCollapse (n=4):
На первом проходе цикла while будут объединены серии длиной 25 и 20 (так как 25 < 20 + 30 и 25 < 30):
На втором проходе цикла (теперь n=3), мы определяем, что инвариант установлен для последних трёх серий, потому что 80 > 45 + 30 и 45 > 30, поэтому mergeCollapse завершает работу. Но mergeCollapse не восстановил инвариант для всего массива: он нарушается в первой тройке, так как 120 < 80 + 45.
Генератор тестов на нашем сайте позволяет выявить эту проблему. Он создаёт входной массив с множеством коротких серий, при этом их длины не удовлетворяют инварианту, что приводит к падению Timsort. Истинная причина ошибки в том, что из-за нарушения инварианта длины серий растут медленнее, чем ожидалось, в результате чего их количество превышает runLen.length и это приводит к ArrayOutOfBoundsException.
Мы обнаружили, что инвариант mergeCollapse нарушается, когда пытались формально верифицировать Timsort. К счастью, мы также поняли, как его исправить. В итоге нам даже удалось верифицировать исправленную версию, в которой инвариант действительно соблюдается. Но не будем спешить. Для начала разберёмся, что такое формальная верификация и как она выполняется.
KeY — это платформа дедуктивной верификации однопоточных программ на Java и JavaCard. Она позволяет доказать корректность программ по заданной спецификации. Грубо говоря, спецификация состоит из предусловий (в терминах KeY — requires) и постусловий (в терминах KeY — ensures). Спецификации задаются перед методами, которые их реализуют (например, перед упомянутым выше mergeCollapse()). Спецификация метода также называется его контрактом.
В случае сортировки предусловие просто утверждает, что на вход подаётся непустой массив, а постусловие требует, чтобы результирующий массив был сортирован и являлся перестановкой входного. Система KeY доказывает, что если верифицируемый метод вызвать с входными данными, которые удовлетворяют предусловиям, то метод завершится нормально и результирующее состояние будет удовлетворять постусловию. Это также называется полной корректностью, потому что доказывается и нормальное завершение метода. Как мы увидели, метод java.utils.Array.sort() из OpenJDK не соблюдает этот контракт, потому что для определённых входных данных он завершается исключением.
Дополнительно используются инварианты классов и объектов, чтобы указать общие ограничения на значения полей. Обычно проверяется согласованность данных или граничные условия:
Этот инвариант говорит, что длины массивов runBase и runLen должны совпадать, но в то же время это должны быть два разных массива. Семантика инвариантов подразумевает, что каждый метод на выходе должен не только обеспечивать постусловия своего контракта, но и инварианты его собственного объекта “this”.
В качестве языка спецификаций KeY использует Java Modeling Language (JML). Выражения на нём пишутся как на обычном языке Java, поэтому Java-программисты его легко освоят. Главное расширение JML — это кванторы (\forall T x — для любого T, \exists T x — существует T) и, конечно, специальные ключевые слова для контрактов. Спецификации JML приводятся в комментариях java-файлов перед кодом, к которому они относятся. Ниже приведён простой пример Java-метода с JML-спецификацией:
Контракт minRunLength() содержит одно предусловие: входной параметр должен быть не меньше, чем MIN_MERGE. В этом случае (и только в этом) метод обещает завершиться нормально (не зациклиться и не выбросить исключение) и вернуть значение, которое больше или равно MIN_MERGE/2. Дополнительно метод помечен как pure (чистый). Это означает, что метод не модифицирует кучу.
Ключевой момент в том, что система KeY способна статически доказать контракты подобных методов для любых входных параметров. Как это возможно? KeY производит символьное выполнение верифицируемого метода, то есть, выполняет его, используя символьные значения, так что учитываются все возможные пути выполнения. Но этого недостаточно, потому что символьное выполнение циклов с нефиксированным числом итераций (таких как цикл в mergeCollapse(), где мы не знаем значение stackSize) никогда не завершится. Чтобы символьное выполнение циклов стало конечным, используется логика инвариантов. Например, вышеприведённый метод minRunLength() содержит цикл, спецификация которого выражена инвариантом цикла. Инвариант утверждает, что после каждой итерации выполняется условие
В общем, для формальной верификации недостаточно контрактов методов. Необходимо также приводить инварианты циклов. Иногда очень непросто придумать инвариант, который соблюдается в цикле и при этом достаточно силён, чтобы из него вывести постусловие метода. Без инструментальной поддержки и технологии автоматизированного доказательства теорем вряд ли возможно составить правильные инварианты циклов в нетривиальных программах. На самом деле именно здесь и кроется ошибка создателей Timsort. При определённых условиях цикл в mergeCollapse нарушает следующий инвариант класса Timsort (смотрите раздел 1.3 Баг Timsort шаг за шагом):
Этот инвариант утверждает, что runLen[i] должно быть больше, чем сумма двух последующих элементов, для любых неотрицательных i, меньших stackSize-4. Инвариант не восстанавливается и после цикла, поэтому весь метод mergeCollapse не сохраняет инвариант класса. Следовательно, инвариант цикла не такой строгий, как предполагали разработчики. Это мы и обнаружили в процессе нашей попытки верифицировать Timsort с помощью KeY. Без специального инструмента обнаружить это было бы почти невозможно.
Хотя JML и очень похож на Java, это полноценный язык программирования по контракту, подходящий для полной функциональной верификации Java-программ.
Упрощённая версия контракта, который по задумке авторов должен соблюдаться в mergeCollapse, приведена ниже.
Две формулы в ensures подразумевают, что когда mergeCollapse завершается, все серии удовлетворяют инварианту, приведённому в разделе 1.2. Мы уже видели, что этот контракт не выполняется в текущей реализации mergeCollapse (раздел 1.3). Теперь мы приводим исправленную версию, которая соблюдает контракт:
Основная идея этой версии — проверять, что инвариант соблюдается для четырёх последних серий в runLen вместо трёх. Как мы увидим ниже, этого достаточно, чтобы длины всех серий удовлетворяли инварианту после завершения mergeCollapse.
Первый шаг в доказательстве контракта для исправленной версии mergeCollapse — это найти подходящий инвариант цикла. Вот его упрощённая версия:
Интуитивно инвариант цикла утверждает, что все серии кроме, возможно, последних четырёх, удовлетворяют условию. При этом заметим, что цикл завершается (по оператору break), только если последние четыре серии тоже ему удовлетворяют. Таким образом, можно гарантировать, что все серии удовлетворяют инварианту.
Когда мы подаём на вход KeY исправленную версию mergeCollapse вместе с контрактом и инвариантом цикла, система производит символьное выполнение цикла и генерирует условия верификации: формулы, из истинности которых следует, что контракт mergeCollapse выполняется. Следующая (упрощённая) формула показывает главное условие доказательства корректности mergeCollapse, сгенерированное KeY:
Формула утверждает, что из условий в скобках, которые истинны после завершения цикла, должно следовать постусловие mergeCollapse. Понятно, откуда взялись выражения в скобках: оператор break, который завершает цикл, выполняется только когда они все истинны. Мы формально доказали эту формулу (и все прочие условия верификации) с помощью KeY в полуавтоматическом режиме. Ниже приведён набросок доказательства:
Доказательство. Формула runLen[stackSize-2] > runLen[stackSize-1] из постусловия mergeCollapse прямо следует из n >= 0 ==> runLen[n] > runLen[n+1].
Докажем следующую формулу:
\forall int i; 0<=i && i<stackSize-2; runLen[i] > runLen[i+1] + runLen[i+2].
Возможны следующие варианты значения i:
Это доказательство показывает, что новая версия mergeCollapse завершается только когда все серии удовлетворяют инварианту.
Наш анализ ошибки (включая исправление mergeCollapse) был отправлен, рассмотрен и принят в багтрекер Java.
Баг присутствует как минимум в версии Java для Android, OpenJDK и OracleJDK: во всех используется одинаковый код Timsort. Также баг присутствует в Python. В следующих разделах приводятся оригинальная и исправленная версии.
Как было сказано выше, идея исправления очень проста: проверять, что инвариант выполняется для последних четырёх серий в runLen, а не только для трёх.
Timsort для Python (написан на C с использованием Python API) доступен в репозитории subversion – Алгоритм также описан здесь.
Версия Timsort для Java была портирована с CPython. Версия на CPython содержит ошибку, разработанная для поддержки массивов вплоть до 264 элементов, также содержит ошибку. Однако на современных машинах вызвать ошибку переполнения массива невозможно: алгоритм выделяет 85 элементов для runLen, и этого хватает (как показывает наш анализ в полной статье) для массивов, содержащих не более 249 элементов. Для сравнения, мощнейший на сегодняшний день суперкомпьютер Tianhe-2 обладает 250 байтами памяти.
Ошибка полностью аналогична ошибке в Python:
Исправление аналогично приведённому выше для Python.
[UPDATE 26/2: мы изменили код по сравнению с исходной версией статьи. Старый код был эквивалентен, но содержал избыточную проверку и отличался по стилю. Спасибо всем, кто обратил внимание!]
При попытке верифицировать Timsort нам не удалось установить инвариант объекта сортировки. Анализируя причины неудачи, мы обнаружили в реализации Timsort ошибку, которая приводит к ArrayOutOfBoundsException для определённых входных данных. Мы предложили исправление ошибочного метода (без ощутимого снижения производительности) и формально доказали, что исправление корректно и ошибки больше нет.
Из этой истории, помимо собственно найденной ошибки, можно сделать несколько наблюдений.
Какие из этого следуют выводы? Мы были бы счастливы, если бы наша работа послужила начальной точкой для более тесного взаимодействия между исследователями формальных методов и разработчиками открытых программных платформ. Формальные методы уже успешно применяются в Amazon и Facebook. Современные языки формальной спецификации и инструменты формальной верификации не являются такими уж запутанными и суперсложными в изучении. Постоянно улучшается их юзабилити и автоматизация. Но нам нужно больше людей, которые бы пробовали, тестировали и использовали наши инструменты. Да, потребуются некоторые усилия, чтобы начать писать формальные спецификации и верифицировать код, но это не сложнее, чем, например, разобраться, как использовать компилятор или средство сборки проектов. Но речь идёт о днях или неделях, а не месяцах или годах. Ну как, вы принимаете вызов?
С наилучшими пожеланиями,
Стайн де Гув, Юриан Рот, Франк де Бур, Ричард Бубель и Райнер Хенле.
Работа частично поддержана проектом седьмой рамочной программы Евросоюза FP7-610582 ENVISAGE: Engineering Virtualized Services.
Эта статья не была бы написана без поддержки и вежливых напоминаний Амунда Твейта! Также мы хотим поблагодарить Беруза Нобакта за то, что предоставил нам видео, демонстрирующее ошибку.
Тим Петерс разработал гибридный алгоритм сортировки Timsort в 2002 году. Алгоритм представляет собой искусную комбинацию идей сортировки слиянием и сортировки вставками и заточен на эффективную работу с реальными данными. Впервые Timsort был разработан для Python, но затем Джошуа Блох (создатель коллекций Java, именно он, кстати, отметил, что большинство алгоритмов двоичного поиска содержит ошибку) портировал его на Java (методы java.util.Collections.sort и java.util.Arrays.sort). Сегодня Timsort является стандартным алгоритмом сортировки в Android SDK, Oracle JDK и OpenJDK. Учитывая популярность этих платформ, можно сделать вывод, что счёт компьютеров, облачных сервисов и мобильных устройств, использующих Timsort для сортировки, идёт на миллиарды.
Но вернёмся в 2015-й год. После того как мы успешно верифицировали Java-реализации сортировки подсчётом и поразрядной сортировки (J. Autom. Reasoning 53(2), 129-139) нашим инструментом формальной верификации под названием KeY, мы искали новый объект для изучения. Timsort казался подходящей кандидатурой, потому что он довольно сложный и широко используется. К сожалению, мы не смогли доказать его корректность. Причина этого при детальном рассмотрении оказалась проста: в реализации Timsort есть баг. Наши теоретические исследования указали нам, где искать ошибку (любопытно, что ошибка была уже в питоновской реализации). В данной статье рассказывается, как мы этого добились.
Статья с более полным анализом, а также несколько тестовых программ доступны на нашем сайте.
Содержание
- Баг в реализации Timsort на Android, Java и Python
1.1 Воспроизводим баг Timsort на Java
1.2 Как в принципе работает Timsort?
1.3 Баг Timsort шаг за шагом - Доказательство (не)корректности Timsort
2.1 Система верификации KeY
2.2 Исправление и его формальная спецификация
2.3 Анализ результатов работы KeY - Предложенные исправления бага к реализациям Timsort на Python и Android/Java
3.1 Некорректная функция merge_collapse (Python)
3.2 Исправленная функция merge_collapse (Python)
3.3 Некорректная функция mergeCollapse (Java/Android)
3.4 Исправленная функция mergeCollapse (Java/Android) - Заключение: какие из этого следуют выводы?
1. Баг в реализации Timsort на Android, Java и Python
Так в чём же заключается баг? И почему бы вам не попробовать воспроизвести его самим?
1.1 Воспроизводим баг Timsort на 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?
Тimsort — это гибридный алгоритм, который использует сортировку вставкой и сортировку слиянием.
Алгоритм переупорядочивает входной массив слева направо, находя в нём последовательные (неперекрывающиеся) сортированные сегменты («серии», или runs). Если серия короче определённой минимальной длины, она дополняется последующими элементами и сортируется вставкой. Длины созданных серий добавляются в конец массива runLen. Когда новая серия добавляется в runLen, метод mergeCollapse сливает серии, пока три последних элемента в runLen не будут удовлетворять следующей паре условий, которая называется «инвариантом»:
- runLen [n-2] > runLen [n-1] + runLen [n]
- runLen [n-1] > runLen [n]
Здесь n — это индекс последней серии в runLen. Идея была в том, что проверка этого инварианта для последних трёх серий гарантирует, что все последовательные тройки серий будут ему удовлетворять. В конце сливаются все серии, что даёт в результате полностью отсортированный входной массив.
Из соображений эффективности желательно выделить как можно меньше памяти под runLen, но её должно быть достаточно, чтобы туда заведомо поместились все серии. Если инвариант выполняется для всех серий, длина серий будет расти экспоненциально (даже быстрее, чем числа Фибоначчи: длина каждой серии строго больше суммы длин двух последующих). Так как серии не перекрываются, их потребуется не так много, чтобы полностью отсортировать даже огромный входной массив.
1.3 Баг Timsort шаг за шагом
Из следующего фрагмента кода видно, что реализация mergeCollapse проверяет инвариант для последних трёх серий в runLen:
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; // инвариант установлен
}
}
}
К сожалению, этого не достаточно, чтобы все серии удовлетворяли инварианту. Предположим, что runLen содержит такой набор длин перед выполнением mergeCollapse (n=4):
120, 80, 25, 20, 30На первом проходе цикла while будут объединены серии длиной 25 и 20 (так как 25 < 20 + 30 и 25 < 30):
120, 80, 45, 30На втором проходе цикла (теперь n=3), мы определяем, что инвариант установлен для последних трёх серий, потому что 80 > 45 + 30 и 45 > 30, поэтому mergeCollapse завершает работу. Но mergeCollapse не восстановил инвариант для всего массива: он нарушается в первой тройке, так как 120 < 80 + 45.
Генератор тестов на нашем сайте позволяет выявить эту проблему. Он создаёт входной массив с множеством коротких серий, при этом их длины не удовлетворяют инварианту, что приводит к падению Timsort. Истинная причина ошибки в том, что из-за нарушения инварианта длины серий растут медленнее, чем ожидалось, в результате чего их количество превышает runLen.length и это приводит к ArrayOutOfBoundsException.
2. Доказательство (не)корректности Timsort
Мы обнаружили, что инвариант mergeCollapse нарушается, когда пытались формально верифицировать Timsort. К счастью, мы также поняли, как его исправить. В итоге нам даже удалось верифицировать исправленную версию, в которой инвариант действительно соблюдается. Но не будем спешить. Для начала разберёмся, что такое формальная верификация и как она выполняется.
2.1 Система верификации KeY
KeY — это платформа дедуктивной верификации однопоточных программ на Java и JavaCard. Она позволяет доказать корректность программ по заданной спецификации. Грубо говоря, спецификация состоит из предусловий (в терминах KeY — requires) и постусловий (в терминах KeY — ensures). Спецификации задаются перед методами, которые их реализуют (например, перед упомянутым выше mergeCollapse()). Спецификация метода также называется его контрактом.
В случае сортировки предусловие просто утверждает, что на вход подаётся непустой массив, а постусловие требует, чтобы результирующий массив был сортирован и являлся перестановкой входного. Система KeY доказывает, что если верифицируемый метод вызвать с входными данными, которые удовлетворяют предусловиям, то метод завершится нормально и результирующее состояние будет удовлетворять постусловию. Это также называется полной корректностью, потому что доказывается и нормальное завершение метода. Как мы увидели, метод java.utils.Array.sort() из OpenJDK не соблюдает этот контракт, потому что для определённых входных данных он завершается исключением.
Дополнительно используются инварианты классов и объектов, чтобы указать общие ограничения на значения полей. Обычно проверяется согласованность данных или граничные условия:
/*@ private invariant
@ runBase.length == runLen.length && runBase != runLen;
@*/
Этот инвариант говорит, что длины массивов runBase и runLen должны совпадать, но в то же время это должны быть два разных массива. Семантика инвариантов подразумевает, что каждый метод на выходе должен не только обеспечивать постусловия своего контракта, но и инварианты его собственного объекта “this”.
В качестве языка спецификаций KeY использует Java Modeling Language (JML). Выражения на нём пишутся как на обычном языке Java, поэтому Java-программисты его легко освоят. Главное расширение JML — это кванторы (\forall T x — для любого T, \exists T x — существует T) и, конечно, специальные ключевые слова для контрактов. Спецификации JML приводятся в комментариях java-файлов перед кодом, к которому они относятся. Ниже приведён простой пример Java-метода с JML-спецификацией:
/*@ 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() содержит одно предусловие: входной параметр должен быть не меньше, чем MIN_MERGE. В этом случае (и только в этом) метод обещает завершиться нормально (не зациклиться и не выбросить исключение) и вернуть значение, которое больше или равно MIN_MERGE/2. Дополнительно метод помечен как pure (чистый). Это означает, что метод не модифицирует кучу.
Ключевой момент в том, что система KeY способна статически доказать контракты подобных методов для любых входных параметров. Как это возможно? KeY производит символьное выполнение верифицируемого метода, то есть, выполняет его, используя символьные значения, так что учитываются все возможные пути выполнения. Но этого недостаточно, потому что символьное выполнение циклов с нефиксированным числом итераций (таких как цикл в mergeCollapse(), где мы не знаем значение stackSize) никогда не завершится. Чтобы символьное выполнение циклов стало конечным, используется логика инвариантов. Например, вышеприведённый метод minRunLength() содержит цикл, спецификация которого выражена инвариантом цикла. Инвариант утверждает, что после каждой итерации выполняется условие
n >= MIN_MERGE/2 && r >= 0 && r <= 1, и из этого можно доказать постусловие всего метода. Аннотация decreases (уменьшается) используется, чтобы доказать завершение цикла. В ней указывается выражение, значение которого неотрицательно и строго уменьшается. Конструкция assignable перечисляет объекты кучи, которые могут быть изменены в цикле. Ключевое слово \nothing означает, что куча не модифицируется. И действительно: цикл изменяет только локальную переменную r и аргумент n.В общем, для формальной верификации недостаточно контрактов методов. Необходимо также приводить инварианты циклов. Иногда очень непросто придумать инвариант, который соблюдается в цикле и при этом достаточно силён, чтобы из него вывести постусловие метода. Без инструментальной поддержки и технологии автоматизированного доказательства теорем вряд ли возможно составить правильные инварианты циклов в нетривиальных программах. На самом деле именно здесь и кроется ошибка создателей Timsort. При определённых условиях цикл в mergeCollapse нарушает следующий инвариант класса Timsort (смотрите раздел 1.3 Баг Timsort шаг за шагом):
/*@ private invariant
@ (\forall int i; 0<=i && i<stackSize-4;
@ runLen[i] > runLen[i+1] + runLen[i+2]))
@*/
Этот инвариант утверждает, что runLen[i] должно быть больше, чем сумма двух последующих элементов, для любых неотрицательных i, меньших stackSize-4. Инвариант не восстанавливается и после цикла, поэтому весь метод 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()
Две формулы в ensures подразумевают, что когда 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);
}
}
Основная идея этой версии — проверять, что инвариант соблюдается для четырёх последних серий в runLen вместо трёх. Как мы увидим ниже, этого достаточно, чтобы длины всех серий удовлетворяли инварианту после завершения 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])
@*/
Интуитивно инвариант цикла утверждает, что все серии кроме, возможно, последних четырёх, удовлетворяют условию. При этом заметим, что цикл завершается (по оператору break), только если последние четыре серии тоже ему удовлетворяют. Таким образом, можно гарантировать, что все серии удовлетворяют инварианту.
2.3 Анализ результатов работы KeY
Когда мы подаём на вход KeY исправленную версию mergeCollapse вместе с контрактом и инвариантом цикла, система производит символьное выполнение цикла и генерирует условия верификации: формулы, из истинности которых следует, что контракт mergeCollapse выполняется. Следующая (упрощённая) формула показывает главное условие доказательства корректности mergeCollapse, сгенерированное KeY:
Формула утверждает, что из условий в скобках, которые истинны после завершения цикла, должно следовать постусловие mergeCollapse. Понятно, откуда взялись выражения в скобках: оператор break, который завершает цикл, выполняется только когда они все истинны. Мы формально доказали эту формулу (и все прочие условия верификации) с помощью KeY в полуавтоматическом режиме. Ниже приведён набросок доказательства:
Доказательство. Формула runLen[stackSize-2] > runLen[stackSize-1] из постусловия mergeCollapse прямо следует из 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. Предложенные исправления бага к реализациям Timsort на Python и Android/Java
Наш анализ ошибки (включая исправление mergeCollapse) был отправлен, рассмотрен и принят в багтрекер Java.
Баг присутствует как минимум в версии Java для Android, OpenJDK и OracleJDK: во всех используется одинаковый код Timsort. Также баг присутствует в Python. В следующих разделах приводятся оригинальная и исправленная версии.
Как было сказано выше, идея исправления очень проста: проверять, что инвариант выполняется для последних четырёх серий в runLen, а не только для трёх.
3.1 Некорректная функция merge_collapse (Python)
Timsort для Python (написан на C с использованием Python API) доступен в репозитории subversion – Алгоритм также описан здесь.
Версия Timsort для Java была портирована с CPython. Версия на CPython содержит ошибку, разработанная для поддержки массивов вплоть до 264 элементов, также содержит ошибку. Однако на современных машинах вызвать ошибку переполнения массива невозможно: алгоритм выделяет 85 элементов для runLen, и этого хватает (как показывает наш анализ в полной статье) для массивов, содержащих не более 249 элементов. Для сравнения, мощнейший на сегодняшний день суперкомпьютер Tianhe-2 обладает 250 байтами памяти.
/* 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.
[UPDATE 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. Заключение: какие из этого следуют выводы?
При попытке верифицировать Timsort нам не удалось установить инвариант объекта сортировки. Анализируя причины неудачи, мы обнаружили в реализации Timsort ошибку, которая приводит к ArrayOutOfBoundsException для определённых входных данных. Мы предложили исправление ошибочного метода (без ощутимого снижения производительности) и формально доказали, что исправление корректно и ошибки больше нет.
Из этой истории, помимо собственно найденной ошибки, можно сделать несколько наблюдений.
- Зачастую программисты считают формальные методы непрактичными и/или далёкими от реальных задач. Это не так: мы нашли и исправили ошибку в программном обеспечении, которым пользуются миллиарды пользователей каждый день. Как показал наш анализ, найти и исправить такой баг без формального анализа и инструмента для верификации было бы практически невозможно. Ошибка долгие годы жила в стандартной библиотеке языков Java и Python. Её проявления замечали ранее и даже думали, что исправили, но в действительности добились только того, что ошибка стала возникать реже.
- Хотя маловероятно, что такая ошибка возникнет случайно, легко представить, как можно её использовать для атаки. Вероятно, в стандартных библиотеках популярных языков программирования кроются и другие незамеченные ошибки. Может быть, стоит заняться их поиском до того как они причинят вред или будут использованы злоумышленниками?
- Реакция разработчиков Java на наш отчёт в некотором смысле разочаровывает. Вместо того, чтобы использовать нашу исправленную (и верифицированную!) версию mergeCollapse(), они предпочли увеличить выделенный размер runLen до «достаточного» размера. Как мы показали, вовсе не обязательно было так делать. Но теперь каждый, кто использует java.utils.Collection.sort() будет вынужден тратить больше памяти. Учитывая астрономическое число программ, использующих настолько базовую функцию, это приведёт к заметным дополнительным затратам энергии. Мы можем только догадываться, почему не было принято наше решение: возможно разработчики JDK не удосужились прочитать наш отчёт полностью и поэтому не поняли суть исправления и решили не полагаться на него. В конце концов, OpenJDK разрабатывает сообщество, в значительной степени состоящее из добровольцев, у которых не так много времени.
Какие из этого следуют выводы? Мы были бы счастливы, если бы наша работа послужила начальной точкой для более тесного взаимодействия между исследователями формальных методов и разработчиками открытых программных платформ. Формальные методы уже успешно применяются в Amazon и Facebook. Современные языки формальной спецификации и инструменты формальной верификации не являются такими уж запутанными и суперсложными в изучении. Постоянно улучшается их юзабилити и автоматизация. Но нам нужно больше людей, которые бы пробовали, тестировали и использовали наши инструменты. Да, потребуются некоторые усилия, чтобы начать писать формальные спецификации и верифицировать код, но это не сложнее, чем, например, разобраться, как использовать компилятор или средство сборки проектов. Но речь идёт о днях или неделях, а не месяцах или годах. Ну как, вы принимаете вызов?
С наилучшими пожеланиями,
Стайн де Гув, Юриан Рот, Франк де Бур, Ричард Бубель и Райнер Хенле.
Благодарности
Работа частично поддержана проектом седьмой рамочной программы Евросоюза FP7-610582 ENVISAGE: Engineering Virtualized Services.
Эта статья не была бы написана без поддержки и вежливых напоминаний Амунда Твейта! Также мы хотим поблагодарить Беруза Нобакта за то, что предоставил нам видео, демонстрирующее ошибку.