Safety and liveness properties
کمپیوٹر پروگرام کے نفاذ کی خصوصیات-خاص طور پر ہم آہنگی اور تقسیم شدہ نظاموں کے لیے-طویل عرصے سے حفاظتی خصوصیات ("بری چیزیں نہیں ہوتیں") اور زندہ خصوصیات ("اچھی چیزیں ہوتی ہیں") دے کر وضع کی گئی ہیں۔ ایک سادہ سی مثال حفاظت اور زندگی کی وضاحت کرے گی۔ ایک پروگرام پیشگی شرط اور پوسٹ کنڈیشن کے حوالے سے مکمل طور پر درست ہے اگر کسی ایسی حالت میں شروع کیا گیا کوئی عمل جو تسلی بخش حالت میں ختم ہوتا ہے۔ مکمل درستگی ایک حفاظتی پراپرٹی اور ایک زندہ پراپرٹی کا امتزاج ہے: حفاظتی پراپرٹی ان "بری چیزوں" کو منع کرتی ہے: ایسی سزائے موت جو تسلی بخش حالت میں شروع ہوتی ہے اور حتمی حالت میں ختم ہوتی ہے جو مطمئن نہیں ہوتی ہے۔ کسی پروگرام کے لیے، یہ حفاظتی خاصیت عام طور پر ہور ٹرپل کا استعمال کرتے ہوئے لکھی جاتی ہے۔ زندگی کی خاصیت، "اچھی چیز"، یہ ہے کہ جو عمل اطمینان بخش حالت میں شروع ہوتا ہے وہ ختم ہو جاتا ہے۔ نوٹ کریں کہ ایک بری چیز مجرد ہوتی ہے، کیونکہ یہ پھانسی کے دوران ایک خاص جگہ پر ہوتی ہے۔ ایک "اچھی چیز" کو مجرد ہونے کی ضرورت نہیں ہے، لیکن ختم کرنے کی زندہ خاصیت مجرد ہے۔ رسمی تعریفیں جو بالآخر حفاظتی خصوصیات اور زندہ خصوصیات کے لیے تجویز کی گئیں تھیں اس سے یہ ظاہر ہوتا ہے کہ یہ سڑنا نہ صرف بدیہی طور پر پرکشش ہے بلکہ مکمل بھی ہے: پھانسی کی تمام خصوصیات حفاظت اور زندہ خصوصیات کا امتزاج ہیں۔ مزید برآں، سڑنا مددگار ثابت ہوسکتا ہے، کیونکہ رسمی تعریفیں اس ثبوت کو قابل بناتی ہیں کہ حفاظتی خصوصیات کی تصدیق کے لیے مختلف طریقے استعمال کیے جانے چاہئیں بمقابلہ زندہ خصوصیات کی تصدیق کے لیے۔ سیفٹی ایک سیفٹی پراپرٹی پھانسی کے دوران غیر متزلزل بری چیزوں کو ہونے سے منع کرتی ہے۔ اس طرح ایک حفاظتی پراپرٹی اس بات کی خصوصیت رکھتی ہے کہ جس چیز کی اجازت ہے وہ یہ بتا کر دی جاتی ہے کہ کیا ممنوع ہے۔ بری چیز کے مجرد ہونے کی ضرورت کا مطلب یہ ہے کہ پھانسی کے دوران ہونے والی بری چیز لازمی طور پر کسی قابل شناخت مقام پر واقع ہوتی ہے۔ ایک غیر متزلزل بری چیز کی مثالیں جو حفاظتی خاصیت کی وضاحت کے لیے استعمال کی جا سکتی ہیں ان میں شامل ہیں: ایک ایسا عمل جو کسی دی گئی پیشگی شرط کو پورا کرنے والی حالت میں شروع ہوتا ہے ختم ہو جاتا ہے، لیکن حتمی حالت مطلوبہ پوسٹ کنڈیشن کو پورا نہیں کرتی ہے۔ دو ہم آہنگی کے عمل کا نفاذ، جہاں دونوں عمل کے لیے پروگرام ایک اہم حصے کے اندر بیانات کو نامزد کرتا ہے۔ دو ہم آہنگی کے عمل کا نفاذ جہاں ہر عمل دوسرے کی حالت بدلنے کا انتظار کر رہا ہے (جسے ڈیڈ لاک کہا جاتا ہے)۔ کسی پروگرام کے نفاذ کو پروگرام کی انفنائٹ سیکوینس دے کر باضابطہ طور پر بیان کیا جا سکتا ہے جس میں کہا گیا ہے کہ اس کے نتیجے میں عمل درآمد ہوتا ہے، جہاں ایک اختتامی پروگرام کے لیے آخری حالت کو لامحدود طور پر دہرایا جاتا ہے۔ دلچسپی کے پروگرام کے لیے، آئیے ممکنہ پروگرام کی حالتوں کے سیٹ کی نشاندہی کریں، پروگرام کی حالتوں کے محدود ترتیبات کے سیٹ کی نشاندہی کریں، اور پروگرام کی حالتوں کے لامحدود ترتیبات کے سیٹ کی نشاندہی کریں۔ رشتہ ترتیبات کے لیے ہے اور آئی ایف ایف یا مساوی کا سابقہ ہے۔ کسی پروگرام کی خاصیت اجازت شدہ سزائے موت کا مجموعہ ہے۔ حفاظتی پراپرٹی کی لازمی خصوصیت یہ ہے کہ: اگر کچھ عمل درآمد مطمئن نہیں ہوتا ہے تو اس حفاظتی پراپرٹی کے لیے تعریف شدہ بری چیز کسی وقت واقع ہوتی ہے۔ نوٹ کریں کہ اس طرح کی بری چیز کے بعد، اگر مزید پھانسی کے نتیجے میں پھانسی دی جاتی ہے، تو یہ بھی مطمئن نہیں ہوتا، کیونکہ اس میں بری چیز بھی ہوتی ہے۔ ہم بری چیزوں کی ناقابل تلافی کے بارے میں اس نتیجے کو حفاظتی ملکیت ہونے کی وضاحتی خصوصیت کے طور پر لیتے ہیں۔ پیش گوئی منطق میں اس کو باضابطہ بنانا حفاظتی پراپرٹی ہونے کی باضابطہ تعریف دیتا ہے۔ حفاظتی خصوصیات کے لیے اس رسمی تعریف کا مطلب یہ ہے کہ اگر کوئی عمل حفاظتی خاصیت کو مطمئن کرتا ہے تو (آخری حالت کو دہرانے کے ساتھ) کا ہر سابقہ بھی مطمئن کرتا ہے۔ زندگی ایک زندگی کی خاصیت ہر پھانسی کے لیے اچھی چیزیں تجویز کرتی ہے یا، مساوی طور پر، کسی ایسی چیز کی وضاحت کرتی ہے جو پھانسی کے دوران ہونی چاہیے۔ اچھی چیز مجرد ہونے کی ضرورت نہیں ہے-اس میں لامحدود تعداد میں اقدامات شامل ہو سکتے ہیں۔ لائیونیس پراپرٹی کی وضاحت کے لیے استعمال ہونے والی اچھی چیز کی مثالوں میں شامل ہیں: کسی مناسب حالت میں شروع ہونے والی پھانسی کو ختم کرنا ؛ کسی مناسب حالت میں شروع ہونے والی پھانسی کو ختم نہ کرنا ؛ جب بھی اندراج کی کوشش کی جائے تو کسی اہم حصے میں حتمی طور پر داخلے کی ضمانت ؛ تنازعہ کی موجودگی میں کسی وسائل تک منصفانہ رسائی۔ پہلی مثال میں اچھی چیز مجرد ہے لیکن دوسروں میں نہیں۔ ایک مخصوص ریئل ٹائم باؤنڈ کے اندر جواب پیش کرنا لائیونیس پراپرٹی کے بجائے حفاظتی پراپرٹی ہے۔ اس کی وجہ یہ ہے کہ ایک مجرد بری چیز پر پابندی عائد کی جا رہی ہے: ایک جزوی عمل جو اس حالت میں پہنچتا ہے جہاں جواب ابھی تک پیش نہیں کیا گیا ہے اور گھڑی کی قیمت (ایک ریاستی متغیر) باؤنڈ کی خلاف ورزی کرتی ہے۔ ڈیڈ لاک فریڈم ایک حفاظتی خاصیت ہے: "بری چیز" ڈیڈ لاک ہے (جو مجرد ہے)۔ زیادہ تر وقت، یہ جاننا کہ ایک پروگرام بالآخر کچھ "اچھا کام" کرتا ہے تسلی بخش نہیں ہے ؛ ہم یہ جاننا چاہتے ہیں کہ پروگرام کچھ مراحل کے اندر یا کچھ ڈیڈ لائن سے پہلے "اچھا کام" انجام دیتا ہے۔ ایک ایسی پراپرٹی جو "اچھی چیز" کو ایک مخصوص باؤنڈ دیتی ہے وہ ایک حفاظتی پراپرٹی ہے (جیسا کہ اوپر بیان کیا گیا ہے)، جبکہ کمزور پراپرٹی جو محض باؤنڈ موجود ہونے کا دعوی کرتی ہے وہ ایک لائیونیس پراپرٹی ہے۔ اس طرح کی لائیونیس پراپرٹی کو ثابت کرنا ممکنہ طور پر سخت حفاظتی پراپرٹی کو ثابت کرنے سے زیادہ آسان ہے کیونکہ لائیونیس پراپرٹی کو ثابت کرنے کے لیے اس قسم کے تفصیلی اکاؤنٹنگ کی ضرورت نہیں ہے جو حفاظتی پراپرٹی کو ثابت کرنے کے لیے ضروری ہے۔ سیفٹی پراپرٹی سے مختلف ہونے کے لیے، لیوینس پراپرٹی کسی پھانسی کے کسی بھی محدود سابقہ کو مسترد نہیں کر سکتی (کیونکہ اس طرح کی ایک "بری چیز" ہوگی اور اس طرح، حفاظتی پراپرٹی کی وضاحت ہوگی)۔ اس سے لیوینس پراپرٹی کو ایک ایسی پراپرٹی کے طور پر بیان کیا جاتا ہے جو کسی بھی محدود سابقہ کو مسترد نہیں کرتا ہے۔ یہ تعریف کسی اچھی چیز کو مجرد ہونے تک محدود نہیں رکھتی-اچھی چیز میں یہ سب شامل ہو سکتے ہیں، جو کہ ایک لامحدود لمبائی کا عمل ہے۔ ہسٹری لیمپورٹ نے ملٹی پروسس (کنکرنٹ) پروگراموں کی درستگی کو ثابت کرنے پر اپنے 1977 کے مقالے میں سیفٹی پراپرٹی اور لیوینس پراپرٹی کی اصطلاحات استعمال کیں۔ انہوں نے پیٹری نیٹ تھیوری سے اصطلاحات ادھار لیں، جو یہ بیان کرنے کے لیے زندگی اور حد کی اصطلاحات استعمال کر رہی تھی کہ پیٹری نیٹ کے "ٹوکن" کو اس کے "مقامات" پر کیسے تفویض کیا جا سکتا ہے ؛ پیٹری نیٹ سیفٹی حد بندی کی ایک مخصوص شکل تھی۔ لامپورٹ نے بعد میں میونخ میں تقسیم شدہ نظاموں پر نیٹو کے مختصر کورس کے لیے حفاظت کی باضابطہ تعریف تیار کی۔ اس نے فرض کیا کہ ہچکچاہٹ کے تحت خصوصیات غیر متغیر ہیں۔ اوپر دی گئی حفاظت کی رسمی تعریف الپرن اور شنائڈر کے ایک مقالے میں ظاہر ہوتی ہے ؛ حفاظتی خصوصیات کی دو رسمی شکل کے درمیان تعلق الپرن، ڈیمرز اور شنائڈر کے ایک مقالے میں ظاہر ہوتا ہے۔ الپرن اور شنائڈر زندہ رہنے کی باضابطہ تعریف دیتے ہیں، اس ثبوت کے ساتھ کہ تمام خصوصیات کو حفاظتی خصوصیات اور زندہ رہنے کی خصوصیات کا استعمال کرتے ہوئے بنایا جا سکتا ہے۔ یہ ثبوت گورڈن پلاٹکن کی بصیرت سے متاثر تھا کہ حفاظتی خصوصیات بند سیٹوں سے مطابقت رکھتی ہیں اور زندہ خصوصیات پروگرام کی حالتوں کے لامحدود ترتیبات کے سیٹ پر قدرتی ٹوپولوجی میں گھنے سیٹوں سے مطابقت رکھتی ہیں۔ اس کے بعد، الپرن اور شنائڈر نے نہ صرف حفاظتی خصوصیات اور زندہ خصوصیات کی باضابطہ تعریفوں کے لیے بوچی آٹومیٹن کی خصوصیت دی بلکہ ان آٹومیٹا فارمولیشنز کو یہ ظاہر کرنے کے لیے استعمال کیا کہ حفاظتی خصوصیات کی تصدیق کے لیے ایک غیر متغیر کی ضرورت ہوگی اور زندہ خصوصیات کی تصدیق کے لیے ایک اچھی بنیاد کی دلیل کی ضرورت ہوگی۔ جائیداد کی قسم (حفاظت بمقابلہ زندگی) کے ساتھ ثبوت کی قسم (غیر متغیر بمقابلہ اچھی بنیاد) کے درمیان خط و کتابت ایک مضبوط دلیل تھی کہ جائیدادوں کو حفاظت اور زندگی میں سڑنا (کسی اور تقسیم کے برخلاف) ایک مفید تھا-جائیداد کی قسم کو جاننا ثابت ہونا ثبوت کی قسم کا تعین کرتا ہے جس کی ضرورت ہوتی ہے۔ حوالہ جات ہم آہنگی کمپیوٹنگ نظریاتی کمپیوٹر سائنس ماڈل کی جانچ