Por que comprar um PC caro se o seu iPhone resolve o SMT mais rapidamente?

A fórmula de teorias de módulo de satisfação (SMT) é o problema de solvabilidade de fórmulas lógicas, levando em consideração as teorias subjacentes a elas. - Wikipedia

Alguns dias atrás, eu twitei : “Um experimento interessante: no novo iPhone, o provador Z3 funciona mais rápido que no meu desktop Intel (bastante caro). É hora de transferir todos os métodos formais de pesquisa para o telefone ".


Eu li sobre o incrível progresso que os desenvolvedores de processadores da Apple fizeram e que os Macs em breve serão transferidos para os próprios processadores ARM da Apple . Esses relatórios geralmente se referem a alguns testes de plataforma cruzada, como o Geekbench, para demonstrar que os processadores móveis da Apple não são inferiores aos processadores móveis e de desktop da Intel. Mas eu sempre fiquei um pouco cético em relação a esses testes de plataforma cruzada (e outros ) - eles realmente refletem a velocidade de executar tarefas reais para as quais eu uso o meu Mac?

Como pesquisador de métodos formais, eu regularmente tenho que executar um solucionador SMT, geralmente o provador Z3 . Passei muito tempo estudando as características de desempenho do Z3. Ele possui alguns recursos que não são levados em consideração nos testes (o Z3 geralmente é de thread único). Recentemente, comprei um novo iPhone XS com o mais recente processador Apple A12 . E de alguma forma, sem nada para fazer, decidi compilar o Z3 no iOS e ver com que rapidez o novo telefone (ou um futuro Mac hipotético) funciona.

Primeiro teste

A compilação cruzada do Z3 acabou surpreendentemente simples, você só precisa alterar algumas linhas de código. Publiquei as fontes para o lançamento do Z3 em seu próprio dispositivo iOS . Para o teste, fiz algumas consultas em meu trabalho recente sobre criação de perfil de cálculos simbólicos : para cada caso, o SMT gerado pelo Rosette foi extraído.

No primeiro teste, comparei o iPhone XS com um dos desktops que rodam no Intel Core i7-7700K - o melhor chip da Intel para o mercado consumidor na época em que construí o carro há 18 meses. A Intel deveria vencer sem problemas, mas acabou diferente:



Neste teste de 23 segundos, o iPhone XS foi cerca de 11% mais rápido! Eu relatei isso no Twitter, mas o Twitter não deixa muito espaço para detalhes, então os apresentarei aqui:

• Esta referência é um fragmento de QF_BV da SMT, portanto, o Z3 resolve esta parte usando detonação de bits e solucionador de SAT.
• O resultado é bastante estável, mesmo se você executar o ciclo dez vezes: o iPhone suporta esse desempenho e parece não começar a desacelerar devido ao superaquecimento. ¹ . No entanto, a referência ainda é bastante passageira.
• Várias pessoas perguntaram se isso era devido ao não determinismo. Talvez, em plataformas diferentes, o solucionador seja diferente devido ao uso de números aleatórios ou por outro motivo? Mas verifiquei cuidadosamente a questão detalhada do Z3 e os resultados dificilmente podem ser explicados por isso.
• Ambos os sistemas executaram o Z3 4.8.1, que eu compilei usando o Clang com as mesmas configurações de otimização. Também executei testes no i7-7700K com binários Z3 pré-criados (compilados pelo GCC), mas eles são ainda mais lentos.

O que está havendo?

Como isso é possível? O Core i7-7700K é o mesmo processador de desktop. Em uma tarefa de thread único, consome cerca de 45 watts e opera com uma frequência de 4,5 GHz. IPhone desconectado, por outro lado. Provavelmente não consome nem 10% dessa energia e funciona (esperamos) em algum lugar da banda de 2 GHz. Além disso, após um teste comparativo, verifiquei o relatório sobre o uso da bateria do iPhone: dizia que o Slack consumia 4 vezes mais energia que o aplicativo Z3, apesar do menor tempo na tela.

A Apple não fornece informações suficientes para entender o desempenho do Z3 no iPhone, mas, felizmente, a Intel fornece essas informações para seu processador. Examinei o VTune por um tempo para encontrar gargalos de desempenho ao iniciar o Z3 na área de trabalho. Conforme observado por Mat Soos , na maioria das vezes o solucionador SAT gasta na distribuição , o que é muito sensível ao cache . O VTune concorda e diz que o Z3 gasta muito tempo aguardando na memória ao iterar sobre os literais observados. Portanto, a chave do desempenho parece ser o tamanho do cache e a latência da memória. Esse efeito pode explicar por que o iPhone é tão poderoso neste teste: o chip A12 possui um cache L2 gigante com baixa latência e também parece ter uma melhor latência de memória após uma falta de cache em comparação com 7700K.

O rápido progresso dos processadores Apple

Para confirmar os resultados, conduzi um experimento mais extenso, coletando todos os dispositivos da Apple que consegui. Também escolhi uma referência 10 vezes mais longa (ou seja, 4 minutos na área de trabalho) para aliviar as preocupações com as explosões no desempenho da CPU móvel.

Aqui estão os resultados para esses dispositivos (com datas de lançamento) para o A7, o primeiro processador de usuário de 64 bits da Apple:



Deve-se notar imediatamente que o processador de desktop i7-7700K é superior ao iPhone XS neste teste mais longo. Mas o iPhone é incrivelmente competitivo, mostrando o resultado entre o i7-7700K e seu antecessor, o i7-6700K, que foi o processador de desktop mais rápido para consumidores há menos de dois anos.

Por diversão, adicionei outro processador Core m7-6Y75 do meu MacBook 2016. No teste Z3, meu telefone é cerca de 50% mais rápido que um laptop.

O mais notável aqui é a tendência: uma melhoria bastante consistente de 30% ao ano para esse benchmark Z3. Obviamente, você não deve tirar conclusões abrangentes de um teste estúpido, mas parece que após algumas iterações, os processadores da Apple se tornarão adequados para cargas de trabalho. ² . Sinceramente, não esperava que estejamos tão perto: a arquitetura moderna dos smartphones é simplesmente incrível!

Agradecemos a Megan Cowan , Max Willsy e Eddie Ian por sua ajuda na execução de testes em outros dispositivos.

---

¹ Max percebeu que o iPhone é à prova d'água, então a teoria pode ser verificada imergindo-o em um banho de gelo. Mas paguei muito dinheiro pelo telefone e não quero conduzir voluntariamente essa experiência. ↑

²⁾ Aposto que o A12X no novo iPad Pro é ainda mais rápido, graças ao envelope térmico maior que o tablet oferece. ↑