2025-11-13T22:01:14.187429

When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking

He, Jia, Bao et al.

Static resource management in languages remains challenging due to tensions among control, expressiveness, and flexibility. Region-based systems [Grossman et al . 2002; Tofte et al. 2001] offer bulk deallocation via lexically scoped regions, where all allocations follow a stack discipline. However, both regions and their resources are second-class, and neither can escape its scope nor be freely returned. Ownership and linear type systems, exemplified by Rust [Clarke et al. 2013], offer non-lexical lifetimes and robust static guarantees, but rely on invariants that limit higher-order patterns and expressive sharing. In this work, we propose a new type system that unifies these strengths. Our system treats all heap-allocated resources as first-class values, while allowing programmers to control lifetime and granularity through three allocation modes: (1) fresh allocation for individual, non-lexical references; (2) subsequent coallocation grouping resources collectively within shadow arenas; and (3) scoped allocation with lexically bounded lifetimes following stack discipline. Regardless of mode, all resources share a uniform type and have no distinction for generic abstractions, preserving the higher-order parametric nature of the language. Obtaining static safety in higher-order languages with flexible sharing is nontrivial. We address this by extending reachability types [Wei et al. 2024] to collectively track first-class resources, and by adopting flow-insensitive deallocation reasoning for selective stack discipline. These mechanisms yield Aq<: and {A}q<: atop, both formalized and proven type safe and memory safe in Rocq.

academic

जब लाइफटाइम्स मुक्त करें: उच्च-क्रम पहुंचनीयता ट्रैकिंग के साथ एरेनास के लिए एक प्रकार प्रणाली

मूल जानकारी

पेपर आईडी: 2509.04253
शीर्षक: When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
लेखक: Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf (Purdue University, Augusta University)
वर्गीकरण: cs.PL (प्रोग्रामिंग भाषाएं)
प्रकाशन समय: 25 अक्टूबर, 2024 (arXiv v2)
पेपर लिंक: https://arxiv.org/abs/2509.04253

सारांश

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

यह कार्य इन लाभों को एकीकृत करने वाली एक नई प्रकार प्रणाली प्रस्तावित करता है। यह प्रणाली सभी हीप आवंटित संसाधनों को प्रथम-श्रेणी मानों के रूप में मानती है, जबकि प्रोग्रामर को तीन आवंटन मोड के माध्यम से लाइफटाइम्स और दानेदारपन को नियंत्रित करने की अनुमति देती है: (1) व्यक्तिगत गैर-शब्दकोशीय संदर्भों का नया आवंटन; (2) छाया एरेनास के भीतर सामूहिक रूप से समूहीकृत संसाधनों का बाद का सह-आवंटन; (3) स्टैक अनुशासन का पालन करने वाली शब्दकोशीय सीमा लाइफटाइम्स का दायरा आवंटन। किसी भी मोड को अपनाने के बावजूद, सभी संसाधन एकीकृत प्रकार साझा करते हैं, सामान्य अमूर्तता में अविभाज्य, भाषा की उच्च-क्रम पैरामीटरीकरण विशेषताओं को बनाए रखते हैं।

अनुसंधान पृष्ठभूमि और प्रेरणा

समस्या परिभाषा

यह अनुसंधान उच्च-क्रम कार्यात्मक भाषाओं में सुरक्षित, लचीले और नियंत्रणीय संसाधन प्रबंधन को लागू करने की मूल समस्या को हल करने का प्रयास करता है। पारंपरिक विधियों को निम्नलिखित दुविधाओं का सामना करना पड़ता है:

स्टैक बनाम हीप आवंटन का संतुलन: स्टैक मानों में कठोर शब्दकोशीय लाइफटाइम्स होती हैं, सुरक्षित और कुशल लेकिन अनिवार्य रूप से द्वितीयक-श्रेणी के नागरिक; हीप आवंटन स्वतंत्र रूप से प्रवाहित होने वाले प्रथम-श्रेणी मान उत्पन्न करते हैं, लेकिन पूर्वानुमानित रिलीज नियंत्रण का त्याग करते हैं।
मौजूदा प्रणालियों की सीमाएं:
- क्षेत्र-आधारित प्रणालियां (जैसे MLKit, Cyclone): बल्क रिलीज प्रदान करती हैं लेकिन क्षेत्र और संसाधन दोनों ही द्वितीयक-श्रेणी के नागरिक हैं
- स्वामित्व प्रकार प्रणालियां (जैसे Rust): गैर-शब्दकोशीय लाइफटाइम्स प्रदान करती हैं लेकिन उच्च-क्रम पैटर्न और अभिव्यक्ति साझाकरण को सीमित करती हैं
- पहुंचनीयता प्रकार प्रणालियां: उच्च-क्रम कार्यों का समर्थन करती हैं लेकिन दूरदर्शी संरचना सीमाओं से प्रभावित हैं, चक्रीय भंडारण संरचनाओं को संभाल नहीं सकतीं

अनुसंधान प्रेरणा

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

मुख्य योगदान

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

विधि विवरण

