मेटास्टेबल विफलताओं के लिए एक सिद्धांत-आधारित समाधान की मेरी खोज मुझे स्व-स्थिरीकरण पर वापस ले आई है। एक हालिया पेपर ने समस्या को स्व-स्थिरीकरण प्रणालियों की संयोजन से जोड़ा, लेकिन साहित्य खोज से कुछ भी उपयोगी नहीं मिला। 2000 के दशक की शुरुआत तक स्तरित स्थिरीकरण पहले से मौजूद था, और तब से कुछ भी मौलिक जोड़ा नहीं गया प्रतीत होता है।

मैंने एक ठोस उदाहरण का उपयोग करके समस्या पर हमला किया: अनुबंधों के साथ दो घटकों के रूप में एक पुनःप्रयास तूफान का भरोसा-गारंटी TLA+ मॉडल। वह मॉडल मेटास्टेबल विफलता को पुन: उत्पन्न करता है क्योंकि संयोजन अच्छे राज्यों से काम करता था लेकिन विफल हो गया जब एक बड़े झटके ने आधार मामले को हटा दिया। हर राज्य से भरोसा-गारंटी संयोजन की खोज करने पर Kim, Arcak और Seshia का 2017 का नियंत्रण सिद्धांत पेपर, "A Small Gain Theorem for Parametric Assume-Guarantee Contracts" सामने आया। यह पेपर मोटे तौर पर वही करता है जो मैं चाहता हूं: स्तरित या अवरोधन के बिना दो घटकों के बीच चक्रीय तर्क का निर्वहन। लेकिन इसमें गंभीर सीमाएँ हैं। एक घटक संकेतों पर एक इनपुट-आउटपुट संबंध है, और अनुबंध एक इनपुट बाध्य को एक आउटपुट बाध्य से जोड़ते हैं। यह स्मृतिहीन दृष्टिकोण पिछले दौर से जमा हो रहे बैकलॉग को व्यक्त नहीं कर सकता, जिससे कतारें बाहर हो जाती हैं। इसका स्थिरीकरण से भी कोई संबंध नहीं है।

फिर भी, स्व-स्थिरीकरण और मेटास्टेबिलिटी के संयोजन सिद्धांत की ओर कुछ टुकड़े चुराने लायक हैं। नीचे मैं इसे काम करने की कोशिश करता हूं... कुछ हद तक असफल।

हमारे मूल मॉडल में, पुनःप्रयासकर्ता की गारंटी सशर्त थी: "यदि कतार 6 से नीचे है, तो मैं कोई पुनःप्रयास नहीं भेजता"। पैरामीट्रिक मान-गारंटी पेपर का बड़ा विचार हर जगह को कवर करने वाले अनुबंधों का एक परिवार लिखना है। स्थिरांक: S=3 सर्वर क्षमता, A_max=2 नए आगमन, T=2 टाइमआउट, विलंबता सीमा S·T=6। यह λ(L) = ⌊(L-6)/2⌋ देता है। पुराना अनुबंध शीर्ष पंक्ति है: λ(6)=0। प्रत्येक पंक्ति को एक वादा मिलता है, इसलिए हमें साधारण अनुबंधों का एक बंडल मिलता है, प्रत्येक बुराई स्तर p के लिए एक: φ_a = ∨_p ψ_a(p); φ_g = ∧_p (ψ_a(p) ⇒ ψ_g(λ(p)))। मान पक्ष एक विच्छेद है क्योंकि स्तर विकल्प हैं। गारंटी पक्ष एक संयोजन है; दायित्व संचयी हैं। जिन पंक्तियों की स्थिति झूठी है उनकी कोई कीमत नहीं है; नेस्टेड स्तरों का मतलब है कि सबसे कड़ा जीतता है।

मुख्य संस्थाएँ: लोग: Kim, Arcak, Seshia