Mengapa membeli PC mahal jika iPhone Anda memecahkan SMT lebih cepat?

Rumus teori satisfoability modulo (SMT) adalah masalah solvabilitas untuk rumus logis, dengan mempertimbangkan teori yang mendasari mereka. - Wikipedia

Beberapa hari yang lalu, saya tweeted : “Eksperimen yang menarik: pada iPhone baru, Z3 prover bekerja lebih cepat daripada pada Intel desktop saya (agak mahal). Sudah waktunya untuk mentransfer semua metode penelitian formal ke telepon. "


Saya membaca tentang kemajuan luar biasa yang telah dibuat oleh pengembang prosesor Apple , dan bahwa Mac akan segera mentransfer ke prosesor ARM milik Apple . Laporan-laporan ini biasanya merujuk pada beberapa pengujian lintas platform, seperti Geekbench, untuk menunjukkan bahwa prosesor seluler Apple tidak kalah dengan prosesor seluler dan desktop Intel. Tetapi saya selalu sedikit skeptis tentang pengujian lintas platform ini (juga yang lain ) - apakah mereka benar-benar mencerminkan kecepatan melakukan tugas nyata yang saya gunakan untuk Mac saya?

Sebagai peneliti metode formal, saya secara teratur harus menjalankan SMT solver, biasanya Z3 prover . Saya menghabiskan banyak waktu mempelajari karakteristik kinerja Z3. Ini memiliki beberapa fitur yang tidak diperhitungkan dalam pengujian (Z3 biasanya single-threaded). Baru-baru ini saya membeli iPhone XS baru dengan prosesor Apple A12 terbaru. Dan entah bagaimana, tanpa ada hubungannya, saya memutuskan untuk mengkompilasi Z3 di iOS dan melihat seberapa cepat ponsel baru (atau Mac masa depan hipotetis) bekerja.

Tes pertama

Kompilasi silang Z3 ternyata sangat sederhana, Anda hanya perlu mengubah beberapa baris kode. Saya memposting sumber untuk meluncurkan Z3 di perangkat iOS Anda sendiri . Untuk pengujian, saya mengambil beberapa pertanyaan dari pekerjaan saya baru-baru ini pada pembuatan profil komputasi simbolik : untuk setiap kasus, SMT yang dihasilkan oleh Rosette diekstraksi.

Pada pengujian pertama, saya membandingkan iPhone XS dengan salah satu desktop yang berjalan pada Intel Core i7-7700K - chip Intel terbaik untuk pasar konsumen pada saat saya membangun mobil 18 bulan yang lalu. Intel seharusnya menang tanpa masalah, tetapi ternyata berbeda:



Dalam pengujian 23 detik ini, iPhone XS sekitar 11% lebih cepat! Saya melaporkan ini di Twitter, tetapi Twitter tidak meninggalkan banyak ruang untuk detail, jadi saya akan menyajikannya di sini:

• Benchmark ini adalah bagian dari QF_BV dari SMT, oleh karena itu Z3 memecahkan bagian ini menggunakan bit-blasting dan SAT-solver.
• Hasilnya cukup stabil, bahkan jika Anda menjalankan siklus sepuluh kali: iPhone mendukung kinerja ini dan tampaknya tidak mulai melambat karena terlalu panas. ¹ . Meski demikian, patokannya masih cukup singkat.
• Beberapa orang bertanya apakah ini karena non-determinisme. Mungkin, pada platform yang berbeda, solver berjalan dengan cara yang berbeda karena penggunaan angka acak atau karena alasan lain? Tapi saya agak hati-hati memeriksa detail penerbitan Z3, dan hasilnya tidak bisa dijelaskan dengan ini.
• Kedua sistem menjalankan Z3 4.8.1, yang saya kompilasi menggunakan Dentang dengan pengaturan optimasi yang sama. Saya juga menjalankan tes pada i7-7700K dengan binari Z3 pre-built (yang dikompilasi oleh GCC), tetapi mereka bahkan lebih lambat.

