Warum einen teuren PC kaufen, wenn Ihr iPhone SMT schneller löst?

Die Formel für Erfüllbarkeitsmodulo-Theorien (SMT) ist das Lösbarkeitsproblem für logische Formeln unter Berücksichtigung der ihnen zugrunde liegenden Theorien. - Wikipedia

Vor einigen Tagen habe ich getwittert : „Ein interessantes Experiment: Auf dem neuen iPhone arbeitet der Z3-Prover schneller als auf meinem (ziemlich teuren) Desktop-Intel. Es ist Zeit, alle formalen Forschungsmethoden auf das Telefon zu übertragen. "


Ich habe über die unglaublichen Fortschritte gelesen, die Apple-Prozessorentwickler gemacht haben, und dass die Macs bald auf Apples eigene ARM-Prozessoren übertragen werden . Diese Berichte beziehen sich normalerweise auf einige plattformübergreifende Tests wie Geekbench, um zu demonstrieren, dass die mobilen Prozessoren von Apple den mobilen und Desktop-Prozessoren von Intel nicht unterlegen sind. Aber ich war immer etwas skeptisch gegenüber diesen plattformübergreifenden Tests (und anderen ) - spiegeln sie wirklich die Geschwindigkeit wider, mit der ich echte Aufgaben ausführe, für die ich meinen Mac verwende?

Als Forscher formaler Methoden muss ich regelmäßig einen SMT-Solver ausführen, normalerweise den Z3-Prover . Ich habe viel Zeit damit verbracht, die Leistungsmerkmale des Z3 zu studieren. Es hat einige Funktionen, die in Tests nicht berücksichtigt werden (Z3 ist normalerweise Single-Threaded). Ich habe kürzlich ein neues iPhone XS mit dem neuesten Apple A12 Prozessor gekauft. Und irgendwie, ohne etwas zu tun, entschied ich mich, Z3 in iOS zu kompilieren und zu sehen, wie schnell das neue Telefon (oder ein hypothetischer zukünftiger Mac) funktioniert.

Erster Test

Das Cross-Compilieren von Z3 erwies sich als überraschend einfach. Sie müssen nur einige Codezeilen ändern. Ich habe die Quellen für den Start von Z3 auf Ihrem eigenen iOS-Gerät veröffentlicht . Für den Test habe ich einige Fragen aus meiner jüngsten Arbeit zur Profilerstellung für symbolisches Computing beantwortet: Für jeden Fall wurde die von Rosette generierte SMT extrahiert.

Im ersten Test habe ich das iPhone XS mit einem der Desktops verglichen, die auf dem Intel Core i7-7700K laufen - dem besten Intel-Chip für den Verbrauchermarkt, als ich das Auto vor 18 Monaten gebaut habe. Intel sollte ohne Probleme gewinnen, aber es stellte sich anders heraus:



In diesem 23-Sekunden-Test war das iPhone XS etwa 11% schneller! Ich habe dies auf Twitter gemeldet, aber Twitter lässt nicht viel Platz für Details, deshalb werde ich sie hier präsentieren:

• Dieser Benchmark ist ein Fragment von QF_BV von SMT, daher löst Z3 diesen Teil mit Bit-Strahlen und SAT-Solver.
• Das Ergebnis ist ziemlich stabil, selbst wenn Sie den Zyklus zehnmal ausführen: Das iPhone unterstützt diese Leistung und scheint sich aufgrund von Überhitzung nicht zu verlangsamen. ¹ . Trotzdem ist der Benchmark noch recht flüchtig.
• Mehrere Personen fragten, ob dies auf Nichtdeterminismus zurückzuführen sei. Vielleicht geht der Löser auf verschiedenen Plattformen aufgrund der Verwendung von Zufallszahlen oder aus einem anderen Grund anders vor? Aber ich habe die detaillierte Ausgabe von Z3 ziemlich sorgfältig geprüft, und die Ergebnisse lassen sich damit kaum erklären.
• Auf beiden Systemen lief Z3 4.8.1, das ich mit Clang mit den gleichen Optimierungseinstellungen kompiliert habe. Ich habe auch Tests auf dem i7-7700K mit vorgefertigten Z3-Binärdateien (die von GCC kompiliert werden) durchgeführt, aber sie sind noch langsamer.

