Доказали самое видное утверждение сортировки — цена при работе не сдвинулась: платит не оно
«Сортировать» из flang/stdlib/lists.flang несёт два утверждения, и после правки ядра 20 августа одно из них — «сортировка не теряет и не добавляет элементов» — стало доказанным, а значит его проверка перестала печататься в код. Ожидание было, что цена утверждений на сортировке упадёт. Она не упала вовсе.
Сортировка вставками, 1500 чисел, 20 прогонов, напечатанный C, по три замера, разброс меньше 2 %:
| что стоит в программе | время | во сколько раз медленнее «без утверждений» |
|---|---|---|
| утверждений нет вовсе | 0,57 с | 1,00 |
| только «сортировка не теряет и не добавляет элементов» | 0,57 с | 1,00 |
только «во главе результата встало меньшее…» у «Вставить по порядку» | 1,70 с | 2,98 |
| оба плюс «наименьшее переживает сортировку» (как в библиотеке) | 1,72 с | 3,02 |
Разложение объясняет всё. Снятая проверка считается РОВНО СТОЛЬКО РАЗ, СКОЛЬКО ВЫЗВАНА ФУНКЦИЯ, при которой она написана: «Сортировать» зовут 20 раз, и 20 раз посчитать длину полутора тысяч звеньев стоит ноль на фоне задачи. А «Вставить по порядку» при тех же входах зовут около 22 миллионов раз — 1500 внешних вызовов, и каждый рекурсирует вглубь до 1500, — и её проверка одна съедает все 1,13 с надбавки.
Правило для следующего раза. Прежде чем доказывать ради скорости, посчитай, СКОЛЬКО РАЗ зовут функцию, при которой утверждение написано. Цена утверждения есть цена одной проверки, умноженная на число вызовов; доказательство утверждения о внешней функции обёртки не трогает внутренний цикл вовсе. Самое видное утверждение почти всегда написано при внешней функции.
Чем подтверждено. Ветка u/svyortka, основание ff8ad5d0. Двоичные до и после правки, одна и та же программа, flang emit … --target c плюс make; вход — 1500 чисел линейного конгруэнтного генератора, «Прогон» зовёт «Сортировать» 20 раз. Снятие проверки видно не по времени, а по печати: в напечатанном C строки постусловие «сортировка не теряет и не добавляет элементов» больше нет, а постусловие «во главе результата…» на месте.
Чем ограничено. Одна задача (сортировка вставками), одна цель печати (C), одна машина. Утверждение «цена равна цене проверки на число вызовов» здесь не измерено отдельно, а прочитано из разложения выше.
Связано: a-proved-postcondition-no-longer-reaches-printed-code, a-postcondition-runs-on-every-call-so-a-walk-inside-it-changes-the-cost-order, left-fold-is-blocked-because-the-fold-rule-does-not-read-the-callee-postcondition