Задача выполнимости формул в теориях (satisfiability modulo theories, SMT) — это задача разрешимости для логических формул с учётом лежащих в их основе теорий. — Википедия
Несколько дней назад я написал в твиттере: «Любопытный эксперимент: на новом iPhone прувер Z3 работает быстрее, чем на моём (довольно дорогом) десктопном Intel. Пора перевести все формальные методы исследований на телефон».
Я читал о невероятном прогрессе, которого добились разработчики процессоров Apple, и что скоро маки переведут на собственные ARM-процессоры от Apple. Эти отчёты обычно ссылаются на некоторые кросс-платформенные тесты, такие как Geekbench для демонстрации, что мобильные процессоры Apple не уступают мобильным и настольным процессорам Intel. Но я всегда немного скептически относился к этим кросс-платформенным тестам (как и к другим) — действительно ли они отражают скорость выполнения реальных задач, для которых я использую свои Mac?
Как исследователю формальных методов, мне регулдярно приходится запускать SMT-решатель, обычно это прувер Z3. Я потратил немало времени на изучение характеристик производительности Z3. У него есть некоторые особенности, которые не учитываются в тестах (Z3 обычно однопоточный). Недавно я купил новый iPhone XS с последним процессором A12 от Apple. И как-то от нечего делать решил скомпилировать Z3 в iOS и посмотреть, насколько быстро работает новый телефон (или гипотетический будущий Mac).
Кросс-компиляция Z3 оказалась на удивление простой, необходимо изменить всего несколько строчек кода. Я выложил исходники для запуска Z3 на вашем собственном устройстве iOS. Для теста я взял несколько запросов из своей недавней работы по профилированию символических вычислений: для каждого случая извлечена выдача SMT, сгенерированная Rosette.
В первом тесте я сравнил iPhone XS с одним из десктопов, который работает на Intel Core i7-7700K — лучший чип Intel для потребительского рынка на тот момент, когда я собирал машину 18 месяцев назад. Предполагалось, что Intel выиграет без особых проблем, но вышло иначе:
В этом 23-секундном тесте iPhone XS оказался примерно на 11% быстрее! Об этом я сообщил в твиттере, но твиттер не оставляет много места для подробностей, поэтому изложу их здесь:
- Данный бенчмарк — фрагмент
QF_BVиз SMT, поэтому Z3 решает эту часть с помощью трансляции (bit-blasting) и SAT-солвера. - Результат вполне устойчив, даже если прогнать цикл десять раз: iPhone поддерживает эту производительность и вроде бы не начинает тормозить из-за перегрева.1. Тем не менее, бенчмарк всё-таки довольно скоротечный.
- Несколько человек спросили, связано ли это с недетерминизмом? Возможно, на разных платформах решатель идёт разным путём из-за использования случайных чисел или по другой причине? Но я довольно тщательно проверил подробную выдачу 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, чтобы найти узкие места производительности при запуске Z3 на десктопе. Как отметил Мэйт Соос, основное время SAT-решатель тратит на распространение, которое очень чувствительно к кэшу. VTune соглашается и говорит, что Z3 тратит много времени на ожидание в памяти при переборе наблюдаемых литералов. Таким образом, ключом к производительности, кажется, является размер кэша и задержка памяти. Этот эффект может объяснить, почему iPhone настолько силён в этом тесте: у чипа A12 гигантский кэш L2 с низкой задержкой, а также, похоже, лучшая задержка памяти после промаха кэша по сравнению с 7700K.
Чтобы подтвердить результаты, я провёл более обширный эксперимент, собрав все устройства 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. Я честно не ожидал, что мы уже так близко: современные архитектуры смартфонов просто невероятны!
Спасибо Меган Коуэн, Максу Уиллси и Эдди Яну за помощь в проведении тестов на других устройствах.
1. Макс обратил внимание, что iPhone водонепроницаем, поэтому теорию можно проверить, погрузив его в ледяную ванну. Но я заплатил много денег за телефон и не хочу добровольно проводить такой опыт. ↑
2. Бьюсь об заклад, что A12X в новом iPad Pro ещё быстрее благодаря большему тепловому конверту, который даёт планшет. ↑
Комментариев нет:
Отправить комментарий