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
  • শিরোনাম: যখন জীবনকাল মুক্তি দেয়: উচ্চতর-ক্রম পৌঁছানোযোগ্যতা ট্র্যাকিং সহ অ্যারেনার জন্য একটি টাইপ সিস্টেম
  • লেখক: সিয়ুয়ান হে, সংলিন জিয়া, ইউয়ান বাও, টিয়ার্ক রম্পফ (পার্ডু বিশ্ববিদ্যালয়, অগাস্টা বিশ্ববিদ্যালয়)
  • শ্রেণীবিভাগ: cs.PL (প্রোগ্রামিং ভাষা)
  • প্রকাশনার সময়: ২০২৫ সালের ১০ অক্টোবর (arXiv v2)
  • পেপার লিংক: https://arxiv.org/abs/2509.04253

সারসংক্ষেপ

স্ট্যাটিক সম্পদ ব্যবস্থাপনা প্রোগ্রামিং ভাষায় এখনও চ্যালেঞ্জিং, প্রধানত নিয়ন্ত্রণযোগ্যতা, প্রকাশনীয়তা এবং নমনীয়তার মধ্যে উত্তেজনার কারণে। অঞ্চল-ভিত্তিক সিস্টেমগুলি শব্দার্থিক সুযোগ অঞ্চলের মাধ্যমে বাল্ক রিলিজ প্রদান করে, কিন্তু অঞ্চল এবং তাদের সম্পদ উভয়ই দ্বিতীয় শ্রেণীর নাগরিক, সুযোগ থেকে পালাতে বা অবাধে ফেরত দিতে পারে না। রাস্টের প্রতিনিধিত্ব করে এমন মালিকানা এবং রৈখিক টাইপ সিস্টেমগুলি অ-শব্দার্থিক জীবনকাল এবং শক্তিশালী স্ট্যাটিক গ্যারান্টি প্রদান করে, কিন্তু নির্ভরশীল অপরিবর্তনীয়তা উচ্চতর-ক্রম প্যাটার্ন এবং প্রকাশনীয় ভাগাভাগি সীমিত করে।

এই কাজটি এই সুবিধাগুলিকে একীভূত করে এমন একটি নতুন টাইপ সিস্টেম প্রস্তাব করে। সিস্টেমটি সমস্ত হিপ বরাদ্দকৃত সম্পদকে প্রথম-শ্রেণীর মান হিসাবে বিবেচনা করে, যখন প্রোগ্রামারদের তিনটি বরাদ্দ প্যাটার্নের মাধ্যমে জীবনকাল এবং দানাদারিত্ব নিয়ন্ত্রণ করতে দেয়: (১) স্বতন্ত্র অ-শব্দার্থিক রেফারেন্সের তাজা বরাদ্দ; (२) ছায়া অ্যারেনার মধ্যে সম্পদ সম্মিলিত গ্রুপিং এর পরবর্তী সহ-বরাদ্দ; (३) স্ট্যাক শৃঙ্খলা অনুসরণ করে এমন শব্দার্থিক সীমানা জীবনকালের সুযোগ বরাদ্দ। যেকোনো প্যাটার্ন গ্রহণ করা হোক না কেন, সমস্ত সম্পদ একটি একীভূত টাইপ ভাগ করে, সাধারণ বিমূর্ততায় পার্থক্যহীন, ভাষার উচ্চতর-ক্রম প্যারামিটারাইজেশন বৈশিষ্ট্য বজায় রাখে।

গবেষণা পটভূমি এবং প্রেরণা

সমস্যা সংজ্ঞা

এই গবেষণা যে মূল সমস্যা সমাধান করতে চায় তা হল উচ্চতর-ক্রম কার্যকরী ভাষায় নিরাপদ, নমনীয় এবং নিয়ন্ত্রণযোগ্য সম্পদ ব্যবস্থাপনা বাস্তবায়ন করা। ঐতিহ্যবাহী পদ্ধতিগুলি নিম্নলিখিত দ্বিধার মুখোমুখি হয়:

১. স্ট্যাক বনাম হিপ বরাদ্দের ভারসাম্য: স্ট্যাক মানগুলির কঠোর শব্দার্থিক জীবনকাল রয়েছে, নিরাপদ এবং দক্ষ কিন্তু অপরিহার্যভাবে দ্বিতীয় শ্রেণীর নাগরিক; হিপ বরাদ্দ অবাধে প্রবাহিত প্রথম-শ্রেণীর মান তৈরি করে, কিন্তু পূর্বাভাসযোগ্য রিলিজ নিয়ন্ত্রণ ত্যাগ করে।

