خصائص السلامة والحيوية

لطالما تم تحديد خصائص تنفيذ برنامج حاسوبي - وخاصة للأنظمة المتزامنة والموزعة - من خلال إعطاء خصائص أمان ("لا تحدث أشياء سيئة") وخصائص حيوية ("تحدث أشياء جيدة"). ^{[ 1 ]}

البرنامج صحيح تمامًا فيما يتعلق بشرط مسبق${\displaystyle P}$والشرط اللاحق${\displaystyle Q}$إذا بدأ أي تنفيذ في حالة مُرضية${\displaystyle P}$ينتهي الأمر بحالة مُرضية${\displaystyle Q}$. الصحة الكاملة هي اقتران بين خاصية السلامة وخاصية الحيوية: ^{[ 2 ]}

• تمنع خاصية الأمان هذه "الأمور السيئة": عمليات التنفيذ التي تبدأ في حالة مُرضية${\displaystyle P}$وتنتهي بحالة نهائية لا تفي بالغرض${\displaystyle Q}$لبرنامج${\displaystyle C}$تُكتب خاصية الأمان هذه عادةً باستخدام ثلاثية هوار.${\displaystyle \{P\}C\{Q\}}$.
• خاصية الحيوية، أو "الشيء الجيد"، هي ذلك التنفيذ الذي يبدأ في حالة مُرضية${\displaystyle P}$ينتهي.

لاحظ أن الأمر السيئ منفصل، ^{[ 3 ]} لأنه يحدث في مكان محدد أثناء التنفيذ. أما "الأمر الجيد" فلا يشترط أن يكون منفصلاً، لكن خاصية استمرارية الإنهاء منفصلة.

أظهرت التعريفات الرسمية التي طُرحت لاحقًا لخصائص السلامة ^{[ 4 ]} وخصائص التشغيل ^{[ 5 ]} أن هذا التفكيك ليس جذابًا بديهيًا فحسب، بل هو أيضًا شامل: فجميع خصائص التنفيذ هي عبارة عن اقتران بين خصائص السلامة وخصائص التشغيل. ^{[ 5 ]} علاوة على ذلك، قد يكون إجراء هذا التفكيك مفيدًا، لأن التعريفات الرسمية تُتيح إثبات ضرورة استخدام طرق مختلفة للتحقق من خصائص السلامة مقارنةً بالتحقق من خصائص التشغيل. ^{[ 6 ] [ 7 ]}

تمنع خاصية الأمان حدوث أمور سيئة محددة أثناء التنفيذ. ^{[ 1 ]} وبالتالي، تحدد خاصية الأمان ما هو مسموح به من خلال بيان ما هو ممنوع. ويعني اشتراط أن يكون الأمر السيئ محددًا أن وقوع أمر سيئ أثناء التنفيذ يحدث بالضرورة في نقطة محددة. ^{[ 5 ]}

تتضمن أمثلة الأشياء السيئة المنفصلة التي يمكن استخدامها لتحديد خاصية السلامة ما يلي: ^{[ 5 ]}

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

يمكن وصف تنفيذ برنامج ما بشكل رسمي من خلال إعطاء التسلسل اللانهائي لحالات البرنامج الناتجة أثناء تقدم التنفيذ، حيث تتكرر الحالة الأخيرة لبرنامج منتهي بشكل لانهائي. بالنسبة لبرنامج معين، لنفترض${\displaystyle S}$تشير إلى مجموعة حالات البرنامج الممكنة،${\displaystyle S^{*}}$تشير إلى مجموعة التسلسلات المحدودة لحالات البرنامج، و${\displaystyle S^{\omega }}$تشير إلى مجموعة التسلسلات اللانهائية لحالات البرنامج. العلاقة${\displaystyle \sigma \leq \tau }$ينطبق على التسلسلات${\displaystyle \sigma }$و${\displaystyle \tau }$إذا${\displaystyle \sigma }$هو بادئة لـ${\displaystyle \tau }$أو${\displaystyle \sigma }$يساوي${\displaystyle \tau }$[ ^{5 ]​}

إحدى خصائص البرنامج هي مجموعة عمليات التنفيذ المسموح بها.

الخاصية الأساسية لخاصية السلامة${\displaystyle SP}$هو: إذا تم تنفيذ بعض العمليات${\displaystyle \sigma }$لا يرضي${\displaystyle SP}$ثم يحدث الشيء السيئ المحدد لخاصية السلامة هذه في مرحلة ما من${\displaystyle \sigma }$لاحظ أنه بعد حدوث أمر سيئ كهذا ، إذا نتج عن تنفيذ لاحق تنفيذ ${\displaystyle \sigma ^{\prime }}$، ثم${\displaystyle \sigma ^{\prime }}$كما أنه لا يرضي${\displaystyle SP}$، لأن الشيء السيئ في${\displaystyle \sigma }$يحدث أيضًا في${\displaystyle \sigma ^{\prime }}$نعتبر هذا الاستنتاج حول استحالة إصلاح الأمور السيئة السمة المميزة لـ${\displaystyle SP}$أن تكون خاصية أمان. إن صياغة هذا في منطق المسندات يعطي تعريفًا رسميًا لـ${\displaystyle SP}$كونها خاصية أمان. ^{[ 5 ]}

