充足可能性モジュロ理論（SMT）式は、論理式の可解性の問題であり、それらの基礎となる理論を考慮に入れています。 - ウィキペディア
数日前、私はつぶやきました ：「興味深い実験：新しいiPhoneでは、Z3の証明者は私の（かなり高価な）デスクトップIntelよりも速く動作します。 すべての正式な調査方法を電話に移します。」
Appleプロセッサの開発者が行った信じられないほどの進歩と、MacがまもなくApple自身のARMプロセッサに移行することについて読みました。 これらのレポートは通常、 Geekbenchなどのいくつかのクロスプラットフォームテストに言及しており、AppleのモバイルプロセッサがIntelのモバイルおよびデスクトッププロセッサよりも劣っていないことを示しています。 しかし、私は常にこれらのクロスプラットフォームテスト（および他のテスト）に少し懐疑的でした-私が私のMacを使用している実際のタスクを実行する速度を本当に反映していますか？
正式な手法の研究者として、私は定期的にSMTソルバー（通常はZ3証明者）を実行する必要があります。 Z3のパフォーマンス特性の調査に多くの時間を費やしました。 テストでは考慮されない機能がいくつかあります（Z3は通常シングルスレッドです）。 最近、最新のApple A12プロセッサを搭載した新しいiPhone XSを購入しました。 そしてどういうわけか、何もすることなく、私はiOSでZ3をコンパイルし、新しい携帯電話（または仮想の将来のMac）がどのくらい速く動作するかを確認することにしました。
最初のテスト
Z3のクロスコンパイルは驚くほど簡単で、コードを数行変更するだけで済みます。 あなた自身のiOSデバイスでZ3を起動するためのソースを投稿しました。 テストでは、 シンボリックコンピューティングのプロファイリングに関する最近の研究からいくつかのクエリを取りました。各ケースについて、 Rosetteによって生成されたSMT が抽出されました。
最初のテストでは、iPhone XSをIntel Core i7-7700Kで動作するデスクトップの1つと比較しました。これは、18か月前に自動車を製造した当時の消費者市場向けの最高のIntelチップです。 Intelは問題なく勝つはずでしたが、結果は異なります。
この23秒間のテストでは、iPhone XSは約11％高速でした！ これをTwitterで報告しましたが、Twitterには詳細の余地があまりないので、ここで紹介します。
- このベンチマークはSMTの
QF_BV
フラグメントであるため、Z3はビットブラストとSATソルバーを使用してこの部分を解決します。 - サイクルを10回実行しても、結果は非常に安定しています。iPhoneはこのパフォーマンスをサポートしており、過熱のために速度が低下し始めていないようです。 1 。 それにもかかわらず、ベンチマークはまだ非常に短いです。
- 何人かの人々は、これが非決定論によるものかどうか尋ねました。 おそらく、異なるプラットフォームでは、ソルバーは乱数の使用または別の理由で異なる方法で進みますか？ しかし、私はZ3の詳細な発行を慎重に確認しましたが、これで結果を説明することはほとんどできません。
- 両方のシステムでZ3 4.8.1を実行しましたが、同じ最適化設定でClangを使用してコンパイルしました。 また、事前に構築されたZ3バイナリ（GCCによってコンパイルされます）を使用してi7-7700Kでテストを実行しましたが、さらに遅くなります。
何が起こっているの？
これはどのように可能ですか？ Core i7-7700Kはデスクトッププロセッサです。 シングルスレッドタスクでは、約45ワットを消費し、4.5 GHzの周波数で動作します。 一方、接続されていないiPhone。 おそらくこの電力の10％も消費せず、2 GHz帯域のどこかで動作します（願っています）。 さらに、比較テストの後、iPhoneバッテリーの使用に関するレポートを確認しました。Slackは、画面での時間が短いにもかかわらず、Z3アプリケーションの4倍のエネルギーを使用すると述べました。
Appleは、iPhoneでのZ3のパフォーマンスを理解するのに十分な情報を提供していませんが、幸い、Intelはこの情報をプロセッサに提供しています。 デスクトップでZ3を起動するときにパフォーマンスのボトルネックを見つけるために、しばらくの間VTuneを駆け巡りました。 Mat Soosが述べたように、SATソルバーはほとんどの時間を分配に費やしますが 、これはキャッシュに非常に敏感です。 VTuneはこれに同意し、観測されたリテラルを反復処理するときにZ3がメモリで待機するのに多くの時間を費やすと言います。 そのため、パフォーマンスの鍵はキャッシュサイズとメモリレイテンシにあるようです。 この効果は、このテストでiPhoneが非常に強力である理由を説明している可能性があります。A12チップには、 低レイテンシの巨大なL2キャッシュがあり 、キャッシュミス後のメモリレイテンシは7700Kよりも優れているようです。
Appleプロセッサの急速な進歩
結果を確認するために、より広範な実験を行い、入手できるすべてのAppleデバイスを収集しました。 また、モバイルCPUのパフォーマンスの急上昇に関する懸念を取り除くために、約10倍長いベンチマーク（つまり、デスクトップで4分）を選択しました。
以下は、アップルの最初の64ビットユーザープロセッサであるA7のこれらのデバイスの結果です（リリース日付き）。
この長いテストでは、i7-7700KデスクトッププロセッサがiPhone XSよりも優れていることにすぐに注意してください。 しかし、iPhoneは信じられないほど競争力があり、i7-7700Kとその前身であるi7-6700Kの間で結果を示しています。i7-6700Kは、2年弱前の最速のコンシューマデスクトッププロセッサでした。
楽しみのために、2016 MacBookから別のCore m7-6Y75プロセッサを追加しました。 Z3テストでは、私の携帯電話はラップトップよりも約50％高速です。
ここで本当に注目すべきことは、このZ3ベンチマークで年間30％のかなり一貫した改善という傾向です。 明らかに、1つの愚かなテストから広範囲にわたる結論を引き出すべきではありませんが、2、3回の反復の後、Appleプロセッサはワークロードに非常に適したものになると思われます。 2 。 正直なところ、私たちがそれほど近くにいるとは思っていませんでした。スマートフォンの最新のアーキテクチャは、信じられないほど素晴らしいです！
他のデバイスでテストを実行する際に助けてくれたMegan Cowan 、 Max Willsi、およびEddie Ianに感謝します。
1 マックスは、iPhoneが防水であることに気づいたので、氷浴に浸すことで理論を確認できます。 しかし、私は電話に多額のお金を支払ったので、そのような経験を自発的に行いたくありません。 ↑
2 。 新しいiPad Proの A12Xは、タブレットが提供するより大きなサーマルエンベロープのおかげでさらに高速になったに違いありません。 ↑