💻 computer science

Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations

تقترح هذه الورقة نهج تحقق هجين يدمج بين دلالات الخطوة الصغيرة (small-step) والدلالات الكلية (big-step) عبر واجهة تجريدية مشتركة لتمكين التحقق الرسمي من تحسينات الحلقات الهيكلية، مثل بسط الحلقة الكامل (full loop unrolling)، ضمن مسار مترجم CompCert مع الحفاظ على جميع الضمانات الدلالية العليا.

المؤلفون الأصليون: David Knothe, Oliver Bringmann

نُشر 2026-02-24

📖 5 دقيقة قراءة🧠 قراءة متعمّقة

CC BY 4.0

المؤلفون الأصليون: David Knothe, Oliver Bringmann

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أنك مهندس معماري ماهر (المُترجم - Compiler) مُكلف بتجديد قلعة قديمة ضخمة (الكود المصدري - Source Code) وتحويلها إلى ناطحة سحاب حديثة وفعالة (لغة الآلة - Machine Code). هدفك هو جعل المبنى أسرع وأقل تكلفة في التشغيل، ولكن يجب أن تعد المالك بأنه لن يتغير أي شيء مهم. إذا استطاع المالك التجول في القلعة القديمة ورأى تنيناً ينفث النار في الردهة، فيجب أن يرى نفس التنين تماماً في نفس المكان في ناطحة السحاب الجديدة.

هذه الورقة البحثية تتحدث عن كيفية إثبات أن عمليات التجديد التي تقوم بها آمنة، وتحديداً عندما تقوم بتغييرات هيكلية كبرى مثل تحسينات الحلقات التكرارية (rearranging how the building handles repetitive tasks).

المخططان: "خطوة بخطوة" مقابل "الصورة الكبيرة"

لإثبات أن عملية التجديد آمنة، فأنت بحاجة إلى مجموعة من القواعد (semantics) لوصف كيفية عمل المبنى. تجادل الورقة بأنه لا ينبغي لك استخدام نوع واحد فقط من كتب القواعد؛ بل تحتاج إلى اثنين، ويجب أن تعرف متى تنتقل بينهما.

1. مخطط "خطوة بخطوة" (Small-Step Semantics)

فكر في هذا كأنه مجهر. إنه ينظر إلى المبنى طوبة تلو الأخرى.

كيف يعمل: يقول: "أولاً، الباب يفتح. ثم، الضوء يشتعل. ثم، الشخص يدخل".
الأفضل لـ: الإصلاحات الصغيرة والمحلية. مثل تغيير مصباح أو إعادة طلاء جدار. إنه رائع للتحقق من أن كل حركة هي قانونية.
المشكلة: عندما تريد نقل جناح كامل من القلعة (تحسين الحلقة - Loop Optimization)، فإن النظر في كل طوبة على حدة يكون مرهقاً ومربكاً. الأمر يشبه محاولة فهم سيمفونية من خلال الاستماع إلى نوتة كمان واحدة في كل مرة.

2. مخطط "الصورة الكبيرة" (Big-Step Semantics)

فكر في هذا كأنه رؤية من طائرة بدون طيار (درون) أو فيلم سينمائي.

كيف يعمل: يقول: "الشخص يمشي من الردهة إلى المطبخ". إنه يتخطى الخطوات التي في المنتصف وينظر فقط إلى البداية والنهاية.
الأفضل لـ: التغييرات الهيكلية. إذا كنت تريد أن تقول: "لنأخذ هذه الحلقة الكاملة من المشي ذهاباً وإياباً ونقوم بها دفعة واحدة"، فإن رؤية "الصورة الكبيرة" تجعل هذا الأمر سهلاً للإثبات.
المشكلة: تاريخياً، كان يُنظر إلى هذه الرؤية على أنها "أقل أماناً" لأنها لم تكن تستطيع بسهولة التعامل مع الحلقات اللانهائية (مثل باب لا يغلق أبداً) أو "التعطل" (مثل انهيار أرضية).

الفكرة الكبرى للورقة: "المترجم"