${\displaystyle \forall \sigma \in S^{\omega }:\sigma \notin SP\implies (\exists \beta \leq \sigma$ :(\forall \tau \in S^{\omega }:\beta \tau \notin SP))}

هذا التعريف الرسمي لخصائص السلامة يعني أنه إذا كان التنفيذ${\displaystyle \sigma }$ يفي بخاصية السلامة${\displaystyle SP}$ثم كل بادئة من${\displaystyle \sigma }$(مع تكرار الحالة الأخيرة) يفي أيضاً بـ${\displaystyle SP}$.

تُحدد خاصية الحيوية أمورًا جيدة لكل عملية تنفيذ، أو بعبارة أخرى، تصف شيئًا يجب أن يحدث أثناء التنفيذ. ^{[ 1 ]} لا يشترط أن يكون الشيء الجيد منفصلًا، فقد يشمل عددًا لا نهائيًا من الخطوات. ومن أمثلة الأشياء الجيدة المستخدمة لتعريف خاصية الحيوية ما يلي: ^{[ 5 ]}

• إنهاء عملية تنفيذ بدأت في حالة مناسبة؛
• عدم إنهاء عملية تنفيذ بدأت في حالة مناسبة؛
• ضمان الدخول النهائي إلى قسم حرج كلما تمت محاولة الدخول؛
• الوصول العادل إلى مورد ما في ظل وجود نزاع.

الشيء الجيد في المثال الأول منفصل، لكن ليس في الأمثلة الأخرى.

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

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

للتمييز عن خاصية السلامة، خاصية الحيوية${\displaystyle LP}$لا يمكن استبعاد أي بادئة محدودة ${\displaystyle \alpha \in S^{*}}$^{[ 8 ]} لتنفيذ حكم الإعدام (لأن مثل هذا${\displaystyle \alpha }$سيكون ذلك "أمرًا سيئًا"، وبالتالي، سيحدد خاصية أمان. وهذا يؤدي إلى تحديد خاصية حيوية.${\displaystyle LP}$أن تكون خاصية لا تستبعد أي بادئة محدودة. ^{[ 5 ]}

${\displaystyle \forall \alpha \in S^{*}:(\exists \tau \in S^{\omega }:\alpha \tau \in LP)}$

لا يقتصر هذا التعريف على كون الشيء الجيد منفصلاً، بل يمكن أن يشمل كل شيء .${\displaystyle \tau }$، وهو تنفيذ لا نهائي الطول.

استخدم لامبورت مصطلحي "خاصية الأمان" و "خاصية الحيوية" في بحثه المنشور عام 1977 ^{[ 1 ]} حول إثبات صحة البرامج متعددة العمليات (المتزامنة) . وقد استعار هذين المصطلحين من نظرية شبكات بتري ، التي كانت تستخدم مصطلحي " الحيوية " و" التقييد" لوصف كيفية تطور عملية إسناد "الرموز" في شبكة بتري إلى "مواقعها"؛ وكان أمان شبكة بتري شكلاً محدداً من أشكال التقييد . ثم وضع لامبورت تعريفاً رسمياً للأمان في دورة تدريبية قصيرة لحلف الناتو حول الأنظمة الموزعة في ميونيخ. ^{[ 9 ]} وقد افترض هذا التعريف أن الخصائص ثابتة في ظل التقطيع . يظهر التعريف الرسمي للأمان المذكور أعلاه في بحث لألبيرن وشنايدر؛ ^{[ 5 ]} بينما يظهر الربط بين الصياغتين الرسميتين لخصائص الأمان في بحث لألبيرن وديمرز وشنايدر. ^{[ 10 ]}

يقدم ألبيرن وشنايدر ^{[ 5 ]} التعريف الرسمي للحيوية، مصحوبًا ببرهان على إمكانية بناء جميع الخصائص باستخدام خصائص السلامة وخصائص الحيوية. وقد استُلهم هذا البرهان من رؤية غوردون بلوتكين القائلة بأن خصائص السلامة تُقابل المجموعات المغلقة ، بينما تُقابل خصائص الحيوية المجموعات الكثيفة في طوبولوجيا طبيعية على المجموعة.${\displaystyle S^{\omega }}$من سلاسل لا نهائية من حالات البرنامج. ^{[ 11 ]} لاحقًا، لم يكتفِ ألبيرن وشنايدر ^{[ 12 ]} بتقديم توصيفٍ لأتمتة بوشي للتعريفات الرسمية لخصائص السلامة وخصائص الحيوية، بل استخدما أيضًا هذه الصيغ الآلية لإظهار أن التحقق من خصائص السلامة يتطلب ثابتًا ، وأن التحقق من خصائص الحيوية يتطلب حجة أساس متين . وكانت المطابقة بين نوع الخاصية (السلامة مقابل الحيوية) ونوع البرهان (الثبات مقابل الأساس المتين) حجة قوية على أن تقسيم الخصائص إلى سلامة وحيوية (بدلًا من أي تقسيم آخر) كان مفيدًا، إذ إن معرفة نوع الخاصية المراد إثباتها تحدد نوع البرهان المطلوب.