Задача выполнимости формул в теориях (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
Чтобы подтвердить результаты, я провёл более обширный эксперимент, собрав все устройства 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 ещё быстрее благодаря большему тепловому конверту, который даёт планшет. ^
Комментарии (32)
Alex_ME
10.11.2018 01:04+1Честно говоря, меня эта статья очень озадачила, я бы даже сказал, обескуражила. Я немного поискал на эту тему, на IXBT наткнулся на ссылку на geekbench со сравнением. Поискал еще немного, вот, что нашел.
%name% vs iPhone X
- i5-7200U. Преобладание в single-core и отставание в multi-core (против 2х мощных ядер и 6и слабых?!)
- FX-8320. Отставание в single-core и небольшое преобладание в multi-corе, кроме html и матриц(!)
- Ryzen 1700. Преобладание везде.
- i9-7980XE. Околонулевое преобладание в single-core (кроме матриц, матрицы лучше), ну и значительное преобладание в multi-core.
Я очень сильно удивлен результатами.
Zverienish
11.11.2018 19:06Ну тот же i3 топовые телефоны телефоны уже как минимум год без проблем обгоняют.
advan20092
10.11.2018 09:09Я подозреваю, что есть некий обширный класс задач, на которых производительность мобильных процессоров будет в десятки и сотни раз хуже чем у дескотпных. Просто из-за отсутсвия наборов неких инструкций.
iproger
10.11.2018 14:02AVX, скорее всего.
DaylightIsBurning
10.11.2018 16:31но это не так критично т.к. добавить SIMD пошире несложно, да и графические ядра — более чем достойная SIMD в CPU.
Goodkat
10.11.2018 16:44В вычислениях с плавающей точкой айфон, навернле, будет сильно отставать от десктопа.
Ещё на Intel могли быть установлены патчи от Spectre/Meltdown, которые могли сильно повлиять на скорость обращения к кэшу процессора.
DaylightIsBurning
10.11.2018 18:18+1Вот тут есть детальное сравнение по категориям.
Есть пару задач (sparse Fourier, матричное умножение), в которых A12X в два раза медленней чем i7-7700K, но в основном разница в пределах 20%.
advan20092
10.11.2018 21:32По словам автора оригинальной статьи патчи не должны были снизить производительность больше чем на 1 процент
lokkiuni
12.11.2018 18:35Немного не так — ARM вне пределов этих инструкций проигрывает где-то в 10 раз. И если с целочисленной частью они более-менее на уровне, то обычные инструкции с плавающей точкой, которые не ложатся на спец. блок, выполняются на уровне пентиума 3, в лучшем случае атлона хр, если брать современные высокочастотные процессоры.
Так и в настольнике GPGPU для этого можно включить и наслаждаться 10х ускорением там, где это хорошо разбивается на много парралелльных операций…
Arxitektor
10.11.2018 09:22Честно говоря, меня эта статья очень озадачила, я бы даже сказал, обескуражила.
Я тоже Удивлён что у Apple такой крутой проц. И это у устройстве без активного охлада. А ведь есть еще и A12X Bionic. Который сильно мощнее. Вот что животворящие 30% в год делают ). Ну и AMD тоже со своим гиперпинком вовремя. Мне кажеться что x86 и x64 нужно кардинально переосмыслять. Выкинув все костыли. Ведь Apple смогла свой проц сделать. Я сомневаюсь что у интел инженеры сильно хуже.
подозреваю, что есть некий обширный класс задач, на которых производительность мобильных процессоров будет в десятки и сотни раз хуже чем у дескотпных.
Тоже так думаю. Но те задачи которые нужны обычным пользователям браузер, фильмы, простейшая обработка фото/видео мобьльные процы хорошо решают.qw1
10.11.2018 12:04сомневаюсь что у интел инженеры сильно хуже
Для рентабельности новой архитектуры, её производительность должна быть раз в 10 выше текущей, чтобы весь существующий софт вытащить на эмуляции и юзеры смогли мигрировать хотя бы в эмулятор на первое время. Иначе, получится как с Itanium — средства вложены, процессоры выведены на рынок, но массово их никто не покупает.
DjPhoeniX
10.11.2018 12:59+1Потому я и попробовал майнить на айфонах. Тогда ещё на SE, он уделывал по хэшрейту ноут (MBA 13" 2017, 1,8 GHz Intel Core i5) где-то на 10% в чистом CPU, а когда добавил Metal, то почти в 2 раза. Сейчас на iPhone X разрыв уже считать даже не хочется. Правда вопрос отвода тепла актуален — но можно решить… Ждём майнинг-фермы на iPhone XR.
iproger
10.11.2018 14:04Чего удивляться если процессор на вашем маке слабый.
DjPhoeniX
10.11.2018 23:18+1Знаете, на моём относительно неслабом компе (AMD FX-9590 / Radeon HD7770) хэшрейт был не сильно выше SE. Понятно, что на двух-ксеоновой серверной платформе с четырьмя 1080Ti будет посерьёзнее, но это немного другой класс… А айфон — всё же потребительский сегмент. Опять же, считая по энергоэффективности — тот же айфон на 10W зарядке или 700-900W системный блок — разные вещи.
iproger
10.11.2018 23:21Ну как сказать, ваш AMD FX-9590 даже до годного, но старичка 3770 не дотягивает, про новейшие мощные i7/i9 и говорить нечего.
С картой еще сложнее.
И не надо 4 1080ti. Сейчас одна вытягивает все кроме нескольких моментов.DjPhoeniX
10.11.2018 23:24+1Ну хорошо, так или иначе если посчитать по TDP и энергопотреблению, моё мнение — сопостовимые по хэшрейту кластеры айфонов и потребительского класса компов будут сильно отличаться в пользу фруктовой компании.
iproger
10.11.2018 23:35Вполне возможно. В теории можно по-разному считать, но пока сервера все так же делаются на обычной х86.
Zverienish
11.11.2018 19:13В ближайшие годы Эпл скорее и перейдет на свои процы. Либо просто iOS систему будет продвигать как основную.
potan
11.11.2018 22:16Скорее всего повлияла длина коныеера. В STM-солвере должно быть много проверок условий и переходов, что плохо сказывается на загрузке исполнительных устройств при длинном конвеере.
lorc
12.11.2018 16:48Вроде как пишут что у Интела очень крутой branch predictor. К счастью, уже давно прошли времена когда конвейер сбрасывался на каждом условном jmp.
mvalery
iPhone можно запаять в пластик под вакуумом и погрузить в неметаллическую (пластик/стекло) емкость с ледяной водой.
Энергия будет поступать через безпроводную зарядку, а обмен данными осуществляться через WiFi или Bluetooth.
qw1
Тут уже неважно, металлическая ёмкость или нет — радиосвязь через воду не пройдёт.
Cenzo
Пройдёт с ослаблением если слой воды достаточно небольшой, иначе на улице в дождь и снег не работала бы никакая связь. Проверено на вайфае установкой внешней связи между зданиями.
qw1
Дождь и снег всё-таки не сплошная водная преграда.
Я думаю, через 5мм слой воды уже не пройдёт никакой WiFi
SADKO
Ну, вода-то сама по себе диэлектрик, чего не скажешь о растворённых в ней солях…
vvzvlad
Через 5мм пройдет.
advan20092
В твиттере предложили более красивое решение
линк
SokolovJuri
можно не полностью запаивать, а сделать как чехол, но длиннее раза в два, и подключить кабелем для зарядки и данных
beatstream
А вы говорите, где инновации… Много ли телефонов поддерживают водяное охлаждение? Реквестирую Kickstarter с «watercool kit». И если раньше для вычислительных кластеров использовали игровые приставки, то теперь можно будет и айфоны.