Доказ некоректність алгоритму сортування Android, Java і Python

Тім Петерс розробив гібридний алгоритм сортування 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 є баг. Наші теоретичні дослідження вказали нам, де шукати помилку (цікаво, що помилка була вже в питоновской реалізації). У цій статті розповідається, як ми цього домоглися.

Стаття з більш повним аналізом, а також кілька тестових програм доступні на нашому сайті.

Зміст
  1. Баг в реалізації Timsort на Android, Java і Python
    1.1 Відтворюємо баг Timsort на Java
    1.2 Як в принципі працює Timsort?
    1.3 Баг Timsort крок за кроком
  2. Доказ (не)коректності Timsort
    2.1 Система верифікації KeY
    2.2 Виправлення і його формальна специфікація
    2.3 Аналіз результатів роботи KeY
  3. Запропоновані виправлення бага до реалізацій Timsort на Python і Android/Java
    3.1 Некоректна функція merge_collapse (Python)
    3.2 Виправлена функція merge_collapse (Python)
    3.3 Некоректна функція mergeCollapse (Java/Android)
    3.4 Виправлена функція mergeCollapse (Java/Android)
  4. Висновок: які з цього випливають висновки?
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 не будуть задовольняти наступній парі умов, яка називається «інваріантної:

  1. runLen [n-2] > runLen [n-1] + runLen [n]
  2. 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 — потрібно) і марнослівями (в термінах 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 (написаний на Python з використанням API) доступний в репозиторії subversion — Алгоритм також описаний тут.

Версія Timsort для Java була портована з CPython. Версія CPython містить помилку, розроблена для підтримки масивів аж до 264 елементів, також містить помилку. Однак на сучасних машинах викликати помилку переповнення масиву неможливо: алгоритм виділяє 85 елементів для runLen, і цього вистачає (як показує наш аналіз у повній статті) для масивів, що містять не більше 249 елементів. Для порівняння, найпотужніший на сьогоднішній день суперкомп'ютер Tianhe-2 має 250 байтами пам'яті.

/* The maximum number of entries in a s MergeState' 
* 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 смішного 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 для певних вхідних даних. Ми запропонували виправлення помилкового методу (без відчутного зниження продуктивності) і формально довели, що виправлення коректно і помилки більше немає.

З цієї історії, крім власне знайденої помилки, можна зробити кілька спостережень.
  1. Часто програмісти вважають формальні методи непрактичними і/або далекими від реальних завдань. Це не так: ми знайшли і виправили помилку у програмному забезпеченні, яким користуються мільярди користувачів щодня. Як показав наш аналіз, знайти і виправити такий баг без формального аналізу та інструменту для верифікації було б практично неможливо. Помилка довгі роки жила в стандартній бібліотеці мов Java і Python. Її прояви помічали раніше та навіть думали, що виправили, але в дійсності добилися тільки того, що помилка стала виникати рідше.
  2. Хоча малоймовірно, що така помилка виникне випадково, легко уявити, як можна її використовувати для атаки. Ймовірно, в стандартних бібліотеках популярних мов програмування криються та інші непомічені помилки. Може бути, варто зайнятися пошуком до того, як вони завдадуть шкоди або будуть використані зловмисниками?
  3. Реакція розробників Java на наш звіт в деякому сенсі розчаровує. Замість того, щоб використовувати нашу виправлену (і верифицированную!) версію mergeCollapse(), вони зволіли збільшити виділений розмір runLen до «достатнього розміру. Як ми показали, зовсім не обов'язково було так робити. Але тепер кожен, хто використовує java.utils.Collection.sort() буде змушений витрачати більше пам'яті. Враховуючи астрономічне число програм, що використовують настільки базову функцію, це призведе до помітних додаткових витрат енергії. Ми можемо тільки здогадуватися, чому не було прийнято наше рішення: можливо розробники JDK не спромоглися прочитати наш звіт повністю і тому не зрозуміли суть виправлення і вирішили не покладатися на нього. Зрештою, OpenJDK розробляє спільнота, в значній мірі складається з добровольців, у яких не так багато часу.


Які з цього випливають висновки? Ми були б щасливі, якби наша робота послужила відправною точкою для більш тісної взаємодії між дослідниками формальних методів і розробниками відкритих програмних платформ. Формальні методи вже успішно застосовуються в Amazon і Facebook. Сучасні мови формальної специфікації та інструменти формальної верифікації є такими заплутаними і суперскладних у вивченні. Постійно поліпшується їх юзабіліті і автоматизація. Але нам потрібно більше людей, які б пробували, тестували і використовували наші інструменти. Так, будуть потрібні деякі зусилля, щоб почати писати формальні специфікації та верифікувати код, але це не складніше, ніж, наприклад, розібратися, як використовувати компілятор або засіб складання проектів. Але мова йде про дні чи тижні, а не місяцях або роках. Ну як, ви приймаєте виклик?

З найкращими побажаннями,
Стайн де Гув, Юриан Рот, Франк де Бур, Річард Бубель і Райнер Хенле.

Подяки

Робота частково підтримана проектом сьомої рамкової програми Євросоюзу FP7-610582 ENVISAGE: Engineering Virtualized Services.
Ця стаття не була б написана без підтримки і ввічливих нагадувань Амунда Твейта! Також ми хочемо подякувати Беруза Нобакта за те, що надав нам відео, яке демонструє помилку.

Envisage logo

Джерело: Хабрахабр

0 коментарів

Тільки зареєстровані та авторизовані користувачі можуть залишати коментарі.