Apa yang sedang terjadi

Bagaimana ini mungkin? Core i7-7700K adalah prosesor desktop yang sama. Dalam tugas single-threaded, ia mengkonsumsi sekitar 45 watt dan beroperasi pada frekuensi 4,5 GHz. IPhone dicabut, di sisi lain. Mungkin tidak mengkonsumsi bahkan 10% dari kekuatan ini dan bekerja (kami harap) di suatu tempat di pita 2 GHz. Selain itu, setelah tes komparatif, saya memeriksa laporan tentang penggunaan baterai iPhone: dikatakan bahwa Slack menggunakan energi 4 kali lebih banyak daripada aplikasi Z3, meskipun lebih sedikit waktu di layar.

Apple tidak memberikan informasi yang cukup untuk memahami kinerja Z3 pada iPhone, tetapi, untungnya, Intel memberikan informasi ini untuk prosesornya. Saya mencari-cari VTune untuk sementara waktu untuk menemukan hambatan kinerja ketika memulai Z3 di desktop. Seperti dicatat oleh Mat Soos , sebagian besar pemecah SAT menghabiskan pada distribusi , yang sangat sensitif terhadap cache . VTune setuju dan mengatakan bahwa Z3 menghabiskan banyak waktu menunggu dalam ingatan ketika beralih pada literasi yang diamati. Jadi kunci kinerja tampaknya adalah ukuran cache dan latensi memori. Efek ini dapat menjelaskan mengapa iPhone sangat kuat dalam pengujian ini: chip A12 memiliki cache L2 raksasa dengan latensi rendah , dan juga tampaknya memiliki latensi memori yang lebih baik setelah cache yang ketinggalan dibandingkan dengan 7700K.

Pesatnya kemajuan prosesor Apple

Untuk mengkonfirmasi hasilnya, saya melakukan percobaan yang lebih luas, mengumpulkan semua perangkat Apple yang bisa saya dapatkan. Saya juga memilih patokan 10 kali lebih lama (mis. 4 menit di desktop) untuk mengurangi kekhawatiran tentang semburan kinerja CPU seluler.

Berikut adalah hasil untuk perangkat ini (dengan tanggal rilis) untuk A7, prosesor pengguna 64-bit pertama Apple:



Harus segera dicatat bahwa prosesor desktop i7-7700K lebih unggul daripada iPhone XS dalam pengujian yang lebih lama ini. Tetapi iPhone sangat kompetitif, menunjukkan hasil antara i7-7700K dan pendahulunya, i7-6700K, yang merupakan prosesor desktop konsumen tercepat sedikit kurang dari dua tahun lalu.

Untuk bersenang-senang, saya menambahkan prosesor Core m7-6Y75 lain dari MacBook 2016 saya. Dalam tes Z3, ponsel saya sekitar 50% lebih cepat daripada laptop.

Hal yang sangat luar biasa di sini adalah tren: peningkatan yang cukup konsisten sebesar 30% per tahun untuk benchmark Z3 ini. Jelas, Anda tidak boleh menarik kesimpulan yang jauh dari satu tes bodoh, tetapi tampaknya setelah beberapa iterasi, prosesor Apple akan menjadi sangat cocok untuk beban kerja. ² . Sejujurnya saya tidak berharap kita begitu dekat: arsitektur modern dari smartphone sangat luar biasa!

Terima kasih kepada Megan Cowan , Max Willsy, dan Eddie Ian atas bantuan mereka dalam menjalankan tes pada perangkat lain.

---

¹ . Max memperhatikan bahwa iPhone itu kedap air, sehingga teorinya dapat diperiksa dengan mencelupkannya ke dalam penangas es. Tetapi saya membayar banyak uang untuk telepon dan saya tidak ingin secara sukarela melakukan pengalaman seperti itu. ↑

² . Saya bertaruh bahwa A12X di Pro iPad baru bahkan lebih cepat berkat amplop termal yang lebih besar yang diberikan tablet. ↑