الالتزام على مرحلتين ومستقبل النظم الموزعة

في هذه المقالة ، نحاكي ونفحص بروتوكول الالتزام ثنائي الطور باستخدام TLA +.

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

الطور ارتكاب المشكلة

تمر المعاملة عبر مديري الموارد (RM) . يجب أن توافق جميع RMs على ما إذا كان سيتم إتمام المعاملة أو إحباطها .

يتخذ مدير المعاملات (TM) القرار النهائي: الالتزام أو الإلغاء . شرط الالتزام هو الاستعداد لإلزام جميع RMs. خلاف ذلك ، ينبغي إلغاء المعاملة.

بعض الملاحظات على النمذجة

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

يمكن RM فقط قراءة حالة TM وقراءة / تحديث حالته الخاصة. لا يمكن قراءة حالة مدير موارد آخر. يمكن لـ TM قراءة حالة جميع عقد RM وقراءة / تحديث حالته الخاصة.

تعاريف

تقوم الخطوط 9-10 بتعيين rmState الأولي لكل RM working ، و TM init .

يكون canCommit true إذا كانت جميع RMs "جاهزة" (جاهزة للالتزام). إذا كان RM موجودًا في الحالة النهائية ، يصبح canAbort .



النمذجة TM بسيط. يتحقق مدير المعاملات من إمكانية الالتزام أو الإلغاء - وبالتالي يقوم بتحديث tmState .

هناك احتمال أن TM لن تكون قادرة على جعل tmState "غير قابلة للوصول" ، ولكن فقط إذا TMMAYFAIL تعيين ثابت TMMAYFAIL على " true قبل التحقق من صحة النموذج. في تسميات TLA + تحدد درجة الذرية ، أي درجة تفصيلها. وفقًا للتسميات F1 و F2 ، فإننا نشير إلى أن المشغلين المقابلين يتم إجراؤهم بطريقة غير تشريحية (بعد فترة زمنية غير محددة) فيما يتعلق بالمشغلين السابقين.

نموذج RM

نموذج RM بسيط أيضًا. نظرًا لأن الدول "العاملة" و "المعدة" غير نهائية ، تختار RM بشكل غير حاسم بين الإجراءات حتى تصل إلى الحالة النهائية. يمكن لـ RM "العاملة" الدخول في حالة "المقاطعة" أو "المعدة". RM "Prepared" تتوقع الالتزام / الإلغاء من TM - وتعمل وفقًا لذلك. يوضح الشكل أدناه تحولات الحالة المحتملة لجذر متوسط. لكن لاحظ أن لدينا العديد من RMs ، كل منها يمر عبر ولاياته وفقًا لسرعته الخاصة دون معرفة حالة RMs الأخرى.

مرحلتين نموذج الالتزام

نحن بحاجة إلى التحقق من اتساق التزامنا على مرحلتين: بحيث لا توجد RM مختلفة ، واحدة منها تقول "ارتكاب" والآخر "إجهاض".

يتحقق المسند المكتمل من عدم تعليق البروتوكول إلى الأبد: في النهاية ، يصل كل RM إلى الحالة النهائية aborted أو aborted .

نحن الآن على استعداد لاختبار نموذج البروتوكول. في البداية ، قمنا بتعيين TMMAYFAIL=FALSE, RM=1..3 لبدء البروتوكول بثلاثة RM و TM واحد ، في تكوين موثوق. يستغرق اختبار النموذج 15 ثانية ويقول إنه لا توجد أخطاء. كل من Consistency Completed راضون عن أي تنفيذ بروتوكول ممكن مع أي تناوب لإجراءات RM وإجراءات TM.



الآن قم بتعيين TMMAYFAIL=TRUE وأعد تشغيل الشيك. ينتج البرنامج بسرعة النتيجة المعاكسة ، حيث تعطل RM في انتظار استجابة من TM غير متوفر.



نرى أنه في State=4 تمت مقاطعة التحولات RM2 ، في State=7 تمت مقاطعة التحولات RM3 ، في State=8 يذهب TM إلى حالة "hang hang" ويقع في State=9 . في State=10 يتجمد النظام لأن RM1 يبقى إلى الأبد في حالة جاهزة ، في انتظار قرار من TM سقط.

محاكاة BTM

لتجنب تجميد المعاملات ، نضيف نسخة احتياطية TM (BTM) ، والتي تتحكم بسرعة في حالة عدم توفر TM الرئيسي. يستخدم BTM نفس منطق TM لاتخاذ القرارات. وللبساطة ، نفترض أن BTM لا تعطل أبدا.



عندما نختبر النموذج من خلال عملية BTM المضافة ، نحصل على رسالة خطأ جديدة.



