अनुक्रमिक प्रक्रियाओं का संचार करना

Not to be confused with Constraint satisfaction problem.

कंप्यूटर विज्ञान में, अनुक्रमिक प्रक्रियाओं (सीएसपी) को संप्रेषित करना समवर्ती प्रणालियों में बातचीत के नमूना का वर्णन करने के लिए एक औपचारिक भाषा है। यह चैनल (प्रोग्रामिंग) के माध्यम से गुजरने वाले संदेश के आधार पर प्रक्रिया बीजगणित, या प्रक्रिया कलन के रूप में ज्ञात संगामिति के गणितीय सिद्धांतों के परिवार का एक सदस्य है। सीएसपी ओकैम (प्रोग्रामिंग भाषा) प्रोग्रामिंग भाषा के डिजाइन में अत्यधिक प्रभावशाली था और लिंबो (प्रोग्रामिंग भाषा) जैसी प्रोग्रामिंग भाषाओं के डिजाइन को भी प्रभावित किया, राफ्टलिब, एरलांग (प्रोग्रामिंग भाषा), जाओ (प्रोग्रामिंग भाषा),क्रिस्टल (प्रोग्रामिंग भाषा), और क्लोजर का core.async। सीएसपी को पहली बार 1978 में टोनी होरे के एक लेख में वर्णित किया गया था, लेकिन तब से काफी हद तक विकसित हो गया है। सीएसपी व्यावहारिक रूप से उद्योग में औपचारिक विनिर्देश के लिए एक उपकरण के रूप में विभिन्न प्रणालियों के समवर्ती पहलुओं, जैसे टी 9000 ट्रांसप्यूटर, के रूप में लागू किया गया है। साथ ही एक सुरक्षित ईकॉमर्स सिस्टम। सीएसपी का सिद्धांत अभी भी सक्रिय शोध का विषय है, जिसमें व्यावहारिक प्रयोज्यता की अपनी सीमा को बढ़ाने के लिए काम शामिल है (उदाहरण के लिए, उन प्रणालियों के पैमाने को बढ़ाना जिनका विश्लेषण किया जा सकता है)।

इतिहास

होरे के मूल 1978 के लेख में प्रस्तुत सीएसपी का संस्करण अनिवार्य रूप से एक प्रक्रिया कलन के बजाय एक समवर्ती प्रोग्रामिंग भाषा थी। सीएसपी के बाद के संस्करणों की तुलना में इसमें काफी भिन्न वाक्य - विन्यास था, गणितीय रूप से परिभाषित शब्दार्थ नहीं था, और अबाधित अनिर्धारणवाद का प्रतिनिधित्व करने में असमर्थ था। मूल सीएसपी में प्रोग्राम एक निश्चित संख्या में अनुक्रमिक प्रक्रियाओं की एक समानांतर रचना के रूप में लिखे गए थे जो एक दूसरे के साथ सख्ती से सिंक्रोनस मैसेज-पासिंग के माध्यम से संचार करते थे। सीएसपी के बाद के संस्करणों के विपरीत, प्रत्येक प्रक्रिया को एक स्पष्ट नाम दिया गया था, और संदेश के स्रोत या गंतव्य को भेजने या प्राप्त करने की प्रक्रिया के नाम को निर्दिष्ट करके परिभाषित किया गया था। उदाहरण के लिए, प्रक्रिया

कॉपी = * [सी: चरित्र; पश्चिम?सी → पूर्व!सी]

नामित प्रक्रिया से बार-बार एक चरित्र प्राप्त करता है west और उस कैरेक्टर को नाम प्रोसेस करने के लिए भेजता है east. समानांतर रचना

[पश्चिम::अलग करना || एक्स :: कॉपी || पूर्व :: इकट्ठा]

नाम देता है west तक DISASSEMBLE प्रक्रिया, X तक COPY प्रक्रिया, और east तक ASSEMBLE प्रक्रिया, और इन तीन प्रक्रियाओं को समवर्ती रूप से निष्पादित करता है।

