Pourquoi acheter un PC cher si votre iPhone résout SMT plus rapidement?

La formule des théories de module de satisfiabilité (SMT) est le problème de solvabilité des formules logiques, en tenant compte des théories qui les sous-tendent. - Wikipédia

Il y a quelques jours, j'ai tweeté : «Une expérience intéressante: sur le nouvel iPhone, le prouveur Z3 fonctionne plus vite que sur mon ordinateur de bureau (plutôt cher) Intel. Il est temps de transférer toutes les méthodes de recherche formelles sur le téléphone. "


J'ai lu les progrès incroyables réalisés par les développeurs de processeurs Apple et le fait que les Mac seront bientôt transférés vers les processeurs ARM d' Apple . Ces rapports font généralement référence à certains tests multiplateformes, tels que Geekbench, pour démontrer que les processeurs mobiles d'Apple ne sont pas inférieurs aux processeurs mobiles et de bureau d'Intel. Mais j'ai toujours été un peu sceptique à l'égard de ces tests multiplateformes (ainsi que d' autres ) - reflètent-ils vraiment la vitesse d'exécution des tâches réelles pour lesquelles j'utilise mon Mac?

En tant que chercheur de méthodes formelles, je dois régulièrement exécuter un solveur SMT, généralement le prouveur Z3 . J'ai passé beaucoup de temps à étudier les caractéristiques de performance du Z3. Il possède certaines fonctionnalités qui ne sont pas prises en compte dans les tests (Z3 est généralement monofil). J'ai récemment acheté un nouvel iPhone XS avec le dernier processeur Apple A12 . Et en quelque sorte, n'ayant rien à faire, j'ai décidé de compiler Z3 dans iOS et de voir à quelle vitesse le nouveau téléphone (ou un futur Mac hypothétique) fonctionne.

Premier test

La compilation croisée de Z3 s'est avérée étonnamment simple, il vous suffit de modifier quelques lignes de code. J'ai publié les sources du lancement de Z3 sur votre propre appareil iOS . Pour le test, j'ai repris quelques requêtes de mes travaux récents sur le profilage de l'informatique symbolique : pour chaque cas, le SMT généré par Rosette a été extrait.

Lors du premier test, j'ai comparé l'iPhone XS à l'un des ordinateurs de bureau fonctionnant sur Intel Core i7-7700K - la meilleure puce Intel pour le marché grand public au moment où j'ai construit la voiture il y a 18 mois. Intel était censé gagner sans aucun problème, mais il s'est avéré différemment:



Dans ce test de 23 secondes, l'iPhone XS était environ 11% plus rapide! Je l'ai signalé sur Twitter, mais Twitter ne laisse pas beaucoup de place aux détails, je vais donc les présenter ici:

• Ce benchmark est un fragment de QF_BV de SMT, donc Z3 résout cette partie en utilisant le dynamitage et le solveur SAT.
• Le résultat est assez stable, même si vous exécutez le cycle dix fois: l'iPhone prend en charge cette performance et ne semble pas commencer à ralentir en raison d'une surchauffe. ¹ . Néanmoins, l'indice de référence est encore assez éphémère.
• Plusieurs personnes ont demandé si cela était dû au non-déterminisme. Peut-être, sur différentes plates-formes, le solveur va d'une manière différente en raison de l'utilisation de nombres aléatoires ou pour une autre raison? Mais j'ai plutôt soigneusement vérifié l'émission détaillée de Z3, et les résultats peuvent difficilement être expliqués par cela.
• Les deux systèmes ont exécuté Z3 4.8.1, que j'ai compilé en utilisant Clang avec les mêmes paramètres d'optimisation. J'ai également effectué des tests sur le i7-7700K avec des binaires Z3 pré-construits (qui sont compilés par GCC), mais ils sont encore plus lents.

Que se passe-t-il?

Comment est-ce possible? Le Core i7-7700K est le même processeur de bureau. Dans une tâche à thread unique, il consomme environ 45 watts et fonctionne à une fréquence de 4,5 GHz. IPhone débranché, d'autre part. Il ne consomme probablement même pas 10% de cette puissance et fonctionne (nous l'espérons) quelque part dans la bande des 2 GHz. De plus, après un test comparatif, j'ai vérifié le rapport sur l'utilisation de la batterie de l'iPhone: il était dit que Slack utilisait 4 fois plus d'énergie que l'application Z3, malgré le moins de temps sur l'écran.

Apple ne fournit pas suffisamment d'informations pour comprendre les performances de Z3 sur l'iPhone, mais, heureusement, Intel fournit ces informations pour son processeur. J'ai fouillé dans VTune pendant un certain temps pour trouver des goulots d'étranglement au niveau des performances lors du démarrage de Z3 sur le bureau. Comme l'a noté Mat Soos , la plupart du temps le solveur SAT passe sur la distribution , qui est très sensible au cache . VTune est d'accord et dit que le Z3 passe beaucoup de temps à attendre en mémoire lors de l'itération sur les littéraux observés. La clé des performances semble donc être la taille du cache et la latence de la mémoire. Cet effet peut expliquer pourquoi l'iPhone est si puissant dans ce test: la puce A12 a un cache L2 géant avec une faible latence , et semble également avoir une meilleure latence mémoire après un manque de cache par rapport à 7700K.

La progression rapide des processeurs Apple

Pour confirmer les résultats, j'ai mené une expérience plus approfondie, en collectant tous les appareils Apple que j'ai pu obtenir. J'ai également choisi une référence environ 10 fois plus longue (soit 4 minutes sur le bureau) pour atténuer les inquiétudes concernant les rafales de performances du processeur mobile.

Voici les résultats de ces appareils (avec les dates de sortie) pour l'A7, le premier processeur utilisateur 64 bits d'Apple:



Il convient de noter tout de suite que le processeur de bureau i7-7700K est supérieur à l'iPhone XS dans ce test plus long. Mais l'iPhone est incroyablement compétitif, montrant le résultat entre l'i7-7700K et son prédécesseur, l'i7-6700K, qui était le processeur de bureau grand public le plus rapide il y a un peu moins de deux ans.

Pour le plaisir, j'ai ajouté un autre processeur Core m7-6Y75 de mon MacBook 2016. Dans le test Z3, mon téléphone est environ 50% plus rapide qu'un ordinateur portable.

La chose vraiment remarquable ici est la tendance: une amélioration assez constante de 30% par an pour ce benchmark Z3. De toute évidence, vous ne devriez pas tirer de conclusions de grande envergure à partir d'un test stupide, mais il semble qu'après quelques itérations, les processeurs Apple deviendront tout à fait adaptés aux charges de travail. ² . Honnêtement, je ne m'attendais pas à ce que nous soyons si proches: l'architecture moderne des smartphones est tout simplement incroyable!

Merci à Megan Cowan , Max Willsy et Eddie Ian pour leur aide lors de l'exécution de tests sur d'autres appareils.

---

¹ . Max a remarqué que l'iPhone est étanche, de sorte que la théorie peut être vérifiée en le plongeant dans un bain de glace. Mais j'ai payé beaucoup d'argent pour le téléphone et je ne veux pas mener volontairement une telle expérience. ↑

² . Je parie que l'A12X dans le nouvel iPad Pro est encore plus rapide grâce à la plus grande enveloppe thermique offerte par la tablette. ↑