Зачем покупать дорогой ПК, если ваш iPhone быстрее решает SMT?

Задача выполнимости формул в теориях (satisfiability modulo theories, SMT) — это задача разрешимости для логических формул с учётом лежащих в их основе теорий. — Википедия

Несколько дней назад я написал в твиттере ^[1]: «Любопытный эксперимент: на новом iPhone прувер Z3 работает быстрее, чем на моём (довольно дорогом) десктопном Intel. Пора перевести все формальные методы исследований на телефон».

Я читал о невероятном прогрессе, которого добились разработчики процессоров Apple ^[4], и что скоро маки переведут на собственные ARM-процессоры от Apple ^[5]. Эти отчёты обычно ссылаются на некоторые кросс-платформенные тесты, такие как Geekbench ^[6] для демонстрации, что мобильные процессоры Apple не уступают мобильным и настольным процессорам Intel. Но я всегда немного скептически относился к этим кросс-платформенным тестам (как и к другим ^[7]) — действительно ли они отражают скорость выполнения реальных задач, для которых я использую свои Mac?

Как исследователю формальных методов, мне регулдярно приходится запускать SMT-решатель, обычно это прувер Z3 ^[8]. Я потратил немало времени на изучение характеристик производительности Z3. У него есть некоторые особенности, которые не учитываются в тестах (Z3 обычно однопоточный). Недавно я купил новый iPhone XS ^[9] с последним процессором A12 ^[10] от Apple. И как-то от нечего делать решил скомпилировать Z3 в iOS и посмотреть, насколько быстро работает новый телефон (или гипотетический будущий Mac).

Первый тест

Кросс-компиляция Z3 оказалась на удивление простой, необходимо изменить всего несколько строчек кода. Я выложил исходники для запуска Z3 на вашем собственном устройстве iOS ^[11]. Для теста я взял несколько запросов из своей недавней работы по профилированию символических вычислений ^[12]: для каждого случая извлечена выдача SMT, сгенерированная Rosette ^[13].

В первом тесте я сравнил iPhone XS с одним из десктопов, который работает на Intel Core i7-7700K — лучший чип Intel для потребительского рынка на тот момент, когда я собирал машину 18 месяцев назад. Предполагалось, что Intel выиграет без особых проблем, но вышло иначе:

В этом 23-секундном тесте iPhone XS оказался примерно на 11% быстрее! Об этом я сообщил в твиттере, но твиттер не оставляет много места для подробностей, поэтому изложу их здесь:

• Данный бенчмарк — фрагмент QF_BV из SMT, поэтому Z3 решает эту часть с помощью трансляции (bit-blasting) и SAT-солвера.
• Результат вполне устойчив, даже если прогнать цикл десять раз: iPhone поддерживает эту производительность и вроде бы не начинает тормозить из-за перегрева.^{1 [14]}. Тем не менее, бенчмарк всё-таки довольно скоротечный.
• Несколько человек спросили, связано ли это с недетерминизмом? Возможно, на разных платформах решатель идёт разным путём из-за использования случайных чисел или по другой причине? Но я довольно тщательно проверил подробную выдачу Z3, и вряд ли результаты можно объяснить этим.
• Обе системы запускали Z3 4.8.1, который я скомпилировал с помощью Clang с одинаковыми настройками оптимизации. Я также запускал тесты на i7-7700K с готовыми бинарниками Z3 (которые скомпилированы GCC), но они ещё медленнее.

Что происходит?

Как такое возможно? Core i7-7700K — это же десктопный процессор. На однопоточной задаче он потребляет около 45 ватт и работает на частоте 4,5 ГГц. С другой стороны телефон iPhone, отключенный от сети. Вероятно, он не потребляет и 10% этой мощности и работает (мы надеемся) где-то в диапазоне 2 ГГц. Более того, после сравнительного теста я проверил отчёт об использовании батареи iPhone: там говорилось, что Slack использовал в 4 раза больше энергии, чем приложение Z3, несмотря на меньшее время на экране.

Apple не предоставляет достаточно информации, чтобы понять производительность Z3 на iPhone, но, к счастью, Intel даёт эти сведения для своего процессора. Я некоторое время покопался в VTune ^[15], чтобы найти узкие места производительности при запуске Z3 на десктопе. Как отметил Мэйт Соос ^[16], основное время SAT-решатель тратит на распространение ^[17], которое очень чувствительно к кэшу ^[18]. VTune соглашается и говорит, что Z3 тратит много времени на ожидание в памяти при переборе наблюдаемых литералов. Таким образом, ключом к производительности, кажется, является размер кэша и задержка памяти. Этот эффект может объяснить, почему iPhone настолько силён в этом тесте: у чипа A12 гигантский кэш L2 с низкой задержкой ^[19], а также, похоже, лучшая задержка памяти после промаха кэша по сравнению с 7700K.

Стремительный прогресс процессоров Apple

Чтобы подтвердить результаты, я провёл более обширный эксперимент, собрав все устройства Apple, которые смог достать. Я также выбрал примерно в 10 раз более продолжительный бенчмарк (т.е. 4 минуты на десктопе), чтобы снять опасения по поводу всплесков производительности мобильного CPU.

Вот результаты для этих устройств (с указанием дат их выпуска) относительно A7, первого 64-разрядного пользовательского процессора от Apple:

Сразу нужно отметить, что настольный процессор i7-7700K превосходит iPhone XS на этом более длинном тесте. Но iPhone невероятно конкурентоспособен, показывая результат между i7-7700K и его предшественником i7-6700K, который был самым быстрым потребительским настольным процессором чуть менее двух лет назад.

По приколу я добавил ещё процессор Core m7-6Y75 из своего макбука 2016 года. В тесте Z3 мой телефон примерно на 50% быстрее, чем ноутбук.

Действительно примечательной вещью здесь является тенденция: довольно последовательное улучшение на 30% в год для этого бенчмарка Z3. Очевидно, что не следует делать далекоидущие выводы из одного глупого теста, но похоже, что через пару итераций процессоры Apple станут вполне пригодны для рабочих нагрузок.^{2 [20]}. Я честно не ожидал, что мы уже так близко: современные архитектуры смартфонов просто невероятны!

Спасибо Меган Коуэн ^[21], Максу Уиллси ^[22] и Эдди Яну ^[23] за помощь в проведении тестов на других устройствах.

---

Макс ^[22] обратил внимание, что iPhone водонепроницаем, поэтому теорию можно проверить, погрузив его в ледяную ванну. Но я заплатил много денег за телефон и не хочу добровольно проводить такой опыт. ↑ ^[24]

iPad Pro ^[25] ещё быстрее благодаря большему ↑ ^[26]

Автор: m1rko

Источник ^[27]