لسنوات، قرر المترجم الشهير CompCert (المعيار الذهبي للمترجمات الآمنة) التخلي عن مخطط "الصورة الكبيرة" تماماً والاعتماد فقط على مجهر "خطوة بخطوة". ظنوا أن هذا أكثر أماناً. لكن هذا جعل من الصعب جداً إضافة ميزات رائعة مثل فك حلقة التكرار (Loop Unrolling) (تنفيذ حلقة 10 مرات متتالية بدلاً من العودة في كل مرة) أو إخراج القرار من الحلقة (Loop Unswitching) (نقل نقطة اتخاذ القرار إلى خارج الحلقة).

تقترح هذه الورقة نهجاً هجيناً:

استخدم المجهر للأشياء المملة والصغيرة (مثل التحقق مما إذا كان المتغير رقماً).
انتقل إلى رؤية الدرون عندما تحتاج للقيام بالأعمال الهيكلية الثقيلة (تحريك الحلقات حول بعضها).
استخدم مترجماً: بنى المؤلفون "مترجماً عالمياً" (يسمى Behavioral Semantics) يتحدث اللغتين. إنه يترجم حركات "الصورة الكبيرة" إلى حركات "خطوة بخطوة" حتى تتمكن فحوصات السلامة الخاصة بالمترجم من فهمها.

الخدعة السحرية: التعامل مع الحلقات اللانهائية

العقبة التقنية الأكبر كانت الحلقات اللانهائية (divergence).

المشكلة القديمة: إذا استمرت الحلقة للأبد، فإن رؤية "الصورة الكبيرة" أحياناً لم تكن تستطيع تحديد ما إذا كانت تعمل للأبد أم أنها تستغرق وقتاً طويلاً جداً فقط. كان الأمر يشبه فيلماً توقف عند إطار واحد؛ لم تكن تعرف ما إذا كان الممثل نائماً أم أن جهاز العرض قد تعطل.
الحل: قام المؤلفون بترقية رؤية "الصورة الكبيرة". لقد أضافوا "عداداً" إلى القواعد. الآن، حتى لو استمرت الحلقة للأبد، يمكن لرؤية "الصورة الكبيرة" أن تثبت أنها تنتج بالفعل أحداثاً (مثل نبضات القلب) وليست مجرد متوقفة. هذا يجعل رؤية "الصورة الكبيرة" قوية وآمنة تماماً مثل رؤية "خطوة بخطوة".

أمثلة من الواقع: ماذا أصلحوا؟

اختبر المؤلفون هذه الطريقة الجديدة على CompCert ونجحوا في التحقق من تحسينين معقدين كان من الصعب إثباتهما سابقاً:

إخراج القرار من الحلقة (تشبيه "إشارة المرور"):
- السيناريو: تخيل حلقة حيث تقود سيارة حول مضمار. داخل المضمار، توجد إشارة مرور. إذا كانت الإشارة حمراء، تتوقف السيارة؛ إذا كانت خضراء، تنطلق.
- التحسين: إذا كانت إشارة المرور لا تغير لونها طوال الجولة، فلماذا نتحقق منها في كل مرة؟ يمكنك نقل عملية التحقق إلى خارج الحلقة.
- النتيجة: تقود السيارة في مضمار سلس دون انقطاع بدلاً من التوقف والتحرك. تثبت الورقة أن هذا آمن باستخدام رؤية "الصورة الكبيرة".
فك حلقة التكرار (تشبيه "خط تجميع المصنع"):
- السيناريو: مصنع لديه روبوت يبني 10 ألعاب. يوجد لافتة تقول: "إذا صنعت 10، توقف".
- التحسين: بما أننا نعرف بالضبط عدد الألعاب (10)، يمكننا ببساطة إزالة لافتة "التوقف" والحلقة. نحن فقط نكتب التعليمات: "ابنِ لعبة 1، ابنِ لعبة 2... ابنِ لعبة 10".
- النتيجة: لا يحتاج الروبوت للتحقق من اللافتة 10 مرات؛ هو فقط يقوم بالعمل. تثبت الورقة أن هذا آمن، حتى لو تعطل الروبوت في منتصف الطريق (التنفيذ الجزئي) أو علق في حلقة لانهائية.

لماذا يجب أن تهتم؟

هذه الورقة هي انتصار لـ الثقة.

