Mechanizing Asynchronous Distributed Algorithms in Rocq: The Echo Algorithm as a Case Study

आधुनिक दुनिया को शक्ति प्रदान करने वाले विशाल, अदृश्य नेटवर्क में, कंप्यूटर मिलकर समस्याओं को हल करने के लिए लगातार सूचनाओं का आदान-प्रदान करते हैं। ये प्रणालियाँ, जिन्हें वितरित एल्गोरिदम (distributed algorithms) के रूप में जाना जाता है, वैश्विक बैंकिंग लेनदेन से लेकर इंटरनेट ट्रैफ़िक के रूटिंग तक, सब कुछ संचालित करने वाले अदृश्य इंजन हैं। एक एकल कंप्यूटर के विपरीत जो निर्देशों के एक सख्त, रैखिक सेट का पालन करता है, एक वितरित प्रणाली स्वतंत्र मशीनों का एक संग्रह है जिन्हें बिना किसी केंद्रीय बॉस के समन्वय करना होता है। वे एक अतुल्यकालिक (asynchronous) वातावरण में काम करते हैं, जिसका अर्थ है कि उन्हें सिंक्रोनाइज़ करने के लिए कोई एकल घड़ी नहीं है; संदेश अप्रत्याशित गति से चलते हैं, और उनके आगमन का क्रम काफी भिन्न हो सकता है। इस वैश्विक समय सारणी के अभाव ने एक अनूठी चुनौती पैदा की है: हम कैसे सुनिश्चित कर सकते हैं कि एक प्रणाली सही ढंग से व्यवहार करेगी जब घटनाओं का समय अराजक और अप्रत्याशिक होता है? दशकों से, गणितज्ञों और कंप्यूटर वैज्ञानिकों ने औपचारिक सत्यापन (formal verification) पर भरोसा किया है, जो यह सिद्ध करने के लिए तर्क का उपयोग करने की एक कठोर विधि है कि एक प्रणाली विफल नहीं हो सकती, न कि केवल यह देखने के लिए परीक्षण करना कि यह अधिकांश समय कैसे काम करती है।

शोधकर्ताओं की एक टीम ने अब कंप्यूटर विज्ञान की एक क्लासिक समस्या, जिसे इको (Echo) एल्गोरिदम के रूप में जाना जाता है, पर इस कठोर तर्क को लागू किया है। यह एल्गोरिदम कंप्यूटरों के एक नेटवर्क के लिए एक संरचना पर सहमत होने का एक मौलिक तरीका है, जो अनिवार्य रूप से उनके कनेक्शनों का एक मानचित्र बनाता है ताकि एक केंद्रीय कंप्यूटर, जिसे इनीशिएटर (initiator) कहा जाता है, प्रत्येक अन्य नोड के साथ संवाद कर सके। इसकी प्रक्रिया अवधारणा में सरल है: इनीशिएटर अपने पड़ोसियों को एक संकेत, या एक "टोकन" भेजता है। वे पड़ोसी उस टोकन को अपने स्वयं के पड़ोसियों तक पहुँचाते हैं, और अंततः, संकेत पूरे नेटवर्क में लहरों की तरह फैलता है। एक बार जब कोई नोड टोकन प्राप्त कर लेता है और अपने सभी पड़ोसियों से प्रतिक्रिया सुन लेता है, तो वह मूल स्थान की ओर एक उत्तर, या "इको" भेजता है। इनीशिएटर तब तक प्रतीक्षा करता है जब तक कि उसे सभी से इको प्राप्त न हो जाए, और फिर कार्य पूरा होने की घोषणा करता है। हालांकि विचार सीधा लगता है, लेकिन संदेशों के विलंब और पुनर्व्यवस्था के हर संभावित परिदृश्य के तहत इस प्रक्रिया के सही ढंग से काम करने को सिद्ध करना अत्यंत कठिन है। शोधकर्ताओं ने, 'रॉक' (Rocq) नामक एक विशेषीकृत प्रूफ़ असिस्टेंट के साथ मिलकर, सफलतापूर्वक एक औपचारिक प्रमाण का निर्माण किया है जो एल्गोरिदम की विश्वसनीयता को प्रदर्शित करता है, विशेष रूप से यह दिखाते हुए कि यदि इनीशिएटर निर्णय लेता है कि कार्य समाप्त हो गया है, तो नेटवर्क वास्तव में पूरी तरह से खोजा जा चुका है।