सीएसपी के मूल संस्करण के प्रकाशन के बाद होरे, स्टीफन ब्रूक्स और बिल रोसको|ए. डब्ल्यू। रोस्को ने सीएसपी के सिद्धांत को अपने आधुनिक, प्रक्रिया बीजगणितीय रूप में विकसित और परिष्कृत किया। CSP को एक प्रक्रिया बीजगणित में विकसित करने के लिए लिया गया दृष्टिकोण रॉबिन मिलनर के कम्युनिकेटिंग सिस्टम्स (CCS) के कलन पर काम से प्रभावित था और इसके विपरीत। सीएसपी का सैद्धांतिक संस्करण शुरू में ब्रुक्स, होरे और रोसको द्वारा 1984 के एक लेख में प्रस्तुत किया गया था, और बाद में होरे की पुस्तक संचार अनुक्रमिक प्रक्रियाओं में,जिसे 1985 में प्रकाशित किया गया था। सितंबर 2006 में, वह पुस्तक अभी भी तीसरा सबसे उद्धृत Citeseer के अनुसार अब तक का कंप्यूटर विज्ञान संदर्भ था (यद्यपि इसके नमूने की प्रकृति के कारण एक अविश्वसनीय स्रोत)। होरे की किताब के प्रकाशन के बाद से सीएसपी के सिद्धांत में कुछ छोटे बदलाव हुए हैं। इनमें से अधिकांश परिवर्तन CSP प्रक्रिया विश्लेषण और सत्यापन के लिए स्वचालित उपकरणों के आगमन से प्रेरित थे। रोसको का सिद्धांत और संगामिति का अभ्यासCSP के इस नए संस्करण का वर्णन करता है।

अनुप्रयोग

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

सॉफ्टवेयर डिजाइन के लिए सीएसपी के औद्योगिक अनुप्रयोग ने आमतौर पर भरोसेमंद और सुरक्षा-महत्वपूर्ण प्रणालियों पर ध्यान केंद्रित किया है। उदाहरण के लिए, ब्रेमेन इंस्टीट्यूट फॉर सेफ सिस्टम्स और डेमलर क्रिसलर एयरोस्पेस | डेमलर-बेंज एयरोस्पेस ने एक फॉल्ट-मैनेजमेंट सिस्टम और एवियोनिक्स इंटरफ़ेस (कोड की लगभग 23,000 लाइनों से मिलकर) को सीएसपी में अंतर्राष्ट्रीय अंतरिक्ष स्टेशन पर उपयोग के लिए तैयार किया और मॉडल का विश्लेषण किया। यह पुष्टि करने के लिए कि उनका डिज़ाइन डेडलॉक और लाइवलॉक से मुक्त था। मॉडलिंग और विश्लेषण प्रक्रिया ऐसी कई त्रुटियों को उजागर करने में सक्षम थी जिनका अकेले परीक्षण का उपयोग करके पता लगाना मुश्किल होता। इसी तरह, प्रैक्सिस हाई इंटीग्रिटी सिस्टम्स ने एक सुरक्षित स्मार्ट-कार्ड प्रमाणन प्राधिकरण के लिए सॉफ्टवेयर के विकास (कोड की लगभग 100,000 लाइनें) के दौरान सीएसपी मॉडलिंग और विश्लेषण लागू किया ताकि यह सत्यापित किया जा सके कि उनका डिज़ाइन सुरक्षित और डेडलॉक से मुक्त था। प्रैक्सिस का दावा है कि तुलनीय प्रणालियों की तुलना में प्रणाली में बहुत कम दोष दर है।

चूंकि सीएसपी जटिल संदेश एक्सचेंजों को शामिल करने वाली प्रणालियों के मॉडलिंग और विश्लेषण के लिए उपयुक्त है, इसलिए इसे संचार और सुरक्षा प्रोटोकॉल के सत्यापन के लिए भी लागू किया गया है। इस प्रकार के अनुप्रयोग का एक प्रमुख उदाहरण लोवे द्वारा CSP और FDR2|FDR शोधन-परीक्षक का उपयोग नीडम-श्रोएडर प्रोटोकॉल|नीडम-श्रोएडर सार्वजनिक-कुंजी प्रमाणीकरण प्रोटोकॉल पर पहले अज्ञात हमले की खोज करने के लिए और फिर एक सही प्रोटोकॉल विकसित करने के लिए किया जाता है। आक्रमण को परास्त करने में सक्षम है।

अनौपचारिक विवरण

जैसा कि इसके नाम से पता चलता है, सीएसपी उन घटक प्रक्रियाओं के संदर्भ में सिस्टम के विवरण की अनुमति देता है जो स्वतंत्र रूप से संचालित होते हैं, और केवल संदेश पासिंग | संदेश-पासिंग संचार के माध्यम से एक दूसरे के साथ बातचीत करते हैं। हालांकि, सीएसपी नाम का अनुक्रमिक हिस्सा अब एक मिथ्या नाम है, क्योंकि आधुनिक सीएसपी घटक प्रक्रियाओं को अनुक्रमिक प्रक्रियाओं के रूप में और अधिक आदिम प्रक्रियाओं की समानांतर संरचना के रूप में परिभाषित करने की अनुमति देता है। विभिन्न प्रक्रियाओं के बीच संबंध, और जिस तरह से प्रत्येक प्रक्रिया अपने पर्यावरण के साथ संचार करती है, उसे विभिन्न प्रक्रिया गणना ऑपरेटरों का उपयोग करके वर्णित किया गया है। इस बीजगणितीय दृष्टिकोण का उपयोग करते हुए, कुछ आदिम तत्वों से काफी जटिल प्रक्रिया विवरणों का निर्माण आसानी से किया जा सकता है।