للبرمجيات الحساسة للسلامة: إذا كنت تكتب برمجيات لجهاز تنظيم ضربات القلب، أو طائرة، أو مفاعل نووي، فلا يمكنك تحمل الأخطاء. تسمح هذه الطريقة للمهندسين باستخدام تحسينات قوية ومعقدة (لجعل البرمجيات أسرع وأصغر) دون كسر "ضمان السلامة".
للمستقبل: تُظهر الورقة أننا لسنا مضطرين للاختيار بين "آمن ولكن بطيء" و"سريع ولكن محفوف بالمخاطر". من خلال دمج نوعي المنطق (خطوة بخطوة والصورة الكبيرة)، يمكننا الحصول على أفضل ما في العالمين.

باختة القول: بنى المؤلفون جسراً بين طريقتين مختلفتين للتفكير في الكود. هذا الجسر يسمح للمترجمات بإجراء عمليات تجديد هيكلية معقدة على البرمجيات مع الحفاظ على ضمانات السلامة للتصميم الأصلي. إنه يشبه إثبات أنه يمكنك إعادة تصميم المخطط الأرضي للمنزل بالكامل دون أن تجعل المالك يسقط من خلال الأرضية.

إليك ملخص تقني مفصل للورقة البحثية بعنوان "الجمع بين دلالات الخطوة الصغيرة والدلالات الكبيرة للتحقق من تحسينات الحلقات التكرارية" (Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations) للباحثين ديفيد نوث وأوليفر برينجمان.

1. بيان المشكلة

تهدف المترجمات التي تم التحقق منها (Verified compilers)، مثل CompCert، إلى ضمان أن عملية الترجمة تحافظ على السلوك الملحوظ للبرامج المصدرية. تاريخيًا، انتقل CompCert من الدلالات الكبيرة (الطبيعية/Big-step) إلى الدلالات الصغيرة (التشغيلية/Small-step) لأن الأخيرة اعتُبرت أكثر تعبيرًا ووفرت إطارًا موحدًا لإثبات الحفاظ على الدلالات.

ومع ذلك، أدى هذا التحول إلى خلق عقبة كبيرة أمام التحويلات الهيكلية (Structural transformations)، لا سيما تحسينات الحلقات التكرارية (مثل إخراج الشرط من الحلقة - loop unswitching، وفك حلقات التكرار - loop unrolling).

محدودية الدلالات الصغيرة: بينما تعد ممتازة للتحويلات المحلية (مثل اختيار التعليمات)، تتطلب الدلالات الصغيرة عمليات "محاكاة" معقدة للتغييرات الهيكلية. هذه الإثباتات تتطلب علاقات مطابقة معقدة بين حالات المصدر والهدف، وغالبًا ما تتطلب تمريرًا يدويًا للثوابت (invariants) عبر خطوات التنفيذ الوسيطة. وهذا يجعل إثباتات تحسينات الحلقات التكرارية مملة، ضخمة، وصعبة التجزئة (modularization).
محدودية الدلالات الكبيرة: بينما تعد الدلالات الكبيرة مناسبة طبيعيًا للاستدلال الهيكلي (عبر الاستقراء على البنية النحوية)، افتقرت النسخة الأصلية من CompCert إلى القدرة التعبيرية اللازمة للتعامل مع التباعد/اللانهاية (divergence) والتنفيذ الجزئي (partial execution) بشكل صحيح بما يتماشى مع المتطلبات الصارمة للمترجمات التي تم التحقق منها.

المشكلة الجوهرية هي كيفية إعادة إدخال سهولة الدلالات الكبيرة للتحسينات الهيكلية دون التضحية بضمانات الصحة الصارمة والتعميمات العليا للإطار الحالي للدلالات الصغيرة.

2. المنهجية

يقترح المؤلفون نهجًا هجينًا يدمج كلا الأسلوبين الدلاليين في خط إنتاج واحد تم التحقق منه باستخدام تجريد الدلالات السلوكية (Behavioral Semantics).

أ. تجريد الدلالات السلوكية

يعرف المؤلفون واجهة مشتركة، وهي الدلالات السلوكية، والتي تجرد سلوك البرنامج إلى ثلاث خصائص (predicates):

