Хабрахабр

[Перевод] SMT-решатель на iPhone

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

Википедия Задача выполнимости формул в теориях (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.

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

Об этом я сообщил в твиттере, но твиттер не оставляет много места для подробностей, поэтому изложу их здесь: В этом 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, несмотря на меньшее время на экране.

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

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

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

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

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

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

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

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

Бьюсь об заклад, что A12X в новом iPad Pro ещё быстрее благодаря большему тепловому конверту, который даёт планшет. 2. ↑

Теги
Показать больше

Похожие статьи

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»
Закрыть