TLA+ - प्रोग्राम और concurrent/distributed systems को मॉडल करने के लिए एक उन्नत भाषा

• TLA+ को software को मॉडल करने के लिए code level के बजाय higher level पर, और hardware को मॉडल करने के लिए circuit level के बजाय higher level पर इस्तेमाल किया जाता है
• यह model लिखने और उन्हें जांचने के लिए integrated development environment (IDE) प्रदान करता है
• इंजीनियरों द्वारा सबसे अधिक इस्तेमाल किया जाने वाला tool TLC model checker है, और proof checker भी उपलब्ध है
• TLA+ गणित पर आधारित है और किसी भी programming language जैसा नहीं है
• अधिकांश engineers के लिए TLA+ की तुलना में PlusCal से शुरुआत करना आसान होता है
• TLA+ model को आमतौर पर "specification" कहा जाता है। नीचे के परिचय में इसे model कहा गया है

PlusCal

• PlusCal algorithm लिखने की भाषा है, खासकर parallel और distributed algorithm लिखने के लिए
• इसका उपयोग pseudocode की जगह testable और precise code में algorithm लिखने के लिए किया जाता है
• यह एक simple programming language जैसा दिखता है, और concurrency तथा nondeterminism को व्यक्त करने वाली संरचनाएँ देता है
• इसमें mathematical formulas को expressions के रूप में इस्तेमाल किया जा सकता है, इसलिए यह बहुत expressive है
• PlusCal algorithm को TLA+ model में बदला जाता है, और TLA+ tools से verify किया जा सकता है
• यह programming language जैसा दिखता है इसलिए सीखना आसान है, लेकिन complex model structuring के लिए TLA+ अधिक उपयुक्त है

मॉडल क्या है

• कंप्यूटर और network निरंतर भौतिक नियमों का पालन करते हैं, लेकिन इनके व्यवहार को discrete events के समूह के रूप में मॉडल करना स्वाभाविक है
• ऐसा कोई model नहीं है जो वास्तविक system का पूरी तरह वर्णन कर सके; model किसी खास उद्देश्य के लिए system के कुछ पहलुओं का वर्णन करता है
• TLA+ एक state-based modeling language है, जो system के execution को states के क्रम के रूप में व्यक्त करती है
• event को लगातार आने वाले दो states की जोड़ी के रूप में व्यक्त किया जाता है, जिसे 'step' कहा जाता है
• system को उन actions के समूह के रूप में मॉडल किया जाता है जो सभी संभव executions का वर्णन करते हैं

code level से ऊपर की modeling

• TLA+ का उपयोग code level से ऊपर system modeling के लिए किया जाता है
• उदाहरण के लिए, Euclidean algorithm को code के रूप में नहीं बल्कि एक procedure के रूप में GCD निकालने के तरीके से समझाया जा सकता है
  • variable x को M, y को N पर set करें
  • x और y में से छोटे मान को बड़े मान से बार-बार घटाएँ
  • x और y के बराबर होने तक दोहराएँ, और वही मान GCD है
• इस तरह का वर्णन variable types या exception handling जैसी details को छोड़ देता है, और केवल algorithm की essential concept को व्यक्त करता है
• अगर केवल coding पर ध्यान दिया जाए तो अच्छा algorithm ढूँढना कठिन होता है → abstract thinking की जरूरत होती है
• अधिकांश programmers high-level model के बिना coding शुरू कर देते हैं, और इससे design errors पैदा होते हैं
• TLA+ एक high-level modeling language है जो code के behavior और उसके तरीके को स्पष्ट रूप से वर्णित कर सकती है
• system जितना जटिल होता है, simplification उतनी महत्वपूर्ण होती है, और यह code लिखने की technique से नहीं बल्कि higher-order thinking से हासिल होती है
• एक industrial project में TLA+ modeling से real-time operating system के code size को दसवें हिस्से तक घटाया गया था
• modeling design errors को पहले से ढूँढने में प्रभावी है, और testing या code fixes की तुलना में अधिक विश्वसनीय है

parallel systems की modeling

• parallel system कई components (processes) से बना होता है जो एक साथ काम करते हैं
• distributed system में स्थानिक रूप से अलग-अलग processes messages के जरिए communicate करते हैं
• TLA+ पूरे system state को global state के रूप में मॉडल करता है
• 40 से अधिक वर्षों के अनुभव के अनुसार, distributed systems को global state के आधार पर मॉडल करना सबसे अधिक सामान्य रूप से उपयोगी है

