💻 computer science

Reasoning about concurrent loops and recursion with rely-guarantee rules

यह शोध पत्र रिलाय-गारंटी (rely-guarantee) दृष्टिकोण का उपयोग करते हुए, परमाणु अभिव्यक्ति मूल्यांकन (atomic expression evaluation) को माने बिना, समवर्ती प्रणालियों (concurrent systems) में रिकर्सिव प्रोग्रामों और 'while' लूप्स के बारे में तर्क करने के लिए यांत्रिक रूप से सत्यापित, सामान्य परिशोधन नियमों (refinement rules) को प्रस्तुत करता है।

मूल लेखक: Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones

प्रकाशित 2026-06-12

📖 7 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Ian J. Hayes, Larissa A. Meinicke, Cliff B. Jones

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक टीम के शेफ के लिए एक रेसिपी लिखने की कोशिश कर रहे हैं जो एक अराजक, साझा रसोई (shared kitchen) में काम कर रहे हैं। हर कोई एक ही समय में काट रहा है, चला रहा है और चख रहा है। समस्या यह है कि जबकि शेफ A रेसिपी का एक चरण पढ़ रहा है, शेफ B चुपके से एक सामग्री को हिला सकता है, तापमान बदल सकता है, या एक उपकरण छिपा सकता है। यह कन्करेंट प्रोग्रामिंग (concurrent programming) की दुनिया है: कई प्रोग्राम एक ही समय में चल रहे हैं, जो एक-दूसरे के डेटा के साथ छेड़छाड़ कर रहे हैं।

हेज़, मीनिक और जोन्स का यह शोध पत्र इन रेसिपीज़ को लिखने के लिए एक नया, अत्यंत सख्त नियम पुस्तिका (rulebook) की तरह है ताकि यह गारंटी दी जा सके कि वे अराजकता के बीच भी काम करेंगी। वे दो विशिष्ट प्रकार के खाना पकाने के निर्देशों पर ध्यान केंद्रित करते हैं: लूप्स (loops) (किसी चीज़ को बार-बार करना) और रिकर्सन (recursion) (एक ऐसी रेसिपी जो समस्या के छोटे हिस्से को हल करने के लिए खुद को ही कॉल करती है)।

यहाँ उनके "रसोई के नियमों" का सरल उपमाओं (analogies) का उपयोग करके विवरण दिया गया है:

1. "रिलाय-गारंटी" (Rely-Guarantee) अनुबंध

एक सामान्य रसोई में, आप शायद सिर्फ इस भरोसे पर काम करेंगे कि कोई आपके बर्तन को नहीं छुएगा। इस पेपर में, लेखक कहते हैं: "भरोसा काफी नहीं है। हमें एक अनुबंध (contract) चाहिए।"

रिलाय कंडीशन (The "Don't Touch" List - "मत छुओ" सूची): अपना कार्य शुरू करने से पहले, आप यह मान लेते हैं कि अन्य शेफ कुछ नियमों का पालन करेंगे। उदाहरण के लिए, "मैं इस बात पर निर्भर (rely) करता हूँ कि जब मैं सूप चख रहा हूँ, तो कोई उसमें नमक नहीं डालेगा।"
गारंटी कंडीशन (The "I Promise" List - "मैं वादा करता हूँ" सूची): बदले में, आप वादा करते हैं कि आप भी नियमों का पालन करेंगे। "मैं गारंटी देता हूँ कि मैं अपना चम्मच दीवार पर नहीं मारूँगा।"
जादू: यदि हर कोई अपने "रिलाय" और "गारंटी" अनुबंधों का पालन करता है, तो पूरा रसोई सुचारू रूप से चलता है, भले ही वे सभी एक साथ काम कर रहे हों।

2. "एटॉमिक" (Atomic) धारणाओं के साथ समस्या

कई पुराने नियम पुस्तिकाओं ने माना था कि जब एक शेफ रेसिपी का एक चरण पढ़ता है, तो वह इसे तुरंत करता है, जैसे उंगलियों का एक जादुई चुटकी बजाना। उन्होंने माना कि शेफ पढ़ता है "2 अंडे डालें" और किसी के पलक झपकने से पहले ही वे अंडे डाल देता है।