الإنهاء (Termination): $p \Downarrow^t \sigma$ (البرنامج $p$ ينتهي بمسار $t$ وحالة نهائية $\sigma$ ).
التباعد (Divergence): $p \Downarrow^\tau_\infty$ (البرنامج $p$ يتباعد بمسار $\tau$ ، والذي يمكن أن يكون محدودًا أو لانهائيًا).
التقييم الجزئي (Partial Evaluation): $p \Downarrow^t$ (البرنامج $p$ ينفذ بادئة محدودة $t$ ولكنه لم ينتهِ أو يتباعد بعد).

يعالج هذا الإطار مسألة "الخطأ" (Undefined behavior) ضمنيًا عبر التقييمات الجزئية التي لا يمكن تمديدها.

ب. توسيع الدلالات الكبيرة التعاونية (Coinductive Big-Step Semantics)

لجعل الدلالات الكبيرة بنفس قدر تعبير الدلالات الصغيرة، قام المؤلفون بتوسيع دلالات Leroy التعاونية:

المسارات العامة: قاموا بتعديل حكم التباعد للتعامل مع المسارات المحدودة واللانهائية ( $\tau$ ) داخل خاصية تعاونية واحدة، بدلاً من الفصل بينهما.
آلية الحماية (Guard Mechanism): أدخلوا عدادًا للقيم الطبيعية ( $n$ ) وشرط حماية (guard) في قواعد التباعد. يضمن هذا أن المسار ليس فقط "من المحتمل" أن يكون لانهائيًا، بل هو مضمون الإنتاج خطوة بخطوة. هذا يحل مشكلة الحالة التي يمكن فيها لحلقة فارغة أن تتباعد نظريًا مع أي مسار لانهائي في التعريفات التعاونية القياسية.
الأحكام الجزئية: أضافوا قواعد لاستخلاص التقييمات الجزئية مباشرة من قواعد الخطوة الكبيرة، مما يسمح للإطار بالتقاط حالات "الخطأ" أو التنفيذات غير المكتملة.

ج. التكامل في خط الإنتاج (Pipeline Integration)

قام المؤلفون بدمج هذا في خط إنتاج CompCert عند التمثيل الوسيط Cminor:

من الخطوة الصغيرة إلى السلوكية: يتم تفسير Cminor القياسي ذو الخطوات الصغيرة كدلالات سلوكية.
التحويل بالخطوة الكبيرة: ينتقل خط الإنتاج إلى دلالات Cminor الكبيرة لتنفيذ تحسينات الحلقات التكرارية.
العودة إلى الخطوة الصغيرة: بعد التحسين، يتم نقل الكود مرة أخرى إلى دلالات الخطوة الصغيرة لبقية عملية الترجمة.

الضمان النظري:
أثبت المؤلفون أن:

Cminor ذو الخطوة الصغيرة والخطوة الكبيرة متكافئان سلوكيًا (الصحة والاكتمال).
إذا كان المصدر مستقبلاً (receptive) والهدف محددًا (determinate)، فإن الحفظ الأمامي (forward preservation) يستلزم الحفظ الخلفي (backward preservation) (وبالتالي التكافؤ الكامل).
يسمح هذا بإدخال تحويلات الخطوة الكبيرة في منتصف خط إنتاج الخطوة الصغيرة مع الحفاظ على جميع تعميمات الصحة العليا لـ CompCert.

3. المساهمات الرئيسية

إطار سلوكي موحد: واجهة دنيا تربط بين دلالات الخطوة الصغيرة والدلالات الكبيرة، مما يسمح بإثبات التعميمات حول حفظ السلوك مرة واحدة وتطبيقها على كلا الأسلوبين.
دلالات كبيرة تعاونية ذات قدرة تعبيرية عالية: امتداد لدلالات Leroy التي تتعامل بشكل صحيح مع التباعد بالمسارات العامة (المحدودة واللانهائية) والتنفيذ الجزئي، مما يجعلها مكافئة تعبيريًا لدلالات الخطوة الصغيرة.
تحسينات الحلقات التكرارية التي تم التحقق منها في CompCert: تنفيذ والتحقق من صحة عدة تحسينات للحلقات في Cminor ذي الخطوة الكبيرة والتي لم تكن مثبتة سابقًا في CompCert:
- إخراج الشرط من الحلقة (Loop Unswitching): رفع الفروع المستقلة خارج الحلقات.
- فك الحلقة الكامل (Full Loop Unrolling): فك الحلقات ذات الحدود الثابتة (مثل حساب $10!$ ثابتًا).
- إزالة الحلقة الصامتة (Silent Loop Elimination): إزالة أجسام الحلقات التي لا تخرج أبدًا ولا تصدر أي أحداث.
إثبات التكافؤ: إثبات رسمي بأن خط الإنتاج الهجين يحافظ على جميع تعميمات الصحة الأصلية لـ CompCert، بما في ذلك خصائص الترجمة والربط المنفصلين.