इस कार्य का मूल इस एल्गोरिदम का एक डिजिटल जुड़वां (digital twin) बनाने में निहित है जो इतना सटीक हो कि इसमें अस्पष्टता की कोई गुंजाइश न रहे। शोधकर्ताओं ने पूरे नेटवर्क को एक एकल, विकसित होती अवस्था (state) के रूप में मॉडल किया। इस अवस्था में प्रत्येक व्यक्तिगत कंप्यूटर की वर्तमान स्थिति और उनके बीच यात्रा कर रहे सभी संदेशों का एक संग्रह शामिल है। इस मॉडल में, संदेशों की गति किसी घड़ी द्वारा नहीं, बल्कि नियमों के एक समूह द्वारा नियंत्रित होती है जो किसी भी संदेश को किसी भी समय वितरित करने की अनुमति देती है, जो अतुल्यकालिक नेटवर्क की अराजक वास्तविकता को दर्शाता है। शोधकर्ताओं ने फिर तार्किक नियमों, या इनवेरिएंट्स (invariants) का एक सेट परिभाषित किया, जो संदेशों के हेरफेर के बावजूद हमेशा सत्य रहने चाहिए। ये नियम गार्डरेल के रूप में कार्य करते हैं, यह सुनिश्चित करते हुए कि सिस्टम कभी ऐसी अवस्था में न जाए जहाँ एक कंप्यूटर यह सोच ले कि उसने काम पूरा कर लिया है जबकि नेटवर्क का कोई हिस्सा अभी भी प्रतीक्षा कर रहा हो।

इस अध्ययन का सबसे महत्वपूर्ण निष्कर्ष निर्णय के क्षण के संबंध में एक सशर्त प्रमाण है। शोधकर्ताओं ने सिद्ध किया कि यदि इनीशिएटर कंप्यूटर कभी ऐसी अवस्था में पहुँचता है जहाँ वह मानता है कि कार्य पूर्ण हो गया है, तो नेटवर्क के प्रत्येक अन्य कंप्यूटर के पास उस इनीशिएटर तक वापस जाने के लिए कनेक्शनों का एक स्पष्ट, परिमित पथ होना चाहिए। दूसरे शब्दों में, नेटवर्क ने सफलतापूर्वक इनीशिएटर में निहित एक पेड़ जैसी संरचना (tree-like structure) बना ली है, जिसमें कोई लूप या अलग-थलग द्वीप नहीं हैं। यह प्रमाण उल्लेखनीय है क्योंकि यह संदेशों के आगमन के क्रम की परवाह किए बिना सत्य रहता है। यह उन जटिल, उलझे हुए परिदृश्यों को भी ध्यान में रखता है जहाँ संदेश एक ही कनेक्शन पर एक-दूसरे को काट सकते हैं, या जहाँ एक कंप्यूटर कार्य शुरू करने से पहले ही दूसरा संकेत प्राप्त कर सकता है। शोधकर्ताओं ने दिखाया कि भले ही ऐसी उलझी हुई स्थितियाँ हों, एल्गोरिदम का तर्क इनीशिएटर को समय से पहले निर्णय लेने से रोकता है। यदि नेटवर्क में एक भी संदेश तैर रहा है जो उस कंप्यूटर के लिए है जिसने अभी तक काम शुरू नहीं किया है, तो इनीशिएटर के आंतरिक काउंटर उसे विजय घोषित करने से रोक देंगे।