२. বিদ্যমান সিস্টেমের সীমাবদ্ধতা:

  • অঞ্চল-ভিত্তিক সিস্টেম (যেমন MLKit, Cyclone): বাল্ক রিলিজ প্রদান করে কিন্তু অঞ্চল এবং সম্পদ উভয়ই দ্বিতীয় শ্রেণীর নাগরিক
  • মালিকানা টাইপ সিস্টেম (যেমন Rust): অ-শব্দার্থিক জীবনকাল প্রদান করে কিন্তু উচ্চতর-ক্রম প্যাটার্ন এবং প্রকাশনীয় ভাগাভাগি সীমিত করে
  • পৌঁছানোযোগ্যতা টাইপ সিস্টেম: উচ্চতর কার্যকারিতা সমর্থন করে কিন্তু টেলিস্কোপ কাঠামো দ্বারা সীমাবদ্ধ, চক্রাকার সংরক্ষণ কাঠামো পরিচালনা করতে পারে না

গবেষণা প্রেরণা

লেখকরা বিভিন্ন সম্পদ ব্যবস্থাপনা কৌশলের সুবিধাগুলি একীভূত করতে চান: স্ট্যাক শৃঙ্খলার নিরাপত্তা, উচ্চতর-ক্রম ভাষার প্রকাশনীয়তা, এবং সম্পদকে প্রথম-শ্রেণীর সত্তা হিসাবে বিবেচনা করার নমনীয়তা।

মূল অবদান

१. একীভূত সম্পদ পরিচালনা: সমস্ত মেমরি সম্পদ একটি একক রেফারেন্স টাইপ সহ প্রথম-শ্রেণীর মান, স্ট্যাক এবং হিপ বরাদ্দ বিমূর্ত করে, ক্লায়েন্ট কোডকে রেফারেন্সের নির্দিষ্ট সংরক্ষণ মডেল সম্পর্কে সাধারণ থাকতে দেয়।

२. নিয়ন্ত্রণের নমনীয়তা: মেমরি সম্পদ ব্যবহারকারী নিয়ন্ত্রণের মাধ্যমে অ-শব্দার্থিক বা শব্দার্থিক হতে পারে, স্বতন্ত্র বা সম্মিলিত হতে পারে, এবং কোনো টাইপ পার্থক্য ছাড়াই।

३. স্ট্যাটিক নিরাপত্তা গ্যারান্টি: পৌঁছানোযোগ্যতা টাইপ মেমরি সম্পদ প্রবাহ ট্র্যাক করে এবং তাদের নিরাপদ ব্যবহার নিশ্চিত করে; ব্যবহারকারীরা প্রবাহ-অসংবেদনশীল যুক্তির মাধ্যমে নির্বাচনী স্ট্যাক শৃঙ্খলা আরোপ করতে পারে পূর্বাভাসযোগ্য রিলিজ এবং ব্যবহার-পরবর্তী-মুক্তি ত্রুটি নিশ্চিত করতে।

४. প্রকাশনীয় উচ্চতর-ক্রম বৈশিষ্ট্য: সিস্টেম পরিবর্তনশীল ভাগাভাগি এবং চক্রাকার সংরক্ষণ কাঠামো সহ উচ্চতর কার্যকারিতা সমর্থন করে, পূর্ববর্তী পৌঁছানোযোগ্যতা সিস্টেমের প্রকাশনীয়তা অতিক্রম করে।

পদ্ধতি বিস্তারিত

মূল ধারণা

१. ছায়া অ্যারেনা (Shadow Arenas)

ছায়া অ্যারেনা সিস্টেমের মূল উদ্ভাবন, নিম্নলিখিত বৈশিষ্ট্য সহ:

  • অন্তর্নিহিত পরিচয়: অ্যারেনা পৃষ্ঠ সিনট্যাক্সে স্পষ্ট নাম বা নির্মাতা নেই, রেফারেন্সের মাধ্যমে অন্তর্নিহিতভাবে চিহ্নিত
  • তিনটি বরাদ্দ ফর্ম: 
    val fr = new Ref(42)           // তাজা বরাদ্দ
