नियंत्रण प्रवाह ग्राफ मशीनों के लिए संरचनात्मक परिचालन 의미

कंपाइलर कम-स्तरीय कार्यक्रमों के नियंत्रण प्रवाह ग्राफ (CFG) प्रतिनिधित्वों का उपयोग करते हैं क्योंकि वे कार्यक्रम विश्लेषण और अनुकूलन के लिए उपयुक्त होते हैं। हालाँकि, CFG कार्यक्रमों के व्यवहार और मेटाथ्योरी को औपचारिक बनाना सरल नहीं है: CFG कार्यक्रम अच्छी तरह से सम्मिलित नहीं होते, उनके अर्थ संलग्न राज्य पर निर्भर करते हैं, और, इसके परिणामस्वरूप, उन्हें ऐसे साधारण समीकरणीय सिद्धांत का लाभ नहीं मिलता जिसका उपयोग कार्यक्रम रूपांतरणों की सटीकता के बारे में तर्क करने के लिए किया जा सके। इसके विपरीत, लैम्ब्डा-कैलकुलस-आधारित मध्यवर्ती प्रतिनिधित्वों में अच्छी तरह से समझी जाने वाली परिचालन 의미 और मेटाथ्योरी होती है, जिसमें समृद्ध समीकरणीय सिद्धांत शामिल होते हैं, जो सभी उन्हें औपचारिक सत्यापन के लिए उपयुक्त बनाते हैं। यह पेपर (एक रूपांतर) लेवी के कॉल-बाय-पुश-वैल्यू (CBPV) कैल्कुलस और एक नियंत्रण प्रवाह ग्राफ मशीन के बीच एक तंग समानता स्थापित करता है जिसके निर्देश स्थिर एकल असाइनमेंट (SSA) रूप में होते हैं। अनुरूपता को एक श्रृंखला के माध्यम से सटीक बनाया गया है जो CBPV भाषा के संरचनात्मक परिचालन 의미 के परिवर्तन और SSA रूप के गणना चरणों को संरेखित करती है। लक्षित मशीन, जो CBPV भाषा से व्युत्पन्न है, नियंत्रण प्रवाह ग्राफों के निष्पादन मॉडल को सटीक रूप से कैप्चर करती है, जिसमें प्रत्यक्ष कूद, आपसी पुनरावर्ती कोड ब्लॉक और मल्टी-आर्गुमेंट फ़ंक्शन कॉल शामिल हैं, और क्लोजर-फ्री उपसंग्रह आधुनिक कंपाइलरों जैसे llvm और gcc में पाए जाने वाले SSA मध्यवर्ती प्रतिनिधित्वों के समान है। सभी भाषा/अभीष्ट मशीन अर्थ और उनके बीच संबंध बनाने वाले प्रमेयों की परिभाषाएँ पूर्ण रूप से कोक में सत्यापित की गई हैं।