आदिम

CSP अपनी प्रक्रिया बीजगणित में प्रिमिटिव के दो वर्ग प्रदान करता है:

आयोजन

घटनाएँ संचार या बातचीत का प्रतिनिधित्व करती हैं। उन्हें अविभाज्य और तात्कालिक माना जाता है। वे परमाणु नाम (जैसे चालू, बंद), यौगिक नाम (जैसे वाल्व.ओपन, वाल्व.क्लोज़), या इनपुट/आउटपुट इवेंट (जैसे माउस?xy, स्क्रीन!बिटमैप) हो सकते हैं।

आदिम प्रक्रियाएं

आदिम प्रक्रियाएं मौलिक व्यवहारों का प्रतिनिधित्व करती हैं: उदाहरणों में STOP (वह प्रक्रिया जो कुछ भी संचार नहीं करती है, जिसे गतिरोध भी कहा जाता है), और SKIP (जो सफल समाप्ति का प्रतिनिधित्व करता है) शामिल हैं।

बीजगणितीय ऑपरेटर

सीएसपी में बीजगणितीय ऑपरेटरों की एक विस्तृत श्रृंखला है। प्रमुख हैं:

उपसर्ग

उपसर्ग ऑपरेटर एक नई प्रक्रिया का उत्पादन करने के लिए एक घटना और एक प्रक्रिया को जोड़ता है। उदाहरण के लिए,

$$a\to P$$

वह प्रक्रिया है जो संवाद करने को तैयार है a अपने पर्यावरण के साथ और उसके बाद a, प्रक्रिया की तरह व्यवहार करता है P.

नियतात्मक पसंद

नियतात्मक (या बाहरी) पसंद ऑपरेटर एक प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच एक विकल्प के रूप में परिभाषित करने की अनुमति देता है और पर्यावरण को किसी एक प्रक्रिया के लिए प्रारंभिक घटना को संप्रेषित करके पसंद को हल करने की अनुमति देता है। उदाहरण के लिए,

$$(a\to P)\Box (b\to Q)$$

वह प्रक्रिया है जो प्रारंभिक घटनाओं को संप्रेषित करने के लिए तैयार है a और b और बाद में या तो व्यवहार करता है P या Q, पर्यावरण किस प्रारंभिक घटना के आधार पर संवाद करना चुनता है। अगर दोनों a और b को एक साथ संप्रेषित किया गया था, तो विकल्प को गैर-निर्धारित रूप से हल किया जाएगा।

गैर नियतात्मक विकल्प

nondeterministic (या आंतरिक) पसंद ऑपरेटर एक प्रक्रिया के भविष्य के विकास को दो घटक प्रक्रियाओं के बीच एक विकल्प के रूप में परिभाषित करने की अनुमति देता है, लेकिन पर्यावरण को किसी भी नियंत्रण की अनुमति नहीं देता है कि कौन से घटक प्रक्रियाओं का चयन किया जाएगा। उदाहरण के लिए,

$$(a\to P)\sqcap (b\to Q)$$

जैसा व्यवहार कर सकता है $(a\to P)$ या $(b\to Q)$. मानने से इंकार कर सकता है a या b और संवाद करने के लिए तभी बाध्य है जब पर्यावरण दोनों प्रदान करता है a और b. यदि पसंद के दोनों पक्षों की प्रारंभिक घटनाएँ समान हैं, तो गैर-नियतात्मकता को अनजाने में एक नाममात्र नियतात्मक पसंद में पेश किया जा सकता है। तो, उदाहरण के लिए,

$$(a\to a\to {\text{STOP}})\Box (a\to b\to {\text{STOP}})$$

के बराबर है

$$a\to {\big (}(a\to {\text{STOP}})\sqcap (b\to {\text{STOP}}){\big )}$$

इंटरलिविंग

इंटरलीविंग ऑपरेटर पूरी तरह से स्वतंत्र समवर्ती गतिविधि का प्रतिनिधित्व करता है। प्रक्रिया

$$P\;|||\;Q$$

दोनों के रूप में व्यवहार करता है P और Q इसके साथ ही। दोनों प्रक्रियाओं की घटनाओं को मनमाने ढंग से समय के साथ जोड़ा जाता है।

इंटरफ़ेस समानांतर

इंटरफ़ेस समानांतर ऑपरेटर समवर्ती गतिविधि का प्रतिनिधित्व करता है जिसके लिए घटक प्रक्रियाओं के बीच सिंक्रनाइज़ेशन की आवश्यकता होती है: इंटरफ़ेस सेट में कोई भी घटना तभी हो सकती है जब सभी घटक प्रक्रियाएँ उस घटना में संलग्न होने में सक्षम हों। उदाहरण के लिए, प्रक्रिया

