Mechanizing Asynchronous Distributed Algorithms in Rocq: The Echo Algorithm as a Case Study

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

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

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

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

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

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

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