इसे प्राप्त करने के लिए, टीम को समस्या को तर्क के विभिन्न स्तरों में विभाजित करना पड़ा। उन्होंने पहले संरचनात्मक तथ्यों को स्थापित किया, यह सुनिश्चित करते हुए कि प्रत्येक कनेक्शन जो एक कंप्यूटर बनाता है वह वैध है और कोई भी कंप्यूटर स्वयं की ओर संकेत नहीं करता है। उन्होंने फिर एक कारण संबंधी परत (causal layer) को सिद्ध किया, यह दिखाते हुए कि यदि किसी कंप्यूटर ने संकेत भेजा है, तो उसका एक पैरेंट (parent) कंप्यूटर होना चाहिए जिसने पहले उसे संकेत भेजा था, जिससे शुरुआत तक एक श्रृंखला बनती है। अंत में, उन्होंने एक लेखांकन परत (accounting layer) पर काम किया, जो भेजे गए और प्राप्त किए गए संदेशों की संख्या को ट्रैक करती है। यह लेखांकन ही इस प्रमाण की कुंजी है: यह एक एकल कंप्यूटर की स्थानीय स्थिति को पूरे नेटवर्क की वैश्विक स्थिति से जोड़ता है। शोधकर्ताओं ने प्रदर्शित किया कि एक कंप्यूटर अपना काम तब तक पूरा नहीं कर सकता जब तक कि उसे अपने सभी पड़ोसियों से उत्तर प्राप्त न हो जाए, और यह आवश्यकता कनेक्शनों की पूरी श्रृंखला के माध्यम से इनीशिएटर तक पहुँचती है। यदि एक भी कंप्यूटर संदेश की प्रतीक्षा कर रहा है, तो इनीशिएटर का काउंटर उसे दर्शाएगा, जिससे अंतिम निर्णय लेने से रोका जा सकेगा।

यह कार्य किसी विशिष्ट नेटवर्क आकार पर सिमुलेशन या परीक्षण नहीं है; यह एक गणितीय प्रमाण है जो विशिष्ट परिकल्पनाओं को संतुष्ट करने वाले किसी भी परिमित सूचीबद्ध ग्राफ (finite listed graph) पर लागू होता है। शोधकर्ताओं ने अपने तर्क के प्रत्येक चरण की जाँच करने के लिए 'रॉक' (Rocq) नामक एक उपकरण का उपयोग किया, जो एक औपचारिक प्रूफ़ असिस्टेंट है। परिणामी कोड, जिसमें एक सौ चालीस से अधिक अलग-अलग तार्किक घोषणाएँ शामिल हैं, को कंप्यूटर द्वारा स्वयं त्रुटिहीन प्रमाणित किया गया है। इसका अर्थ यह है कि प्रमाण केवल एक मानवीय तर्क नहीं है जिसमें कोई छिपा हुआ दोष हो सकता है, बल्कि एक मशीन-जाँचा गया गारंटी है। शोधकर्ताओं ने यह सिद्ध नहीं किया कि एल्गोरिदम हमेशा अंततः समाप्त हो जाएगा, क्योंकि इसके लिए यह मानना आवश्यक होगा कि संदेश अंततः वितरित किए जाएंगे, एक ऐसी शर्त जिसे उन्होंने प्रमाण को सुरक्षा पर केंद्रित रखने के लिए जानबूझकर बाहर रखा है। इसके बजाय, उन्होंने सिद्ध किया कि यदि एल्गोरिदम समाप्त होता है, तो वह सही ढंग से समाप्त होता है।

यह उपलब्धि इस बात को रेखांकित करती है कि हम जटिल प्रणालियों को कैसे सत्यापित कर सकते हैं। समस्या को पुन: प्रयोज्य घटकों में तोड़कर, शोधकर्ताओं ने एक ऐसी विधि बनाई है जिसे भविष्य में अन्य वितरित एल्गोरिदम पर लागू किया जा सकता है, हालाँकि वर्तमान आर्टिफैक्ट किसी भी मनमाने एल्गोरिदम के लिए एक प्लग-इन सत्यापन ढांचा नहीं है और इसके लिए अन्य मामलों के लिए पुनर्गठन की आवश्यकता होगी। जबकि वर्तमान कार्य विशेष रूप से इको एल्गोरिदम पर केंद्रित है, संरचनात्मक नियमों को लेखांकन तर्क से अलग करने की पद्धति अन्य समस्याओं को हल करने के लिए एक ब्लूप्रिंट प्रदान करती है जहाँ समय अनिश्चित होता है। प्रमाण पुष्टि करता है कि अप्रत्याशित देरी वाली दुनिया में भी, ऐसी प्रणालियाँ बनाना गणितीय रूप से संभव है जो इच्छित रूप से व्यवहार करने के लिए निश्चित हैं। शोधकर्ताओं ने अपने कोड और प्रमाणों को दूसरों के निरीक्षण और निर्माण के लिए उपलब्ध कराया है, जो आधुनिक समाज को शक्ति प्रदान करने वाले डिजिटल नेटवर्कों की विश्वसनीयता सुनिश्चित करने के भविष्य के कार्यों के लिए एक ठोस आधार प्रदान करता है।