लेखक कहते हैं: "नहीं, वास्तविक रसोई में ऐसा नहीं होता है।"
वास्तविकता में, "2 अंडे डालें" पढ़ने में समय लगता है। जब तक शेफ अंडों के लिए हाथ बढ़ा रहा होता है, तब तक दूसरा शेफ कार्टन को हटा सकता है। यह पेपर इस अव्यवस्थपूर्ण वास्तविकता को ध्यान में रखते हुए नियम बनाता है। वे यह नहीं मानते कि सब कुछ तुरंत होता है; वे मानते हैं कि हर चीज़ में थोड़ा समय लगता है और उसमें बाधा डाली जा सकती है।

3. "व्हाइल" लूप (The Never-Ending Stir - कभी न खत्म होने वाला चलाना) को वश में करना

एक "व्हाइल लूप" (while loop) एक ऐसे शेफ की तरह है जो सॉस को "गाढ़ा होने तक" चला रहा है।

पुरानी समस्या: एक साझा रसोई में, एक शेफ सॉस चला सकता है, उसे चेक कर सकता है, और तय कर सकता है कि यह अभी गाढ़ा नहीं हुआ है। लेकिन जब वह चूल्हे की ओर जा रहा होता है, तो दूसरा शेफ उसमें पानी डाल सकता है, जिससे वह फिर से पतला हो जाता है। पहला शेफ इसे अनंत काल तक चलाता रह सकता है, या तब रुक सकता है जब उसे रुक जाना चाहिए था।
नया नियम (अर्ली टर्मिनेशन - Early Termination): लेखक एक चतुर तकनीक पेश करते हैं जिसे "अर्ली टर्मिनेशन" कहा जाता है।
- कल्पना करें कि शेफ के पास एक टाइमर (एक "वेरिएंट") है। हर बार जब वह चलाता है, तो टाइमर कम होता जाता है।
- आमतौर पर, शेफ को टाइमर कम करने के लिए चलाना पड़ता है।
- ट्विस्ट: यदि दूसरा शेफ गलती से पानी डाल देता है (हस्तक्षेप/interference), तो टाइमर उम्मीद से तेजी से कम हो सकता है, या सॉस अचानक इतना गाढ़ा हो सकता है कि लूप को रुक जाना चाहिए।
- नया नियम लूप को जल्दी समाप्त करने की अनुमति देता है यदि वातावरण (अन्य शेफ) काम को पूरा करने में मदद करता है, बजाय इसके कि लूप खुद सारा काम करने के लिए मजबूर हो। यह यह कहने जैसा है कि, "यदि किसी और की मदद से सॉस पहले ही गाढ़ा हो गया है, तो आप तुरंत चलाना बंद कर सकते हैं।"

4. रिकर्सन (Recursion) को वश में करना (वह रेसिपी जो खुद को कॉल करती है)

रिकर्सन एक ऐसे शेफ की तरह है जो कहता है, "इस बड़े स्टू को बनाने के लिए, मुझे पहले ब्रॉथ (broth) का एक छोटा बैच बनाना होगा। उस ब्रॉथ को बनाने के लिए, मुझे स्टॉक का एक बहुत छोटा हिस्सा बनाना होगा..."

चुनौती: एक साझा रसोई में, यदि शेफ A ब्रॉथ बना रहा है, तो शेफ B स्टॉक का बर्तन चुरा सकता है।
समाधान: लेखकों ने एक गणितीय "सीढ़ी" (well-founded relation) बनाई है। कल्पना करें कि शेफ छोटी और छोटी समस्याओं को हल करने के लिए एक सीढ़ी से नीचे उतर रहा है।
- नियम: आप केवल तभी सीढ़ी से नीचे उतर सकते हैं जब आप सुनिश्चित हों कि आप फंसेंगे नहीं।
- "अर्ली एग्जिट" (Early Exit) ट्रिक: लूप के साथ ही, यदि अन्य शेफ आपको सीढ़ी के नीचे जल्दी पहुँचने में मदद करते हैं (किसी उप-समस्या को आपके लिए हल करके), तो आपको सीढ़ी से जल्दी उतरने की अनुमति है। आपको हर एक कदम खुद करने की ज़रूरत नहीं है यदि वातावरण आपको काम पूरा करने में मदद करता है।