val ar = new Ref(42) scoped    // সুযোগ বরাদ্দ  
val a1 = new Ref(42) at ar     // সহ-বরাদ্দ

२. মোটা-দানাদার পৌঁছানোযোগ্যতা ট্র্যাকিং

সিস্টেম একটি দ্বি-মাত্রিক সংরক্ষণ মডেল গ্রহণ করে, প্রতিটি রেফারেন্স অ্যারেনা অবস্থান এবং অভ্যন্তরীণ অফসেট (ℓ, o) দ্বারা সূচীকৃত:

  • পৌঁছানোযোগ্যতা অ্যারেনা স্তরে ℓ মোটা-দানাদার ট্র্যাক করা হয়
  • একই অ্যারেনার মধ্যে সমস্ত অবজেক্ট একই পৌঁছানোযোগ্যতা পরিচয় ভাগ করে
  • টেলিস্কোপ সীমাবদ্ধতা দূর করে, অ্যারেনার মধ্যে অবজেক্ট গ্রাফের নির্বিচার সমর্থন করে

টাইপ সিস্টেম ডিজাইন

A^q<: ক্যালকুলাস

ভিত্তি সিস্টেম F^q<: ক্যালকুলাস প্রসারিত করে, অন্তর্ভুক্ত:

  • অ-শব্দার্থিক ছায়া অ্যারেনা: রেফারেন্স তাদের শব্দার্থিক সুযোগ থেকে পালাতে সমর্থন করে
  • সহ-বরাদ্দ সিনট্যাক্স: ref t1 at t2 নতুন রেফারেন্স বিদ্যমান অ্যারেনায় রাখে
  • একীভূত রেফারেন্স টাইপ: সমস্ত বরাদ্দ ফর্ম Ref[T]^q টাইপ ভাগ করে

{A}^q<: ক্যালকুলাস

সুযোগ সম্পদ ব্যবস্থাপনা যোগ করতে A^q<: প্রসারিত করে:

  • সুযোগ বরাদ্দ: ref t as x in b শব্দার্থিক সীমাবদ্ধ রেফারেন্স তৈরি করে
  • প্রবাহ-অসংবেদনশীল যুক্তি: গতিশীল ট্র্যাকিং স্থানীয় অবস্থানের মাধ্যমে নিরাপদ রিলিজ নিশ্চিত করে
  • বাল্ক রিলিজ: সুযোগ শেষে স্বয়ংক্রিয়ভাবে সম্পূর্ণ অ্যারেনা রিলিজ করে

প্রযুক্তিগত উদ্ভাবন পয়েন্ট

१. টেলিস্কোপ কাঠামোর শিথিলকরণ: মোটা-দানাদার ট্র্যাকিং অ্যারেনার মধ্যে এবং অ্যারেনা জুড়ে চক্রাকার কাঠামো অনুমতি দেয় २. একীভূত টাইপ বিমূর্ততা: প্রথম এবং দ্বিতীয় শ্রেণীর সম্পদের মধ্যে টাইপ পার্থক্য দূর করে ३. নির্বাচনী স্ট্যাক শৃঙ্খলা: প্রবাহ-অসংবেদনশীল যুক্তি বজায় রেখে পূর্বাভাসযোগ্য রিলিজ প্রদান করে

পরীক্ষামূলক সেটআপ

আনুষ্ঠানিক যাচাইকরণ

  • যান্ত্রিক প্রমাণ: সমস্ত আনুষ্ঠানিক ফলাফল Rocq-এ যান্ত্রিক
  • টাইপ নিরাপত্তা: অগ্রগতি এবং সংরক্ষণ উপপাদ্য প্রমাণ করা হয়েছে
  • মেমরি নিরাপত্তা: ব্যবহার-পরবর্তী-মুক্তি ত্রুটি নিশ্চিত করে

কেস স্টাডি

পেপার তিনটি কেস স্টাডির মাধ্যমে সিস্টেম প্রকাশনীয়তা যাচাই করে:

१. কলব্যাক নিবন্ধন: অ-শব্দার্থিক অ্যারেনা কীভাবে ইভেন্ট-চালিত প্রোগ্রামিং প্যাটার্ন সমর্থন করে তা প্রদর্শন করে २. সাধারণ অনির্দিষ্ট পয়েন্ট সংমিশ্রক: সিস্টেম পূর্ববর্তী পৌঁছানোযোগ্যতা টাইপের সীমাবদ্ধতা অতিক্রম করে প্রমাণ করে ३. চক্রাকার সংরক্ষণ কাঠামো: বহু-হপ চক্র নিরাপদে নির্মাণ এবং পুনর্ব্যবহার করার ক্ষমতা প্রদর্শন করে