4. النتائج

التنفيذ: قام المؤلفون بتنفيذ هذه التحويلات في مترجم CompCert (باستخدام مساعد الإثبات Rocq).
التحقق: نجحوا في التحقق من صحة إخراج الشرط من الحلقة وفك الحلقة الكامل:
- مثال: حلقة تحسب $10!$ تم فكها وتحسينها عبر نشر الثوابت (constant propagation) لتعيد الثابت 3628800 مباشرة.
تعقيد الإثبات:
- الخطوة الكبيرة: كانت الإثباتات أكثر تجزئة بشكل ملحوظ. بالنسبة لإخراج الشرط من الحلقة، اعتمد الإثبات على الاستقراء الهيكلي ولمحة واحدة (indep_spec) تتعلق بالاستقلالية، متجنبًا علاقات مطابقة الحالة المعقدة.
- مقارنة بالخطوة الصغيرة: رسم المؤلفون مخططًا لإثبات الخطوة الصغيرة لنفس التحويل، موضحين أنه يتطلب "مُطابقًا شرطيًا" (match predicate) معقدًا مع حالات متعددة ( $=0, =1, =2$ ) للتعامل مع الحالات الوسيطة حيث يتم تقييم الشرط في أوقات مختلفة في المصدر مقابل الهدف. نتج عن ذلك إثباتات "ضخمة" ذات ثوابت مبعثرة.
حجم الكود: رغم التعامل مع ثلاث حالات سلوكية (الإنهاء، الجزئي، التباعد)، فإن التعريف الكامل وإثبات فك الحلقة في أسلوب الخطوة الكبيرة لم يتجاوز ~700 سطر من كود Rocq.

5. الأهمية

العملية للمترجمات التي تم التحقق منها: توضح الورقة أن المترجمات التي تم التحقق منها لا يجب أن تكون متجانسة في أسلوب دلالاتها. فهي تثبت جدوى استراتيجية استخدام الدلالات الصغيرة للتحويلات المحلية القريبة من العتاد والدلالات الكبيرة للتحسينات الهيكلية عالية المستوى.
التجزئة وإعادة الاستخدام: يحسن النهج بشكل كبير من تجزئة إثباتات الصحة. فالتعميمات حول خصائص البرنامج (مثل استقلالية التعبيرات) يمكن إثباتها مرة واحدة وإعادة استخدامها عبر تحسينات مختلفة، بينما تتطلب إثباتات الخطوة الصغيرة غالبًا إعادة إثبات هذه الثوابت لكل سيناريو مطابقة خطوة محدد.
القابلية للتطبيق الأوسع: بينما تم عرض ذلك على CompCert، فإن المنهجية (التجريد السلوكي والدلالات التعاونية الموسعة) قابلة للتطبيق على المترجمات والتمثيلات الوسيطة الأخرى التي تم التحقق منها.
سد الفجوة: يحل هذا العمل التوتر التاريخي بين القدرة التعبيرية للدلالات الصغيرة وراحة الدلالات الكبيرة، مما يسمح لمطوري المترجمات باختيار الأداة الأكثر طبيعية لكل مرحلة تحسين محددة دون المساس بضمان الصحة الإجمالي.

باختًا، يقدم هذا العمل أساسًا نظريًا وعمليًا قويًا لدمج تحسينات الحلقات الهيكلية في المترجمات التي تم التحقق منها، مما يثبت أن الدلالات الكبيرة يمكن أن تتعايش مع خطوط إنتاج الخطوة الصغيرة وتعززها.