5. "एज़ल ट्रेस" (The Aczel Trace - रसोई का सुरक्षा कैमरा)

यह साबित करने के लिए कि उनके नियम काम करते हैं, लेखक एक अवधारणा का उपयोग करते हैं जिसे "एज़ल ट्रेस" (Aczel trace) कहा जाता है।

कल्पना करें कि एक सुरक्षा कैमरा रसोई की रिकॉर्डिंग कर रहा है।
कैमरा दो प्रकार की गतिविधियों को रिकॉर्ड करता है: प्रोग्राम मूव्स (जो शेफ आप देख रहे हैं वह करता है) और एनवायरनमेंट मूव्स (जो अन्य शेफ करते हैं)।
लेखकों के नियम यह सुनिश्चित करते हैं कि चाहे कैमरा अराजकता को कैसे भी रिकॉर्ड करे, यदि "रिलाय" और "गारंटी" अनुबंधों को रखा जाता है, तो अंतिम व्यंजन एकदम सही होगा।

सारांश

यह शोध पत्र उन निर्देशों को लिखने का एक नया, मजबूत तरीका प्रदान करता है जो एक ही समय में चलने वाले कंप्यूटर प्रोग्रामों के लिए हैं।

कोई जादू नहीं: यह यह मानने से रोकता है कि चीजें तुरंत होती हैं।
अनुबंध: यह प्रोग्रामों के बीच बातचीत को प्रबंधित करने के लिए "रिलाय" और "गारंटी" का उपयोग करता है।
लचीलापन: यह लूप और रिकर्सिव फंक्शन को जल्दी समाप्त करने की अनुमति देता है यदि वातावरण उन्हें पूरा करने में मदद करता है, जिससे उन्हें अनंत लूप में फंसने या हस्तक्षेप के कारण विफल होने से रोका जा सके।

लेखकों ने इन नियमों का परीक्षण एक कंप्यूटर प्रूफ असिस्टेंट (Isabelle/HOL) का उपयोग करके पहले ही किया है, जो एक अत्यंत सख्त गणित शिक्षक की तरह काम करता है, जो यह सुनिश्चित करने के लिए हर एक चरण की जांच करता है कि तर्क त्रुटिहीन है। उन्होंने केवल अनुमान नहीं लगाया; उन्होंने इसे सिद्ध किया है कि यह काम करता है।

तकनीकी सारांश: रिलाय-गारंटी नियमों के साथ समवर्ती लूप और पुनरावृत्ति (Recursion) के बारे में तर्क देना

समस्या विवरण

समवर्ती कार्यक्रमों (concurrent programs) का सत्यापन, विशेष रूप से जिनमें पुनरावृत्ति संरचनाएं (recursive structures) और while लूप शामिल हैं, समानांतर थ्रेडों से होने वाले हस्तक्षेप (interference) के कारण महत्वपूर्ण चुनौतियों का सामना करता है। लूप के लिए पारंपरिक होअर-शैली (Hoare-style) के सत्यापन नियम इनवेरियंट्स (invariants) और वेरिएंट अभिव्यक्तियों (variant expressions) पर निर्भर करते हैं ताकि शुद्धता और समाप्ति (termination) को सिद्ध किया जा सके। हालाँकि, एक समवर्ती परिवेश में, हस्तक्षेप इनवेरियंट्स को अमान्य कर सकता है, वेरिएंट अभिव्यक्तियों को बढ़ा सकता है, या लूप गार्ड के मूल्यांकन को बाधित कर सकता है, जिससे मानक अनुक्रमिक नियम अमान्य हो जाते हैं।