পরীক্ষামূলক ফলাফল

প্রধান ফলাফল

টাইপ নিরাপত্তা প্রমাণ

উপপাদ্য ४.१ (অগ্রগতি): যদি [∅ | Σ] φ ⊢ t : Q এবং Σ ok,
তাহলে t একটি মান বা ∃ t'、σ' যেমন t | σ → t' | σ'

উপপাদ্য ४.२ (সংরক্ষণ): যদি টাইপ-ভালো পদ হ্রাস পায়,
তাহলে ∃ প্রসারিত টাইপ পরিবেশ যেমন হ্রাস ফলাফল এখনও টাইপ-ভালো

প্রকাশনীয়তা উন্নতি

বিদ্যমান সিস্টেমের সাথে তুলনা দেখায় এই সিস্টেম নিম্নলিখিত বৈশিষ্ট্যের ছেদ অর্জন করে:

  • ✓ স্ট্যাক শৃঙ্খলা
  • ✓ প্রকাশনীয় ভাগাভাগি
  • ✓ প্রথম-শ্রেণীর সম্পদ
  • ✓ উচ্চতর-ক্রম কার্যকারিতা

এটি একটি একীভূত সিস্টেমে এই সমস্ত বৈশিষ্ট্য বাস্তবায়নকারী প্রথম কাজ।

কেস বিশ্লেষণ

কলব্যাক নিবন্ধন প্যাটার্ন

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}

চক্রাকার রেফারেন্স কাঠামো নিরাপদে নির্মাণ এবং রিলিজ করা প্রদর্শন করে।

সম্পর্কিত কাজ

অঞ্চল/অ্যারেনা সিস্টেম

  • MLKit: কার্যকরী ভাষায় অন্তর্নিহিত অঞ্চল ব্যবস্থাপনা
  • Cyclone: C-শৈলী ভাষায় স্পষ্ট অঞ্চল এবং অস্তিত্ব প্রকার
  • রৈখিক অঞ্চল: রৈখিক টাইপ এবং অঞ্চল ধারণা সংমিশ্রণ

মালিকানা এবং রৈখিক টাইপ

  • Rust: অনন্য মালিকানা এবং একক পরিবর্তনশীল অ্যাক্সেস পথ
  • Pony: অন্তর্নিহিত অঞ্চল এবং ভগ্নাংশ ক্ষমতা
  • Vergio: মালিকানা এবং স্পষ্ট অঞ্চল সংমিশ্রণ

পৌঁছানোযোগ্যতা টাইপ

  • F^q<:: বহুরূপী পৌঁছানোযোগ্যতা টাইপ সিস্টেম
  • λ^◦: স্ব-চক্র সমর্থন করে এমন সম্প্রসারণ
  • ক্যাপচার টাইপ: Scala-তে প্রভাব নিরাপত্তা সিস্টেম

উপসংহার এবং আলোচনা

প্রধান উপসংহার

পেপার সফলভাবে পৌঁছানোযোগ্যতা টাইপ, অ্যারেনা-ভিত্তিক সম্পদ ব্যবস্থাপনা এবং স্ট্যাক শৃঙ্খলা একীভূত করে, উচ্চতর-ক্রম ভাষায় নিরাপদ সম্পদ ব্যবস্থাপনার জন্য একটি হালকা এবং প্রকাশনীয় ভিত্তি প্রদান করে।

সীমাবদ্ধতা

१. চক্রাকার নির্মাণ সীমাবদ্ধতা: যদিও চক্রাকার কাঠামো সমর্থন করে, কমপক্ষে দুটি ইউনিট প্রয়োজন २. প্রবাহ-সংবেদনশীল সম্প্রসারণ: স্পষ্ট রিলিজ এখনও অতিরিক্ত প্রবাহ-সংবেদনশীল প্রভাব সম্প্রসারণ প্রয়োজন ३. বাস্তবায়ন জটিলতা: দ্বি-মাত্রিক সংরক্ষণ মডেল রানটাইম বাস্তবায়নের জটিলতা বৃদ্ধি করে

ভবিষ্যত দিকনির্দেশনা