لا يمكن لـ BTM قبول التزام لأن حالتنا الأصلية ، canCommit تنص على أن جميع RMstates يجب أن تكون "معدة" ولا تأخذ في الاعتبار الشرط RMstates في أن بعض RMs قد حصلت بالفعل على قرار التزام من TM الأصلي قبل أن يتحكم TMB. من الضروري إعادة كتابة شروط canCommit مع مراعاة مثل هذا الموقف.



النجاح! عندما نختبر النموذج ، نحقق كل من الاتساق والكمال ، حيث أن BTM تتحكم وتستكمل المعاملة في حالة سقوط TM. هنا هو نموذج 2PCwithBTM في TLA + (BTM والخط الثاني من canCommit غير مبدئي في البداية) وقوات الدفاع الشعبي المقابلة .

ماذا لو فشل RM أيضا؟

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





من الضروري أيضًا تحسين canAbort مع مراعاة حالة عدم canAbort . يمكن أن يتخذ TM القرار "معطلاً" إذا كانت أي من الخدمات في حالة انقطاع أو يتعذر الوصول إليها. إذا تم حذف هذا الشرط ، فإن RM الساقطة وغير المستعادة سوف يقطع تقدم العملية. بالطبع ، مرة أخرى ، يجب أن تفكر في RM ، الذي تعلم قرار إتمام المعاملة من المصدر TM.

تحقق النموذج

عندما نختبر النموذج ، هناك مشكلة عدم الاتساق! كيف يمكن أن يحدث هذا؟ نحن تتبع التتبع.

مع State=6 جميع RMs في حالة استعداد ، اتخذت TM قرارًا بإكمال الصفقة ، RM1 رأيت هذا القرار وتحولت إلى ملصق RC ، مما يعني الاستعداد لتغيير حالته إلى "مكتمل". (تذكر RM1 ، سيتم إطلاق هذه البندقية في الفعل الأخير). لسوء الحظ ، يقع TM في State=7 ، ويصبح RM2 غير متاح في State=8 . في الخطوة التاسعة ، تتحكم النسخة الاحتياطية لـ BTM وتقرأ حالة RMs الثلاثة على أنها "معدة ، لا يمكن الوصول إليها ، معدة" - وتقرر إلغاء المعاملة في الخطوة العاشرة. تذكر RM1؟ يقرر إكمال المعاملة لأنه تلقى مثل هذا القرار من TM الأصلي ، ويدخل في حالة committed في الخطوة 11. في State=13 يفي RM3 بقرار إلغاء المعاملة من BTM ويدخل في الحالة aborted - والآن قطعنا التنسيق مع RM1.

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

يتوفر ملف نموذج TLA + محدث هنا ، بالإضافة إلى ملف PDF المقابل .

استحالة FLP

إذن ماذا حدث؟ عثرنا على نظرية فيشر ، لينش ، باترسون (FLP) حول استحالة التوافق في نظام غير متزامن مع الفشل.

في مثالنا ، لا يمكن لـ BTM أن تقرر بشكل صحيح ما إذا كانت RM2 في حالة فاشلة أم لا - وتقرر بشكل غير صحيح إحباط المعاملة. إذا اتخذ TM الأصلي القرار فقط ، فإن عدم الدقة في التعرف على الفشل لن يكون مشكلة. سوف RM تطيع أي قرار TM ، بحيث سيتم الحفاظ على الاتساق والتقدم.

المشكلة هي أن لدينا كائنين يتخذان القرارات: TM و BTM ، فهم ينظرون إلى حالة RM في أوقات مختلفة ويتخذون قرارات مختلفة. هذا التباين في المعلومات هو أصل كل الشرور في النظم الموزعة.

لا تختفي المشكلة حتى مع التوسع في التزام ثلاثي المراحل. فيما يلي التزام من ثلاث مراحل تم تصميمه في TLA + ( إصدار pdf ) ، وفيما يلي تتبع خطأ يوضح أنه قد تم انتهاك التقدم هذه المرة (على صفحة Wikipedia حول التزام من ثلاث مراحل ، يتم توضيح الموقف عندما يتجمد RM1 بعد تلقي قرار قبل الالتزام ، و RM2 الالتزام ارتكاب ، الذي ينتهك الاتساق).

تحاول باكسوس جعل العالم مكانًا أفضل.

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

يمكنك محاكاة TM على نظام مجموعة مع ثلاث نقاط Paxos ، وهذا سيؤدي إلى حل مشكلة عدم تناسق TM / BTM. أو ، كما أظهر Gray and Lampport في مقال علمي حول الإجماع في تنفيذ المعاملة ، إذا استخدمت RM حاوية Paxos لتخزين قراراتها في وقت واحد مع استجابة TM ، فإن هذا يلغي خطوة واحدة إضافية في خوارزمية البروتوكول القياسي.