इसके अलावा, कई मौजूदा रिलाय-गारंटी (Rely-Guarantee - RG) दृष्टिकोण यह मान लेते हैं कि अभिव्यक्ति मूल्यांकन (expression evaluation) परमाणु (atomic) है। यह धारणा प्रोग्रामिंग भाषा के कार्यान्वयन की वास्तविकता को प्रतिबिंबित नहीं करती है, जहाँ अभिव्यक्तियों में साझा चरों (shared variables) तक कई पहुँच शामिल हो सकती हैं जो पर्यावरण संक्रमणों (environment transitions) के साथ इंटरलीव (interleaved) हो सकती हैं। यह परमाणुता की धारणा जटिल अभिव्यक्तियों के लिए औपचारिक तर्क की श्रृंखला को तोड़ देती है और सत्यापन नियमों की प्रयोज्यता को सीमित करती है।

कार्यप्रणाली (Methodology)

लेखक एक विस्तृत-स्पेक्ट्रम भाषा (wide-spectrum language) का उपयोग करते हुए, जो कमांड्स के पूर्ण वितरक जालक (complete distributive lattice) पर आधारित है, रिलाय-गारंटी संदर्भ के भीतर पुनरावर्ती कार्यक्रमों और while लूप के बारे में तर्क देने के लिए एक ढांचा विकसित करते हैं। यह कार्यप्रणाली निम्नलिखित प्रमुख घटकों पर आधारित है:

एज़ेल ट्रेस सिमेंटिक्स (Aczel Trace Semantics): सिमेंटिक मॉडल एज़ेल ट्रेसेस (Aczel traces) के सेट का उपयोग करता है, जो प्रोग्राम ( $\pi$ ) और पर्यावरण ( $\epsilon$ ) संक्रमणों के अनुक्रमों को रिकॉर्ड करते हैं। यह अभिव्यक्ति मूल्यांकन या असाइनमेंट कमांड की परमाणुता का अनुमान लगाए बिना हस्तक्षेप के कम्पोजिशनल उपचार की अनुमति देता है।
रिलाय-गारंटी स्थितियाँ (Rely-Guarantee Conditions): ढांचा पर्यावरण के व्यवहार को नियंत्रित करने के लिए रिलाय स्थितियों ( $r$ ) और प्रोग्राम के व्यवहार को नियंत्रित करने के लिए गारंटी स्थितियों ( $g$ ) का उपयोग करता है। एक थ्रेड की गारंटी सभी समानांतर थ्रेडों की रिलाय स्थिति को लागू करनी चाहिए।
फिक्स्ड-पॉइंट थ्योरी (Fixed-Point Theory): पुनरावर्ती कार्यक्रमों को कमांड्स के जालक पर फिक्स्ड-पॉइंट के रूप में परिभाषित किया गया है। लेखक इन फिक्स्ड-पॉइंट्स के बारे में तर्क देने के लिए नियम विकसित करते हैं, विशेष रूप से समाप्ति को सिद्ध करने के लिए वेरिएंट अभिव्यक्तियों और संबंधों के साथ वेल-फाउंडेड इंडक्शन (well-founded induction) का उपयोग करते हैं।
प्रारंभिक समाप्ति (Early Termination): एक केंद्रीय कार्यप्रणाली नवाचार पुनरावृत्ति और लूप दोनों के लिए "प्रारंभिक समाप्ति" संस्करणों का विकास है। मानक दृष्टिकोणों के विपरीत, जिन्हें यह आवश्यक होता है कि फंक्शन बॉडी द्वारा किसी भी पुनरावर्ती कॉल से पहले वेरिएंट को सख्ती से कम किया जाए, ये नियम फंक्शन बॉडी को या तो वेरिएंट को कम करने या एक ऐसी स्थिति (बेस केस) स्थापित करने की अनुमति देते हैं जो यह सुनिश्चित करती है कि आगे कोई पुनरावर्ती कॉल न की जाए। यह समवर्तीता के लिए महत्वपूर्ण है, जहाँ हस्तक्षेप वेरिएंट को इस तरह कम कर सकता है जो फंक्शन बॉडी द्वारा इसे कम करने को रोक दे, फिर भी समाप्ति सुनिश्चित करता है।
गैर-परमाणु अभिव्यक्ति मूल्यांकन (Non-Atomic Expression Evaluation): दृष्टिकोण स्पष्ट रूप से अभिव्यक्तियों के गैर-परमाणु मूल्यांकन को संभालता है। यह जटिल अभिव्यक्तियों के लिए सब-एक्सप्रेशन (sub-expressions) का विश्लेषण करके पोस्टकंडीशन स्थापित करने के लिए एक कम्पोजिशनल विधि का उपयोग करता है, जिससे "सिंगल क्रिटिकल रेफरेंस" जैसे सिंटैक्टिक प्रतिबंधों की आवश्यकता समाप्त हो जाती है जो परमाणु-धारणा सिद्धांतों में पाए जाते हैं।