state machine

• TLA+ निम्न दो तत्वों से actions के समूह को परिभाषित करता है:
  • initial condition: संभावित शुरुआती state को निर्दिष्ट करती है
  • next-state relation: संभावित steps (लगातार आने वाले state pairs) को निर्दिष्ट करती है
• इन दो शर्तों को पूरा करने वाले actions का समूह ही model है
• ऐसे model को state machine कहा जाता है
• finite-state machine वह state machine है जिसमें states की संख्या सीमित होती है
• Turing machine state machine का एक उदाहरण है, और deterministic Turing machine में प्रत्येक state के लिए अगला state अधिकतम एक होता है
• programming language के अर्थ को सटीक रूप से समझाने का व्यावहारिक तरीका operational semantics है, जो उसे state machine में बदलता है
• next-state action केवल उन steps को निर्दिष्ट करती है जो हो सकते हैं; इसका यह मतलब नहीं कि वे अवश्य होंगे
• किसी step के अनिवार्य रूप से होने को निर्दिष्ट करने के लिए fairness property जोड़नी पड़ती है
• fairness के बिना भी commission errors ढूँढने के लिए यह पर्याप्त है, लेकिन omission errors का पता नहीं चलता
• अधिकांश मामलों में errors commission वाले अधिक होते हैं, इसलिए beginners को initial condition और next-state relation लिखने से शुरुआत करनी चाहिए

properties का verification

• यह जाँचने के लिए model लिखा जाता है कि system इच्छित तरीके से काम करता है या नहीं
• TLA+ tools से verify किया जा सकता है कि model सभी संभावित actions के लिए किसी खास property को satisfy करता है या नहीं
• उदाहरण: भले ही 99% initial states में execution सामान्य रूप से समाप्त हो, फिर भी यह verify करना चाहिए कि सभी actions सामान्य रूप से समाप्त हों
• सबसे सामान्य property invariance property है, जो हर state में हमेशा true होनी चाहिए
• fairness condition वाले model में liveness property भी verify करनी चाहिए → उदाहरण: execution का अवश्य समाप्त होना
• अधिक जटिल properties को state machine के रूप में व्यक्त किया जा सकता है, और यह verify किया जा सकता है कि कोई दूसरी state machine उसे implement करती है या नहीं
• TLA+ में state machine और property के बीच कोई औपचारिक भेद नहीं है; दोनों को समान रूप से mathematical formulas के रूप में व्यक्त किया जाता है
• एक state machine का दूसरी state machine को implement करना यह दर्शाता है कि वह formula तार्किक रूप से उसमें शामिल है
• व्यवहार में अधिकांश लोग केवल invariance और simple liveness properties की जाँच करते हैं, लेकिन अधिक जटिल concepts को समझना भी code errors रोकने में मदद करता है

खुद TLA+ भाषा

• TLA+ एक mathematics-based language है और programming language जैसी नहीं दिखती
• programmers mathematical expressions की तुलना में programming languages के अधिक अभ्यस्त होते हैं, इसलिए शुरुआत में यह कठिन लग सकती है
• लेकिन वास्तव में गणित programming language की तुलना में अधिक expressive है
• उदाहरण: GCD को उस सबसे बड़े positive integer के रूप में परिभाषित किया जा सकता है जो दो संख्याओं को divide करता है (calculation method को छोड़ा जा सकता है)
• mathematical definition उद्देश्य के लिए आवश्यक मूल तत्वों को रखकर, अनावश्यक implementation details को abstract कर सकती है
• proceduralization abstraction नहीं देती; वह सिर्फ code को किसी और जगह छिपाती है
• PlusCal, TLA+ में प्रवेश के लिए उपयुक्त है, और अनुभवी लोग भी simple models के लिए PlusCal को पसंद करते हैं
• लेकिन mathematical thinking और high-level modeling के लिए खुद TLA+ को सीखना महत्वपूर्ण है

[gera1d]

https://cacm.acm.org/research/… AWS में इसका अच्छा इस्तेमाल हो रहा है।

[xguru]

Coding प्रोग्रामिंग नहीं है
इस लेख में इसका ज़िक्र हुआ था, इसलिए मैंने इसे खोजकर देखा।

[ryj0902]

मैंने भी इसे पहली बार इसी लेख में देखा, इसलिए इसके बारे में खोज रहा था।