मल्टीथ्रेड एल्गोरिदम डिज़ाइन/डिबग/साबित करने के लिए विशेष रूप से कठिन हैं। डेकर का एल्गोरिदम एक प्रमुख उदाहरण है कि सही सिंक्रनाइज़ किए गए एल्गोरिदम को डिजाइन करना कितना मुश्किल हो सकता है। तनेनबाम के आधुनिक ऑपरेटिंग सिस्टम अपने आईपीसी अनुभाग में उदाहरणों से भरे हुए हैं। क्या इसके लिए किसी के पास एक अच्छा संदर्भ (किताबें, लेख) है? धन्यवाद!मल्टीथ्रेड एल्गोरिदम की शुद्धता प्रदान करना
@ बस मामले में: मैं हूं। लेकिन जो मैंने सीखा, उससे एक गैर तुच्छ एल्गोरिदम के लिए ऐसा करना एक बड़ा दर्द है। मैं उस तरह की चीज को मस्तिष्क के लोगों के लिए छोड़ देता हूं। मैंने समांतर प्रोग्राम डिज़ाइन से मुझे क्या सीखा है: ए फाउंडेशन (1 9 88) केएम चंडी द्वारा, जे मिश्रा
गारनेटेस पर निर्माण किए बिना कुछ साबित करना असंभव है, इसलिए सबसे पहले आप जो करना चाहते हैं वह परिचित होना है आपके लक्षित मंच का मेमोरी मॉडल; जावा और एक्स 86 दोनों में ठोस और मानकीकृत मेमोरी मॉडल हैं - मैं सीएलआर के बारे में इतना निश्चित नहीं हूं, लेकिन अगर सब कुछ विफल हो जाता है, तो आप अपने लक्ष्य सीपीयू आर्किटेक्चर के मेमोरी मॉडल पर निर्माण करेंगे। इस नियम का अपवाद यह है कि यदि आप ऐसी भाषा का उपयोग करना चाहते हैं जो किसी साझा साझा करने योग्य स्थिति को अनुमति नहीं देता है - मैंने सुना है कि एरलांग ऐसा ही है।
समरूपता की पहली समस्या को परिवर्तनीय स्थिति साझा की जाती है।
द्वारा निर्धारित किया जा सकता है कि:
दूसरी प्रोब समेकन का लीम सुरक्षित प्रकाशन है। आप अन्य धागे के लिए डेटा कैसे उपलब्ध कराते हैं? आप हाथ से कैसे काम करते हैं? आप एपीआई में स्मृति मॉडल में और (उम्मीद है) में इस समस्या का समाधान करेंगे। उदाहरण के लिए जावा, राज्य को प्रकाशित करने के कई तरीके हैं और java.util.concurrent पैकेज में विशेष रूप से इंटर-थ्रेड संचार को संभालने के लिए डिज़ाइन किए गए टूल शामिल हैं।
समेकन की तीसरी (और कठिन) समस्या लॉक हो रही है। Mismanaged लॉक ऑर्डर मृत-ताले का स्रोत है। आप विश्लेषणात्मक रूप से साबित कर सकते हैं, स्मृति मॉडल guarentees पर निर्माण, चाहे आपके कोड में मृत-ताले संभव हो। हालांकि, आपको अपने कोड को उस दिमाग में डिजाइन और लिखने की ज़रूरत है, अन्यथा कोड की जटिलता अभ्यास में प्रदर्शन करने के लिए असंभव ऐसे विश्लेषण को प्रस्तुत कर सकती है।
फिर, आपके पास होने के बाद, या आपके समक्ष होने के बाद, समवर्तीता के सही उपयोग को साबित करें, आपको एकल-थ्रेडेड शुद्धता साबित करनी होगी। एक समवर्ती कोड बेस में हो सकता है कि बग का सेट एकल थ्रेडेड प्रोग्राम कीड़े के सेट के बराबर है, साथ ही सभी संभावित समवर्ती बग।
संक्षिप्त उत्तर: यह कठिन है।
1 9 80 के दशक के अंत से डीईसी एसआरसी मॉडुला -3 और लार्च सामान में कुछ वाकई अच्छा काम था।
उदा।
Thread synchronization: A formal specification (1991) ई Birrell, जेवी Guttag, जे जे Horning, Modula-3 के साथ आर लेविन सिस्टम प्रोग्रामिंग, अध्याय 5
Extended static checking (1998) डेविड एल Detlefs द्वारा द्वारा, डेविड एल Detlefs, के.एच. Rustan, के.एच. Rustan, एम Leino, एम Leino, ग्रेग नेल्सन, ग्रेग नेल्सन, जेम्स बी सैक्स, जेम्स बी Saxe
Modula के अच्छे विचार से कुछ - 3 इसे जावा दुनिया में बना रहे हैं, उदा। जेएमएल, हालांकि intro कहता है कि "जेएमएल वर्तमान में अनुक्रमिक विनिर्देश तक सीमित है"।
gatekeeper.dec.com लिंक टूटा हुआ है, लेकिन विस्तारित स्थैतिक जांच पर डीईसी एसआरसी रिपोर्ट http://research.microsoft.com/en-us/um/people/leino/papers/src-159.pdf पर उपलब्ध है । मैं सहमत हूं कि ईएससी वास्तव में अच्छा काम था। –
मेरे पास कोई ठोस संदर्भ नहीं है, लेकिन हो सकता है कि आप ओविकि-ग्रिस सिद्धांत (यदि आप प्रमेय सिद्ध करना चाहते हैं) या सिद्धांत/बीजगणित प्रक्रिया (जिसके लिए विभिन्न मॉडल-जांच उपकरण भी उपलब्ध हैं) में देखना चाहें ।
The Pi-Calculus, A Theory of Mobile Processes शुरू करने के लिए एक अच्छी जगह है।
"समवर्ती और वितरण प्रोग्रामिंग के सिद्धांत", एम बेन-अरी
ISBN-13:
http://my.safaribooksonline.com/9780321312839
यह वही था जो मैं खोज रहा था। धन्यवाद! – Leandro
@Leandro: यदि यह "आप बहुत कुछ" बिल्कुल खोज रहे थे, तो आप जवाब स्वीकार कर सकते हैं। –
विस्तृत करने का प्रयास करें। – GEOCHET