१. কর্মক্ষমতা অপ্টিমাইজেশন: দ্বি-মাত্রিক সংরক্ষণ মডেলের দক্ষ বাস্তবায়ন গবেষণা করা २. সমসাময়িক সম্প্রসারণ: সিস্টেম সমসাময়িক সেটিংসে প্রসারিত করা ३. ব্যবহারিক ভাষা একীকরণ: প্রকৃত প্রোগ্রামিং ভাষায় সিস্টেম বাস্তবায়ন করা

গভীর মূল্যায়ন

শক্তি

१. তাত্ত্বিক অবদান উল্লেখযোগ্য: একটি একীভূত সিস্টেমে স্ট্যাক শৃঙ্খলা, প্রকাশনীয় ভাগাভাগি, প্রথম-শ্রেণীর সম্পদ এবং উচ্চতর-ক্রম কার্যকারিতার ছেদ বাস্তবায়নকারী প্রথম २. প্রযুক্তিগত উদ্ভাবন বিশিষ্ট: ছায়া অ্যারেনা এবং মোটা-দানাদার পৌঁছানোযোগ্যতা ট্র্যাকিং গুরুত্বপূর্ণ উদ্ভাবন ३. আনুষ্ঠানিক কঠোরতা: সম্পূর্ণ যান্ত্রিক প্রমাণ ফলাফলের বিশ্বাসযোগ্যতা বৃদ্ধি করে ४. প্রকাশনীয়তা উন্নতি: পূর্ববর্তী পৌঁছানোযোগ্যতা টাইপ সিস্টেমের টেলিস্কোপ কাঠামো সীমাবদ্ধতা অতিক্রম করে

অপূর্ণতা

१. ব্যবহারিক প্রয়োগ সীমিত: এখনও প্রকৃত ভাষায় বাস্তবায়িত নয়, ব্যবহারিক মূল্য যাচাই করা বাকি २. কর্মক্ষমতা বিবেচনা অপর্যাপ্ত: দ্বি-মাত্রিক সংরক্ষণ মডেলের কর্মক্ষমতা প্রভাবের বিশ্লেষণ অভাব ३. শেখার বক্ররেখা খাড়া: সিস্টেম জটিলতা প্রোগ্রামার গ্রহণকে প্রভাবিত করতে পারে

প্রভাব

এই কাজ প্রোগ্রামিং ভাষা তত্ত্ব ক্ষেত্রে গুরুত্বপূর্ণ, সম্পদ ব্যবস্থাপনার জন্য নতুন তাত্ত্বিক ভিত্তি প্রদান করে, ভবিষ্যত প্রোগ্রামিং ভাষা ডিজাইনকে প্রভাবিত করতে পারে। বিশেষত নির্ভুল সম্পদ নিয়ন্ত্রণ প্রয়োজন এমন সিস্টেম প্রোগ্রামিং ক্ষেত্রের জন্য, এই পদ্ধতি নতুন সম্ভাবনা প্রদান করে।

প্রযোজ্য পরিস্থিতি

१. সিস্টেম প্রোগ্রামিং: নির্ভুল মেমরি ব্যবস্থাপনা প্রয়োজন এমন নিম্ন-স্তরের সিস্টেম २. এম্বেডেড সিস্টেম: সম্পদ-সীমিত পরিবেশে নিরাপদ প্রোগ্রামিং ३. কার্যকরী ভাষা: সম্পদ ব্যবস্থাপনা ক্ষমতা প্রয়োজন এমন উচ্চতর-ক্রম কার্যকরী ভাষা ४. সমসাময়িক সিস্টেম: মাল্টি-থ্রেড পরিবেশে নিরাপদ সম্পদ ভাগাভাগি

সংদর্ভ

পেপার প্রোগ্রামিং ভাষা তত্ত্ব ক্ষেত্রের গুরুত্বপূর্ণ কাজ উদ্ধৃত করে, যার মধ্যে রয়েছে:

  • Grossman et al. 2002: Cyclone অঞ্চল সিস্টেম
  • Tofte et al. 2001: MLKit অঞ্চল অনুমান
  • Wei et al. 2024: বহুরূপী পৌঁছানোযোগ্যতা টাইপ
  • Clarke et al. 2013: Rust মালিকানা টাইপ
  • Bao et al. 2021: পৌঁছানোযোগ্যতা টাইপ ভিত্তি তত্ত্ব