मूल अवधारणाएं

1. छाया एरेनास (Shadow Arenas)

छाया एरेनास प्रणाली का मुख्य नवाचार हैं, जिनकी निम्नलिखित विशेषताएं हैं:

अंतर्निहित पहचान: एरेनास सतह वाक्य रचना में स्पष्ट नाम या निर्माता नहीं हैं, संदर्भों के माध्यम से अंतर्निहित रूप से पहचाने जाते हैं

तीन आवंटन रूप:

val fr = new Ref(42)           // नया आवंटन
val ar = new Ref(42) scoped    // दायरा आवंटन  
val a1 = new Ref(42) at ar     // सह-आवंटन

2. मोटे दानेदार पहुंचनीयता ट्रैकिंग

प्रणाली एक द्वि-आयामी भंडारण मॉडल अपनाती है, जहां प्रत्येक संदर्भ एरेना स्थान और आंतरिक ऑफसेट (ℓ, o) द्वारा अनुक्रमित होता है:

पहुंचनीयता एरेना स्तर ℓ पर मोटे दानेदार रूप से ट्रैक की जाती है
एक ही एरेना के भीतर सभी वस्तुएं समान पहुंचनीयता पहचान साझा करती हैं
दूरदर्शी बाधाओं को समाप्त करता है, मनमानी आंतरिक एरेना वस्तु ग्राफ का समर्थन करता है

प्रकार प्रणाली डिजाइन

A^q<: कलन

आधार प्रणाली F^q<: कलन को विस्तारित करती है, जिसमें शामिल हैं:

गैर-शब्दकोशीय छाया एरेनास: संदर्भों को उनके शब्दकोशीय दायरे से बचने का समर्थन करता है
सह-आवंटन वाक्य रचना: ref t1 at t2 नए संदर्भ को मौजूदा एरेना में रखता है
एकीकृत संदर्भ प्रकार: सभी आवंटन रूप Ref[T]^q प्रकार साझा करते हैं

{A}^q<: कलन

दायरा संसाधन प्रबंधन जोड़ने के लिए A^q<: को विस्तारित करता है:

दायरा आवंटन: ref t as x in b शब्दकोशीय सीमा वाले संदर्भ बनाता है
प्रवाह-असंवेदनशील तर्क: गतिशील ट्रैकिंग के माध्यम से स्थानीय स्थान सुरक्षित रिलीज सुनिश्चित करता है
बल्क रिलीज: दायरे के अंत में पूरे एरेना को स्वचालित रूप से रिलीज करता है

तकनीकी नवाचार बिंदु

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

प्रायोगिक सेटअप

औपचारिक सत्यापन

यांत्रिक प्रमाण: सभी औपचारिक परिणाम Rocq में यांत्रिक हैं
प्रकार सुरक्षा: प्रगति और संरक्षण प्रमेय सिद्ध किए गए हैं
मेमोरी सुरक्षा: मुक्त-के-बाद-उपयोग त्रुटियों की अनुपस्थिति की गारंटी देता है

केस स्टडीज

पेपर तीन केस स्टडीज के माध्यम से प्रणाली की अभिव्यक्ति को सत्यापित करता है:

कॉलबैक पंजीकरण: दिखाता है कि गैर-शब्दकोशीय एरेनास कैसे ईवेंट-संचालित प्रोग्रामिंग पैटर्न का समर्थन करते हैं
सामान्य निश्चित बिंदु संयोजक: सिद्ध करता है कि प्रणाली पूर्व पहुंचनीयता प्रकार की सीमाओं को कैसे दूर करती है
चक्रीय भंडारण संरचनाएं: बहु-हॉप चक्रों को सुरक्षित रूप से निर्माण और पुनर्प्राप्त करने की क्षमता प्रदर्शित करता है

प्रायोगिक परिणाम

मुख्य परिणाम

प्रकार सुरक्षा प्रमाण

प्रमेय 4.1 (प्रगति): यदि [∅ | Σ] φ ⊢ t : Q और Σ ok,
तो t एक मान है या ऐसे t', σ' मौजूद हैं कि t | σ → t' | σ'

प्रमेय 4.2 (संरक्षण): यदि प्रकार-अच्छे पद में कमी होती है,
तो विस्तारित प्रकार पर्यावरण मौजूद है जिससे कमी परिणाम अभी भी प्रकार-अच्छा है

अभिव्यक्ति में वृद्धि

मौजूदा प्रणालियों के साथ तुलना दिखाती है कि यह प्रणाली निम्नलिखित विशेषताओं का प्रतिच्छेदन प्राप्त करती है:

✓ स्टैक अनुशासन
✓ अभिव्यक्ति साझाकरण
✓ प्रथम-श्रेणी संसाधन
✓ उच्च-क्रम कार्य

यह एकीकृत प्रणाली में इन सभी गुणों को लागू करने वाला पहला कार्य है।

केस विश्लेषण

कॉलबैक पंजीकरण पैटर्न