Was ist los?

Wie ist das möglich? Core i7-7700K ist der gleiche Desktop-Prozessor. Bei einer Single-Threaded-Aufgabe verbraucht es etwa 45 Watt und arbeitet mit einer Frequenz von 4,5 GHz. Unplugged iPhone dagegen. Es verbraucht wahrscheinlich nicht einmal 10% dieser Leistung und funktioniert (wir hoffen) irgendwo im 2-GHz-Band. Darüber hinaus habe ich nach einem Vergleichstest den Bericht über die Verwendung des iPhone-Akkus überprüft: Slack verbrauchte trotz der kürzeren Zeit auf dem Bildschirm viermal mehr Energie als die Z3-Anwendung.

Apple bietet nicht genügend Informationen, um die Leistung von Z3 auf dem iPhone zu verstehen, aber zum Glück stellt Intel diese Informationen für seinen Prozessor bereit. Ich habe eine Weile in VTune gestöbert , um Leistungsengpässe beim Starten von Z3 auf dem Desktop zu finden. Wie von Mat Soos festgestellt, verbringt der SAT-Solver die meiste Zeit mit der Verteilung , die sehr empfindlich auf den Cache reagiert . VTune stimmt zu und sagt, dass der Z3 viel Zeit damit verbringt, im Gedächtnis zu warten, wenn er die beobachteten Literale durchläuft. Der Schlüssel zur Leistung scheint also die Cache-Größe und die Speicherlatenz zu sein. Dieser Effekt könnte erklären, warum das iPhone in diesem Test so leistungsfähig ist: Der A12-Chip verfügt über einen riesigen L2-Cache mit geringer Latenz und scheint nach einem Cache-Fehler im Vergleich zu 7700K auch eine bessere Speicherlatenz zu haben.

Der schnelle Fortschritt der Apple-Prozessoren

Um die Ergebnisse zu bestätigen, führte ich ein ausführlicheres Experiment durch und sammelte alle Apple-Geräte, die ich bekommen konnte. Ich habe mich auch für einen zehnmal längeren Benchmark entschieden (d. H. 4 Minuten auf dem Desktop), um Bedenken hinsichtlich der Bursts bei der Leistung mobiler CPUs auszuräumen.

Hier sind die Ergebnisse für diese Geräte (mit Veröffentlichungsdaten) für den A7, Apples ersten 64-Bit-Benutzerprozessor:



Es sollte sofort beachtet werden, dass der i7-7700K-Desktop-Prozessor in diesem längeren Test dem iPhone XS überlegen ist. Das iPhone ist jedoch unglaublich wettbewerbsfähig und zeigt das Ergebnis zwischen dem i7-7700K und seinem Vorgänger, dem i7-6700K, der vor etwas weniger als zwei Jahren der schnellste Desktop-Prozessor für Verbraucher war.

Zum Spaß habe ich einen weiteren Core m7-6Y75-Prozessor von meinem 2016 MacBook hinzugefügt. Im Z3-Test ist mein Telefon etwa 50% schneller als ein Laptop.

Das wirklich Bemerkenswerte hier ist der Trend: eine ziemlich konstante Verbesserung von 30% pro Jahr für diesen Z3-Benchmark. Natürlich sollten Sie aus einem dummen Test keine weitreichenden Schlussfolgerungen ziehen, aber es scheint, dass Apple-Prozessoren nach einigen Iterationen für Workloads gut geeignet sind. ² . Ich habe ehrlich gesagt nicht erwartet, dass wir uns so nahe sind: Die moderne Architektur von Smartphones ist einfach unglaublich!

Vielen Dank an Megan Cowan , Max Willsy und Eddie Ian für ihre Hilfe bei der Durchführung von Tests auf anderen Geräten.

---

¹ . Max bemerkte, dass das iPhone wasserdicht ist, sodass die Theorie durch Eintauchen in ein Eisbad überprüft werden kann. Aber ich habe viel Geld für das Telefon bezahlt und möchte eine solche Erfahrung nicht freiwillig machen. ↑

² . Ich wette, dass das A12X im neuen iPad Pro dank der größeren thermischen Hülle , die das Tablet bietet, noch schneller ist. ↑