لماذا تشتري جهاز كمبيوتر باهظ الثمن إذا كان جهاز iPhone الخاص بك يحل SMT بشكل أسرع؟تعد صيغة نظريات المعادلة (SMT) مشكلة قابلية الحلول للصيغ المنطقية ، مع مراعاة النظريات الكامنة وراءها. - ويكيبيدياقبل بضعة أيام ،
غردت : "تجربة مثيرة للاهتمام: على جهاز iPhone الجديد ، يعمل Z3 prover بشكل أسرع من جهاز Intel المكتبي (باهظ الثمن نوعًا ما). حان الوقت لنقل جميع طرق البحث الرسمية إلى الهاتف ".
قرأت عن التقدم المذهل الذي أحرزه
مطورو معالج Apple ، وأن أجهزة Mac ستنتقل قريبًا إلى
معالجات ARM الخاصة بشركة Apple . تشير هذه التقارير عادةً إلى بعض الاختبارات عبر الأنظمة الأساسية ، مثل
Geekbench ، لإثبات أن معالجات Apple المحمولة ليست أقل شأناً من معالجات Intel المحمولة وأجهزة سطح المكتب. لكنني كنت دائمًا متشككًا قليلاً في هذه الاختبارات عبر الأنظمة الأساسية (بالإضافة إلى
غيرها ) - هل تعكس حقًا سرعة أداء المهام الحقيقية التي أستخدم جهاز Mac الخاص بها؟
بصفتي باحثًا في الأساليب الرسمية ، يتعين علي بانتظام تشغيل SMT حلالا ، وعادة ما يكون
Z3 prover . قضيت الكثير من الوقت في دراسة خصائص أداء Z3. يحتوي على بعض الميزات التي لا يتم أخذها في الاعتبار في الاختبارات (عادةً ما يكون Z3 مترابطًا واحدًا). اشتريت مؤخرًا جهاز
iPhone XS جديدًا مزودًا بأحدث معالج Apple
A12 . وبطريقة ما ، مع عدم القيام بأي شيء ، قررت تجميع Z3 في iOS ومعرفة مدى سرعة عمل الهاتف الجديد (أو جهاز Mac الافتراضي المستقبلي).
الاختبار الأول
تبين أن الترجمة المتقاطعة Z3 بسيطة بشكل مدهش ، ما عليك سوى تغيير بضعة أسطر من التعليمات البرمجية. لقد نشرت مصادر تشغيل
Z3 على جهاز iOS الخاص بك . للاختبار ، أخذت بعض الاستفسارات من عملي الأخير حول
تحديد الحسابات الحسابية الرمزية : لكل حالة ،
تم استخراج SMT الذي تم إنشاؤه بواسطة
Rosette .
في الاختبار الأول ، قارنت جهاز iPhone XS بأحد أجهزة الكمبيوتر المكتبية التي تعمل على Intel Core i7-7700K - أفضل رقاقة Intel للسوق الاستهلاكية في الوقت الذي صنعت فيه السيارة قبل 18 شهرًا. كان من المفترض أن تفوز إنتل دون أي مشاكل ، ولكن تبين بشكل مختلف:
في هذا الاختبار لمدة 23 ثانية ، كان جهاز iPhone XS أسرع بنسبة 11٪ تقريبًا! لقد أبلغت عن هذا على Twitter ، لكن Twitter لا يترك مساحة كبيرة للتفاصيل ، لذلك سأقدمها هنا:
- هذا المعيار هو جزء من
QF_BV من SMT ، وبالتالي فإن Z3 يحل هذا الجزء باستخدام التفجير QF_BV و حلال SAT. - والنتيجة مستقرة تمامًا ، حتى إذا قمت بتشغيل الدورة عشر مرات: يدعم iPhone هذا الأداء ولا يبدو أنه يتباطأ بسبب ارتفاع درجة الحرارة. 1 . ومع ذلك ، لا يزال المؤشر عابرًا جدًا.
- سأل العديد من الناس عما إذا كان ذلك بسبب عدم الحتمية. ربما ، على منصات مختلفة ، يذهب حلالا بطريقة مختلفة بسبب استخدام أرقام عشوائية أو لسبب آخر؟ لكنني تحققت بعناية من الإصدار التفصيلي لـ Z3 ، ولا يمكن تفسير النتائج بهذا.
- ركز كلا النظامين Z3 4.8.1 ، والذي قمت بتجميعه باستخدام Clang مع نفس إعدادات التحسين. لقد أجريت أيضًا اختبارات على i7-7700K مع ثنائيات Z3 سابقة الإعداد (والتي يتم تجميعها بواسطة GCC) ، ولكنها أبطأ.
ما الذي يجري؟
كيف هذا ممكن؟ Core i7-7700K هو نفس معالج سطح المكتب. في مهمة واحدة ، تستهلك حوالي 45 واط وتعمل بتردد 4.5 جيجا هرتز. من ناحية أخرى. ربما لا تستهلك حتى 10 ٪ من هذه الطاقة وتعمل (نأمل) في مكان ما في نطاق 2 غيغاهرتز. علاوة على ذلك ، بعد اختبار مقارن ، راجعت التقرير حول استخدام بطارية iPhone: قال إن Slack استخدم طاقة أكبر بأربع مرات من تطبيق Z3 ، على الرغم من الوقت الأقل على الشاشة.
لا تقدم Apple معلومات كافية لفهم أداء Z3 على iPhone ، ولكن لحسن الحظ ، توفر Intel هذه المعلومات لمعالجها. بحثت حول
VTune لفترة من الوقت للعثور على اختناقات الأداء عند بدء تشغيل Z3 على سطح المكتب. كما لاحظ
Mat Soos ، معظم الوقت
يقضي حلال SAT
على التوزيع ، وهو
حساس جدًا لذاكرة التخزين المؤقت . يوافق VTune ويقول أن Z3 يقضي الكثير من الوقت في الانتظار في الذاكرة عند التكرار على الحرف المرصودة. لذا يبدو أن مفتاح الأداء هو حجم ذاكرة التخزين المؤقت ووقت استجابة الذاكرة. قد يفسر هذا التأثير سبب قوة iPhone في هذا الاختبار: تحتوي شريحة A12 على
ذاكرة تخزين مؤقت عملاقة L2 بوقت
استجابة منخفض ، ويبدو أيضًا أن لها وقت استجابة أفضل للذاكرة بعد فقدان ذاكرة التخزين المؤقت مقارنة بـ 7700K.
التقدم السريع لمعالجات آبل
لتأكيد النتائج ، أجريت تجربة أكثر شمولاً ، جمعت جميع أجهزة Apple التي يمكنني الحصول عليها. لقد اخترت أيضًا معيارًا مرجعيًا أطول بنحو 10 مرات (أي 4 دقائق على سطح المكتب) للتخفيف من المخاوف بشأن الاندفاعات في أداء وحدة المعالجة المركزية المتنقلة.
فيما يلي نتائج هذه الأجهزة (مع تواريخ الإصدار) لـ A7 ، أول معالج مستخدم 64 بت من Apple:
وتجدر الإشارة على الفور إلى أن معالج سطح المكتب i7-7700K متفوق على جهاز iPhone XS في هذا الاختبار الأطول. لكن جهاز iPhone منافس بشكل لا يصدق ، ويظهر النتيجة بين i7-7700K وسلفه ، i7-6700K ، والذي كان أسرع معالج سطح مكتب للمستهلكين قبل أقل من عامين بقليل.
للمتعة ، أضفت معالج Core m7-6Y75 آخر من جهاز MacBook 2016. في اختبار Z3 ، هاتفي أسرع بحوالي 50٪ من الكمبيوتر المحمول.
الشيء الرائع حقًا هنا هو الاتجاه: تحسن ثابت إلى حد ما بنسبة 30 ٪ سنويًا لهذا المعيار Z3. من الواضح أنه لا يجب عليك استخلاص نتائج بعيدة المدى من اختبار غبي واحد ، ولكن يبدو أنه بعد تكرارين ستصبح معالجات Apple مناسبة تمامًا لأحمال العمل.
2 . بصراحة ، لم أكن أتوقع أن نكون قريبين جدًا: الهندسة المعمارية الحديثة للهواتف الذكية لا تصدق!
بفضل Megan Cowan و Max Willsy و Eddie Ian لمساعدتهم في إجراء الاختبارات على الأجهزة الأخرى.
1 . لاحظ
ماكس أن iPhone مقاوم للماء ، لذلك يمكن التحقق من النظرية عن طريق غمره في حمام ثلجي. لكنني دفعت الكثير من المال للهاتف ولا أريد إجراء مثل هذه التجربة طواعية.
↑2 . أراهن على أن A12X في
iPad Pro الجديد أصبح أسرع بفضل
الغلاف الحراري الأكبر الذي يمنحه الجهاز اللوحي.
↑