¿Por qué comprar una PC costosa si su iPhone resuelve SMT más rápido?La fórmula de las teorías del módulo de satisfacción (SMT) es el problema de la solución para las fórmulas lógicas, teniendo en cuenta las teorías subyacentes. - WikipediaHace unos días,
tuiteé : “Un experimento interesante: en el nuevo iPhone, el probador Z3 funciona más rápido que en mi (bastante costosa) computadora de escritorio Intel. Es hora de transferir todos los métodos de investigación formales al teléfono ".
Leí sobre el increíble progreso que
los desarrolladores de procesadores de Apple han hecho, y que las Mac pronto se transferirán a
los procesadores ARM de Apple . Estos informes generalmente se refieren a algunas pruebas multiplataforma, como
Geekbench, para demostrar que los procesadores móviles de Apple no son inferiores a los procesadores móviles y de escritorio de Intel. Pero siempre fui un poco escéptico con respecto a estas pruebas multiplataforma (así como a
otras ): ¿reflejan realmente la velocidad de realizar tareas reales para las que uso mi Mac?
Como investigador de métodos formales, regularmente tengo que ejecutar un solucionador SMT, generalmente el
probador Z3 . Pasé mucho tiempo estudiando las características de rendimiento del Z3. Tiene algunas características que no se tienen en cuenta en las pruebas (Z3 suele ser de un solo subproceso). Recientemente compré un nuevo
iPhone XS con el último procesador Apple
A12 . Y de alguna manera, sin nada que hacer, decidí compilar Z3 en iOS y ver qué tan rápido funciona el nuevo teléfono (o un hipotético futuro Mac).
Primera prueba
La compilación cruzada de Z3 resultó ser sorprendentemente simple, solo necesita cambiar algunas líneas de código. Publiqué las fuentes para
lanzar Z3 en su propio dispositivo iOS . Para la prueba, tomé algunas consultas de mi trabajo reciente sobre el
perfil de la computación simbólica : para cada caso,
se extrajo el SMT generado por
Rosette .
En la primera prueba, comparé el iPhone XS con uno de los equipos de escritorio que funciona con el Intel Core i7-7700K, el mejor chip Intel para el mercado de consumo en el momento en que construí el automóvil hace 18 meses. Se suponía que Intel ganaría sin ningún problema, pero resultó diferente:
¡En esta prueba de 23 segundos, el iPhone XS fue aproximadamente un 11% más rápido! Informé esto en Twitter, pero Twitter no deja mucho espacio para los detalles, por lo que los presentaré aquí:
- Este punto de referencia es un fragmento de
QF_BV de SMT, por lo tanto, Z3 resuelve esta parte utilizando bit-blasting y SAT-solver. - El resultado es bastante estable, incluso si ejecuta el ciclo diez veces: el iPhone es compatible con este rendimiento y no parece comenzar a disminuir debido al sobrecalentamiento. 1 . Sin embargo, el punto de referencia sigue siendo bastante fugaz.
- Varias personas preguntaron si esto se debió al no determinismo. ¿Quizás, en diferentes plataformas, el solucionador va de una manera diferente debido al uso de números aleatorios o por otra razón? Pero revisé con cuidado la emisión detallada de Z3, y los resultados difícilmente pueden explicarse por esto.
- Ambos sistemas ejecutaban Z3 4.8.1, que compilé usando Clang con la misma configuración de optimización. También ejecuté pruebas en el i7-7700K con binarios Z3 precompilados (compilados por GCC), pero son aún más lentos.
Que esta pasando
¿Cómo es esto posible? Core i7-7700K es el mismo procesador de escritorio. En una tarea de subproceso único, consume aproximadamente 45 vatios y funciona a una frecuencia de 4,5 GHz. IPhone desconectado, por otro lado. Probablemente no consume ni el 10% de esta potencia y funciona (esperamos) en algún lugar de la banda de 2 GHz. Además, después de una prueba comparativa, verifiqué el informe sobre el uso de la batería del iPhone: decía que Slack usaba 4 veces más energía que la aplicación Z3, a pesar del menor tiempo en la pantalla.
Apple no proporciona suficiente información para comprender el rendimiento de Z3 en el iPhone, pero, afortunadamente, Intel proporciona esta información para su procesador. Rebusqué en
VTune por un tiempo para encontrar cuellos de botella en el rendimiento al iniciar Z3 en el escritorio. Como señaló
Mat Soos , la mayoría de las veces el solucionador de SAT
gasta en distribución , que es
muy sensible al caché . VTune está de acuerdo y dice que el Z3 pasa mucho tiempo esperando en la memoria al iterar sobre los literales observados. Entonces, la clave del rendimiento parece ser el tamaño de la memoria caché y la latencia de la memoria. Este efecto puede explicar por qué el iPhone es tan poderoso en esta prueba: el chip A12 tiene un
caché L2 gigante con baja latencia , y también parece tener una mejor latencia de memoria después de una falla de caché en comparación con 7700K.
El rápido progreso de los procesadores Apple
Para confirmar los resultados, realicé un experimento más extenso, recolectando todos los dispositivos Apple que pude obtener. También elegí un punto de referencia aproximadamente 10 veces más largo (es decir, 4 minutos en el escritorio) para aliviar las preocupaciones sobre las ráfagas en el rendimiento de la CPU móvil.
Aquí están los resultados para estos dispositivos (con fechas de lanzamiento) para el A7, el primer procesador de usuario de 64 bits de Apple:
Cabe señalar de inmediato que el procesador de escritorio i7-7700K es superior al iPhone XS en esta prueba más larga. Pero el iPhone es increíblemente competitivo, mostrando el resultado entre el i7-7700K y su predecesor, el i7-6700K, que fue el procesador de escritorio de consumo más rápido hace poco menos de dos años.
Por diversión, agregué otro procesador Core m7-6Y75 de mi MacBook 2016. En la prueba Z3, mi teléfono es aproximadamente un 50% más rápido que una computadora portátil.
Lo realmente notable aquí es la tendencia: una mejora bastante consistente del 30% anual para este punto de referencia Z3. Obviamente, no debe sacar conclusiones de largo alcance de una prueba estúpida, pero parece que después de un par de iteraciones, los procesadores de Apple serán muy adecuados para las cargas de trabajo.
2 . Sinceramente, no esperaba que estuviéramos tan cerca: ¡la arquitectura moderna de los teléfonos inteligentes es simplemente increíble!
Gracias a Megan Cowan , Max Willsy y Eddie Ian por su ayuda en la ejecución de pruebas en otros dispositivos.
1) Max notó que el iPhone es resistente al agua, por lo que la teoría se puede verificar sumergiéndola en un baño de hielo. Pero pagué mucho dinero por el teléfono y no quiero llevar a cabo esa experiencia voluntariamente.
↑2) Apuesto a que el A12X en el nuevo
iPad Pro es aún más rápido gracias al
sobre térmico más grande que ofrece la tableta.
↑