मुख्य योगदान

यह शोध पत्र समवर्ती प्रोग्राम सत्यापन के सिद्धांत में कई विशिष्ट योगदान प्रस्तुत करता है:

पुनरावृत्ति के लिए सामान्य रिफाइनमेंट नियम: प्रमेय 5 ("recursion-early") एक पुनरावृत्ति पेश करने के लिए एक नियम प्रदान करता है जो हस्तक्षेप को समायोजित करता है। यह एक वेल-फाउंडेड संबंध और एक वेरिएंट अभिव्यक्ति का उपयोग करता है, जिससे समाप्ति को तब भी सिद्ध किया जा सकता है जब वेरिएंट फंक्शन बॉडी के बजाय पर्यावरण द्वारा कम किया जाता है, बशर्ते कि एक बेस केस स्थापित किया गया हो।
While लूप के लिए सामान्य रिफाइनमेंट नियम: प्रमेय 6 ("intro-while") पुनरावृत्ति नियम के आधार पर while लूप पेश करने के लिए एक नियम व्युत्पन्न करता है। इसमें एक "प्रारंभिक समाप्ति" स्थिति ( $p_X$ ) शामिल है जो लूप को बाहर निकलने की अनुमति देती है यदि हस्तक्षेप के कारण गार्ड (guard) गलत (false) हो जाता है, भले ही लूप बॉडी ने वेरिएंट को सख्ती से कम न किया हो।
गैर-परमाणु अभिव्यक्तियों को संभालना: ढांचा ऐसे अनुमान नियम (जैसे, कंडीशनल के लिए प्रमेय 2, फंक्शन कॉल्स के लिए प्रमेय 3) प्रदान करता है जो परमाणु मूल्यांकन का अनुमान लगाए बिना हस्तक्षेप के तहत अभिव्यक्तियों और गार्ड्स के बारे में कम्पोजिशनल तर्क की अनुमति देते हैं।
औपचारिक सत्यापन (Formal Verification): पेपर के सभी लेम्मा और प्रमेय आइसोबेल/एचओएल (Isabelle/HOL) थ्योरम प्रूवर का उपयोग करके यांत्रिक रूप से सत्यापित किए गए हैं।
फेयर टर्मिनेशन (Fair Termination): पेपर फेयर टर्मिनेशन को संबोधित करता है, एक fair कमांड को परिभाषित करता है जो पर्यावरण संक्रमणों के अनंत निरंतर अनुक्रमों को रोकता है, और यह दिखाने के लिए कि एक कमांड फेयर निष्पादन के तहत केवल सीमित संख्या में संक्रमण करता है।

परिणाम और उदाहरण

पेपर विकसित कानूनों की उपयोगिता को दो प्राथमिक उदाहरणों के माध्यम से प्रदर्शित करता है:

पैरलल रिकर्सिव सर्च (Parallel Recursive Search): एक रेंज $[0, N)$ में एक मान $i$ खोजने के लिए एक पुनरावर्ती खोज एल्गोरिदम विकसित किया गया है जो प्रेडिकेट $P$ को संतुष्ट करता है। कार्यान्वयन समानांतर पुनरावर्ती कॉल्स के साथ डिवाइड-एंड-कॉन्कर रणनीति का उपयोग करता है। प्रमाण "recursion-early" कानून का उपयोग करता है ताकि उस मामले को संभाला जा सके जहाँ एक समवर्ती थ्रेड ने पहले ही समाधान (एक found फ्लैग सेट करना) पा लिया है, जिससे पुनरावर्ती कॉल्स को आगे की प्रोसेसिंग के बिना जल्दी समाप्त करने की अनुमति मिलती है।
CAS के साथ एटोमिक अपडेट (Atomic Update with CAS): एक वेरिएबल $m$ को $\min(m, lo)$ में अपडेट करने के लिए कंपेयर-एंड-स्वैप (CAS) निर्देश का उपयोग करके एक एटोमिक स्पेसिफिकेशन को लागू करने का उदाहरण। लूप बार-बार CAS का प्रयास करता है। "प्रारंभिक समाप्ति" वाला लूप कानून यहाँ आवश्यक है: यदि गार्ड चेक और CAS निष्पादन के बीच $m$ को $lo$ से कम करने के लिए हस्तक्षेप होता है, तो CAS $m$ (वेरिएंट) को कम करने में विफल हो सकता है। हालाँकि, लूप समाप्त हो जाता है क्योंकि गार्ड ($lo < m$) गलत (false) हो जाता है। मानक लूप कानून इस परिदृश्य में समाप्ति सिद्ध करने में विफल रहेगा, लेकिन प्रस्तावित कानून सफल होता है क्योंकि यह प्रारंभिक निकास स्थिति को पहचान लेता है।

महत्व और दावे

लेखक दावा करते हैं कि उनका कार्य समवर्तीता की उपस्थिति में पुनरावृत्ति और लूप के बारे में तर्क देने के लिए सामान्य, यांत्रिक रूप से सत्यापित रिफाइनमेंट नियम प्रदान करता है। इस कार्य का महत्व निम्नलिखित में निहित है:

परमाणुता धारणाओं को हटाना: अभिव्यक्ति मूल्यांकन को परमाणु न मानकर, नियम अधिक यथार्थवादी प्रोग्रामिंग परिदृश्यों के लिए लागू होते हैं और उन सिद्धांतों के तर्क को टूटने से बचाते हैं जो परमाणुता पर निर्भर करते हैं।
समाप्ति प्रमाणों में हस्तक्षेप को संभालना: "प्रारंभिक समाप्ति" कानून समवर्ती सत्यापन में एक विशिष्ट अंतराल को संबोधित करते हैं जहाँ हस्तक्षेप मानक समाप्ति तर्कों को अमान्य कर सकता है। यह उन कार्यक्रमों के सत्यापन की अनुमति देता है जहाँ पर्यावरण की क्रियाएँ समाप्ति की स्थिति में योगदान करती हैं।
कम्पोजिशनल डेवलपमेंट: दृष्टिकोण साझा-चर (shared-variable) समवर्ती कार्यक्रमों के कम्पोजिशनल विकास का समर्थन करता है, जिससे थ्रेड्स को उनके रिलाय और गारंटी शर्तों के आधार पर स्वतंत्र रूप से डिजाइन और सत्यापित किया जा सकता है।
औपचारिक कठोरता (Formal Rigor): परिणाम केवल सैद्धांतिक प्रस्ताव नहीं हैं बल्कि उन्हें आइसोबेल/एचओएल थ्योरम प्रूवर के भीतर औपचारिक रूप से सत्यापित किया गया है, जो उनकी तार्किक शुद्धता सुनिश्चित करते हैं।

पेपर पिछले बीजगणितीय रिलाय-गारंटी अनुसंधान के विस्तार के रूप में खुद को स्थापित करता है, जो विशेष रूप से समवर्ती प्रणालियों में पुनरावृत्ति, लूप और गैर-परमाणु अभिव्यक्ति मूल्यांकन द्वारा पेश की गई जटिलताओं को लक्षित करता है। यह दावा नहीं करता है कि यह कंकरेंट सेपरेशन लॉजिक (CSL) जैसे अन्य लॉजिक को बदल देगा, बल्कि एक वैकल्पिक कम्पोजिशनल विधि प्रदान करता है, विशेष रूप से यह नोट करते हुए कि जबकि CSL रेस-फ्रीडम (race freedom) के बारे में तर्क करने का समर्थन करता है, RG "रेसी" (racy) प्रोग्रामों (ऐसे प्रोग्राम जहाँ रेस को रिलाय/गारंटी स्थितियों के माध्यम से प्रबंधित किया जाता है) के विकास के लिए डिज़ाइन किया गया है।