val makeHandler = {
  val rp = new Ref() // गैर-शब्दकोशीय संसाधन पूल
  (cb: Int => Unit) => {
    val h = new Ref(cb) at rp
    h // हैंडलर लौटाएं
  }
}

दिखाता है कि कॉलबैक लाइफटाइम्स को प्रबंधित करने के लिए गैर-शब्दकोशीय एरेनास का उपयोग कैसे करें।

चक्रीय संरचना प्रबंधन

{ // दायरा शुरुआत
  val a = new Ref() scoped
  val c1, c2, c3 = new Ref(f) at a
  c1 := x => { (!c2)(x) } // चक्र बनाएं
  c2 := x => { (!c3)(x) }
  c3 := x => { (!c1)(x) }
} // बल्क रिलीज {a, c1, c2, c3}

चक्रीय संदर्भ संरचनाओं को सुरक्षित रूप से निर्माण और रिलीज करने का प्रदर्शन करता है।

निष्कर्ष और चर्चा

मुख्य निष्कर्ष

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

सीमाएं

चक्रीय निर्माण सीमा: हालांकि चक्रीय संरचनाओं का समर्थन करता है, लेकिन कम से कम दो इकाइयों की आवश्यकता है
प्रवाह-संवेदनशील विस्तार: स्पष्ट रिलीज को अभी भी अतिरिक्त प्रवाह-संवेदनशील प्रभाव विस्तार की आवश्यकता है
कार्यान्वयन जटिलता: द्वि-आयामी भंडारण मॉडल रनटाइम कार्यान्वयन की जटिलता बढ़ाता है

भविष्य की दिशाएं

प्रदर्शन अनुकूलन: द्वि-आयामी भंडारण मॉडल के कुशल कार्यान्वयन पर अनुसंधान
समवर्ती विस्तार: प्रणाली को समवर्ती सेटिंग्स तक विस्तारित करना
व्यावहारिक भाषा एकीकरण: वास्तविक प्रोग्रामिंग भाषाओं में प्रणाली को लागू करना

गहन मूल्यांकन

शक्तियां

सैद्धांतिक योगदान महत्वपूर्ण: स्टैक अनुशासन, अभिव्यक्ति साझाकरण, प्रथम-श्रेणी संसाधन और उच्च-क्रम कार्यों के प्रतिच्छेदन को एकीकृत प्रणाली में लागू करने वाला पहला
तकनीकी नवाचार प्रमुख: छाया एरेनास और मोटे दानेदार पहुंचनीयता ट्रैकिंग महत्वपूर्ण नवाचार हैं
औपचारिक कठोरता: पूर्ण यांत्रिक प्रमाण परिणामों की विश्वसनीयता बढ़ाते हैं
अभिव्यक्ति में वृद्धि: पूर्व पहुंचनीयता प्रकार प्रणालियों की दूरदर्शी संरचना सीमाओं को दूर करता है

कमियां

सीमित व्यावहारिकता: अभी तक वास्तविक भाषा में कार्यान्वित नहीं, व्यावहारिक मूल्य सत्यापन के लिए प्रतीक्षा कर रहा है
प्रदर्शन विचार अपर्याप्त: द्वि-आयामी भंडारण मॉडल के प्रदर्शन प्रभाव का विश्लेषण अभाव
सीखने की वक्र खड़ी: प्रणाली जटिलता प्रोग्रामर अपनाने को प्रभावित कर सकती है

प्रभाव

यह कार्य प्रोग्रामिंग भाषा सिद्धांत क्षेत्र में महत्वपूर्ण है, संसाधन प्रबंधन के लिए नई सैद्धांतिक नींव प्रदान करता है, भविष्य की प्रोग्रामिंग भाषा डिजाइन को प्रभावित कर सकता है। विशेष रूप से सटीक संसाधन नियंत्रण की आवश्यकता वाले सिस्टम प्रोग्रामिंग क्षेत्र के लिए, यह विधि नई संभावनाएं प्रदान करती है।

लागू परिदृश्य

सिस्टम प्रोग्रामिंग: सटीक मेमोरी प्रबंधन की आवश्यकता वाली निम्न-स्तरीय प्रणालियां
एम्बेडेड सिस्टम: संसाधन-सीमित वातावरण में सुरक्षित प्रोग्रामिंग
कार्यात्मक भाषाएं: संसाधन प्रबंधन क्षमता की आवश्यकता वाली उच्च-क्रम कार्यात्मक भाषाएं
समवर्ती प्रणालियां: बहु-थ्रेड वातावरण में सुरक्षित संसाधन साझाकरण

संदर्भ

पेपर प्रोग्रामिंग भाषा सिद्धांत क्षेत्र के महत्वपूर्ण कार्यों का हवाला देता है, जिनमें शामिल हैं:

Grossman et al. 2002: Cyclone क्षेत्र प्रणाली
Tofte et al. 2001: MLKit क्षेत्र तर्क
Wei et al. 2024: बहुरूपी पहुंचनीयता प्रकार
Clarke et al. 2013: Rust स्वामित्व प्रकार
Bao et al. 2021: पहुंचनीयता प्रकार मूल सिद्धांत