كيف تكتشف عيوب المرونة في أنظمة لم تُبنَ بعد؟

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

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

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

ابدأ بتعريف ما يعنيه «صحيح»

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

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

النموذج المبسط يكشف المشكلة الأساسية

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

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

عامل «الغريم» في التزامن والفشل

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

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

الافتراضات جزء من التصميم

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

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

ما الذي يتغير عملياً؟

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

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