$$P\;|[\{a\}]|\;Q$$

इसकी आवश्यकता है P और Q दोनों को ईवेंट करने में सक्षम होना चाहिए a उस घटना के घटित होने से पहले। तो, उदाहरण के लिए, प्रक्रिया

$$(a\to P)\;|[\{a\}]|\;(a\to Q)$$

आयोजन में शामिल हो सकते हैं a और प्रक्रिया बनें

$$P\;|[\{a\}]|\;Q$$

जबकि

$$(a\to P)\;|[\{a,b\}]|\;(b\to Q)$$

बस गतिरोध होगा।

छुपा रहे है

छुपाने वाला ऑपरेटर कुछ घटनाओं को अप्राप्य बनाकर अमूर्त प्रक्रियाओं का एक तरीका प्रदान करता है। छिपाने का एक तुच्छ उदाहरण है

$$(a\to P)\setminus \{a\}$$

जो, यह मानते हुए कि घटना a में दिखाई नहीं देता P, बस इतना कम कर देता है

$$P$$

उदाहरण

मूलरूप सीएसपी उदाहरणों में से एक चॉकलेट वेंडिंग मशीन का एक सार प्रतिनिधित्व है और कुछ चॉकलेट खरीदने के इच्छुक व्यक्ति के साथ इसकी बातचीत है। यह वेंडिंग मशीन दो अलग-अलग घटनाओं, "कॉइन" और "चोक" को अंजाम देने में सक्षम हो सकती है, जो क्रमशः भुगतान की प्रविष्टि और चॉकलेट की डिलीवरी का प्रतिनिधित्व करती हैं। एक मशीन जो चॉकलेट देने से पहले भुगतान (केवल नकद में) की मांग करती है, उसे इस प्रकार लिखा जा सकता है:

$$\mathrm {VendingMachine} =\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP}$$

एक व्यक्ति जो भुगतान करने के लिए एक सिक्के या कार्ड का उपयोग करना चुन सकता है, उसे इस प्रकार मॉडल किया जा सकता है:

$$\mathrm {Person} =(\mathrm {coin} \rightarrow \mathrm {STOP} )\Box (\mathrm {card} \rightarrow \mathrm {STOP} )$$

इन दोनों प्रक्रियाओं को समानांतर में रखा जा सकता है, ताकि वे एक दूसरे के साथ बातचीत कर सकें। समग्र प्रक्रिया का व्यवहार उन घटनाओं पर निर्भर करता है जिन पर दो घटक प्रक्रियाओं को सिंक्रनाइज़ करना चाहिए। इस प्रकार,

$$\mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} ,\mathrm {card} \right\}\right]\right\vert \mathrm {Person} \equiv \mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP}$$

जबकि यदि केवल "कॉइन" पर सिंक्रोनाइज़ेशन की आवश्यकता होती है, तो हम प्राप्त करेंगे

$$\mathrm {VendingMachine} \left\vert \left[\left\{\mathrm {coin} \right\}\right]\right\vert \mathrm {Person} \equiv \left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)$$

यदि हम "सिक्का" और "कार्ड" घटनाओं को छिपाकर इस बाद की समग्र प्रक्रिया को अमूर्त करते हैं, अर्थात

$$\left(\left(\mathrm {coin} \rightarrow \mathrm {choc} \rightarrow \mathrm {STOP} \right)\Box \left(\mathrm {card} \rightarrow \mathrm {STOP} \right)\right)\setminus \left\{\mathrm {coin,card} \right\}$$

हमें गैर-नियतात्मक प्रक्रिया मिलती है

$$\left(\mathrm {choc} \rightarrow \mathrm {STOP} \right)\sqcap \mathrm {STOP}$$

यह एक ऐसी प्रक्रिया है जो या तो "चोक" घटना की पेशकश करती है और फिर रुक जाती है, या बस रुक जाती है। दूसरे शब्दों में, यदि हम अमूर्तता को सिस्टम के बाहरी दृश्य के रूप में मानते हैं (उदाहरण के लिए, कोई व्यक्ति जो व्यक्ति द्वारा किए गए निर्णय को नहीं देखता है), गैर-नियतात्मक एल्गोरिदम पेश किया गया है।

औपचारिक परिभाषा

सिंटेक्स

CSP का सिंटैक्स "कानूनी" तरीकों को परिभाषित करता है जिसमें प्रक्रियाओं और घटनाओं को जोड़ा जा सकता है। होने देना e एक घटना हो, और X घटनाओं का एक सेट हो। तब CSP के मूल सिंटैक्स को इस प्रकार परिभाषित किया जा सकता है:

$$\mathbf {div}$$