2025-11-19T09:28:13.762419

Typestate via Revocable Capabilities

Jia, Liu, He et al.

Managing stateful resources safely and expressively is a longstanding challenge in programming languages, especially in the presence of aliasing. While scope-based constructs such as Java's synchronized blocks offer ease of reasoning, they restrict expressiveness and parallelism. Conversely, imperative, flow-sensitive management enables fine-grained control but demands sophisticated typestate analyses and often burdens programmers with explicit state tracking. In this work, we present a novel approach that unifies the strengths of both paradigms by extending flow-insensitive capability mechanisms into flow-sensitive typestate tracking. Our system decouples capability lifetimes from lexical scopes, allowing functions to provide, revoke, and return capabilities in a flow-sensitive manner, based on the existing mechanisms explored for the safety and ergonomics of scoped capability programming. We implement our approach as an extension to the Scala 3 compiler, leveraging path-dependent types and implicit resolution to enable concise, statically safe, and expressive typestate programming. Our prototype generically supports a wide range of stateful patterns, including file operations, advanced locking protocols, DOM construction, and session types. This work demonstrates that expressive and safe typestate management can be achieved with minimal extensions to existing capability-based languages, paving the way for more robust and ergonomic stateful programming.

academic

পুনরুদ্ধারযোগ্য ক্ষমতার মাধ্যমে টাইপস্টেট

মৌলিক তথ্য

পেপার আইডি: 2510.08889
শিরোনাম: Typestate via Revocable Capabilities
লেখক: Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, Tiark Rompf (Purdue University & Augusta University)
শ্রেণীবিভাগ: cs.PL (প্রোগ্রামিং ভাষা)
প্রকাশনার সময়: ২০২৫ সালের ১০ অক্টোবর (arXiv প্রি-প্রিন্ট)
পেপার লিঙ্ক: https://arxiv.org/abs/2510.08889

সারসংক্ষেপ

এই পেপারটি পুনরুদ্ধারযোগ্য ক্ষমতা (revocable capabilities) এর মাধ্যমে টাইপস্টেট (typestate) ট্র্যাকিং বাস্তবায়নের একটি নতুন পদ্ধতি প্রস্তাব করে। এই পদ্ধতিটি স্কোপ-ভিত্তিক নিরাপত্তা এবং আদেশমূলক প্রবাহ-সংবেদনশীল ব্যবস্থাপনার প্রকাশনীয়তাকে একীভূত করে, প্রবাহ-অসংবেদনশীল ক্ষমতা প্রক্রিয়াকে প্রবাহ-সংবেদনশীল টাইপস্টেট ট্র্যাকিংয়ে প্রসারিত করে অবস্থা সম্পদ ব্যবস্থাপনার দীর্ঘস্থায়ী চ্যালেঞ্জ সমাধান করে। সিস্টেমটি ক্ষমতা জীবনচক্র এবং শব্দভাণ্ডার স্কোপকে বিচ্ছিন্ন করে, ফাংশনগুলিকে প্রবাহ-সংবেদনশীল উপায়ে ক্ষমতা প্রদান, পুনরুদ্ধার এবং প্রত্যাবর্তন করতে অনুমতি দেয়। লেখকরা Scala 3 কম্পাইলারে এই পদ্ধতিটি বাস্তবায়ন করেছেন, পথ-নির্ভর প্রকার এবং অন্তর্নিহিত সমাধান ব্যবহার করে সংক্ষিপ্ত, স্ট্যাটিকভাবে নিরাপদ এবং সমৃদ্ধ প্রকাশনীয় টাইপস্টেট প্রোগ্রামিং বাস্তবায়ন করেছেন।

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

মূল সমস্যা

অবস্থা সম্পদ ব্যবস্থাপনার দ্বিধা:
- স্কোপ-ভিত্তিক নির্মাণ (যেমন Java এর synchronized ব্লক) যুক্তি করা সহজ কিন্তু প্রকাশনীয়তা এবং সমান্তরালতা সীমাবদ্ধ করে
- আদেশমূলক প্রবাহ-সংবেদনশীল ব্যবস্থাপনা সূক্ষ্ম-দানাদার নিয়ন্ত্রণ প্রদান করে কিন্তু জটিল টাইপস্টেট বিশ্লেষণ প্রয়োজন
বিদ্যমান পদ্ধতির সীমাবদ্ধতা:
- স্কোপ পদ্ধতি LIFO (শেষে আসা প্রথমে যাওয়া) জীবনচক্র জোরপূর্বক করে, অপ্টিমাইজেশন বাধা দেয়
- প্রবাহ-সংবেদনশীল পদ্ধতি জটিল উপনাম ট্র্যাকিং এবং স্পষ্ট অবস্থা ব্যবস্থাপনা প্রয়োজন
- নিরাপত্তা এবং প্রকাশনীয়তার একীভূত নিশ্চয়তার অভাব
গবেষণা প্রেরণা:
- এমন একটি পদ্ধতির প্রয়োজন যা স্কোপ যুক্তির সরলতা বজায় রেখে আদেশমূলক ব্যবস্থাপনার প্রকাশনীয়তা প্রদান করে
- উপনাম উপস্থিতিতে নিরাপদ অবস্থা সম্পদ ব্যবস্থাপনা বাস্তবায়ন করা
- বিদ্যমান ক্ষমতা-ভিত্তিক ভাষায় টাইপস্টেট সমর্থনের জন্য ন্যূনতম সম্প্রসারণ প্রদান করা

মূল অবদান

পুনরুদ্ধারযোগ্য ক্ষমতা প্রক্রিয়া প্রস্তাব:
- প্রবাহ-অসংবেদনশীল ক্ষমতা সিস্টেমকে প্রবাহ-সংবেদনশীল টাইপস্টেট ট্র্যাকিং সমর্থন করার জন্য সম্প্রসারিত করা
তিনটি মূল প্রযুক্তিগত স্তম্ভ:
- প্রবাহ-সংবেদনশীল বিনাশকারী প্রভাব সিস্টেম (destructive effect system)
- পথ-নির্ভর প্রকার-ভিত্তিক ক্ষমতা-বস্তু পরিচয় সংযোগ
- প্রকার-নির্দেশিত ANF রূপান্তর অন্তর্নিহিত ক্ষমতা ব্যবস্থাপনা বাস্তবায়নের জন্য
সম্পূর্ণ Scala 3 প্রোটোটাইপ বাস্তবায়ন:
- Scala 3 কম্পাইলার প্রসারিত করা, একাধিক অবস্থা প্যাটার্ন সমর্থন করা
ব্যাপক প্রয়োগ যাচাইকরণ:
- ফাইল অপারেশন, উন্নত লক প্রোটোকল, DOM নির্মাণ, সেশন প্রকার ইত্যাদি একাধিক ক্ষেত্রে কেস স্টাডি

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

কাজের সংজ্ঞা

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

সম্পদ ব্যবহারের নিরাপত্তা স্ট্যাটিকভাবে নিশ্চিত করা
নমনীয় অ-LIFO সম্পদ জীবনচক্র ব্যবস্থাপনা সমর্থন করা
স্পষ্ট অবস্থা ট্র্যাকিং বোঝা এড়ানো

পদ্ধতি স্থাপত্য

1. প্রবাহ-সংবেদনশীল ক্ষমতা পুনরুদ্ধার প্রক্রিয়া

বিনাশকারী প্রভাব সিস্টেম:

def close(f: OpenFile^): ClosedFile^ @kill(f) = ...

@kill(f) টীকা ব্যবহার করে ফাংশন যা পরামিতি f এর ক্ষমতা পুনরুদ্ধার করে তা চিহ্নিত করা
মৃত চলক {k: ...} এর সংগৃহীত সেট বজায় রাখা
ট্রানজিটিভ বিচ্ছিন্নতা পরীক্ষার মাধ্যমে পুনরুদ্ধৃত ক্ষমতার ব্যবহার প্রতিরোধ করা

তীর প্রকার স্বরলিপি:

=!>: পরামিতি পুনরুদ্ধার করে এমন তীর প্রকার
?=!>: অন্তর্নিহিত পুনরুদ্ধার তীর প্রকার
?<=>: অন্তর্নিহিত রিটার্ন তীর প্রকার
?=!>?: সমন্বিত তীর, গ্রহণ-পুনরুদ্ধার-রিটার্নের সম্পূর্ণ অবস্থা রূপান্তর প্রকাশ করে

2. পথ-নির্ভর ক্ষমতা

সমস্যা: ঐতিহ্যবাহী পদ্ধতি একই বস্তুতে অবস্থা রূপান্তর অপারেশন নিশ্চিত করতে পারে না

সমাধান: পথ-নির্ভর প্রকার ব্যবহার করে ক্ষমতা বস্তু পরিচয়ের সাথে সংযুক্ত করা

class File:
  type IsClosed  // বিমূর্ত প্রকার সদস্য
  type IsOpen

def openDep(f: File, c: f.IsClosed^): f.IsOpen^ @kill(c) = ...

Σ প্রকার সমর্থন: নির্ভর জোড় (dependent pairs) ব্যবহার করে একসাথে সম্পদ এবং ক্ষমতা রিটার্ন করা

trait Sigma:
  type A
  type B
  val a: A  
  val b: B

def newFile(name: String): Sigma { type A = File; type B = a.IsClosed^ } = ...

3. অন্তর্নিহিত ক্ষমতা ব্যবস্থাপনা

প্রকার-নির্দেশিত ANF রূপান্তর:

Sigma প্রকার ধারণকারী অভিব্যক্তি স্বয়ংক্রিয়ভাবে পুনর্গঠন করা
প্রথম ক্ষেত্র নিষ্কাশন এবং একক প্রকার নির্ধারণ করা
দ্বিতীয় ক্ষেত্রকে অন্তর্নিহিত প্রার্থী হিসাবে ঘোষণা করা

অন্তর্নিহিত Σ উন্নয়ন:

স্বয়ংক্রিয়ভাবে রিটার্ন মান Sigma জোড়ের প্রথম ক্ষেত্রে উন্নীত করা
অন্তর্নিহিত আহ্বানের মাধ্যমে দ্বিতীয় ক্ষেত্রের ক্ষমতা পূরণ করা

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

ক্ষমতা জীবনচক্র এবং শব্দভাণ্ডার স্কোপের বিচ্ছিন্নতা:
- ঐতিহ্যবাহী LIFO সীমাবদ্ধতা অতিক্রম করা, নমনীয় সম্পদ ব্যবস্থাপনা প্যাটার্ন সমর্থন করা
পৌঁছানো-যোগ্যতা প্রকার-ভিত্তিক উপনাম ট্র্যাকিং:
- চলক সম্ভবত ক্যাপচার করতে পারে এমন সম্পদ over-approximate করতে সীমাবদ্ধ সেট ব্যবহার করা
- ট্রানজিটিভ বিচ্ছিন্নতা পরীক্ষা নিরাপত্তা নিশ্চিত করা: fC* ∩ k* = ∅
ন্যূনতম সম্প্রসারণ নীতি:
- বিদ্যমান ক্ষমতা সিস্টেমের উপর ভিত্তি করে টাইপস্টেট ট্র্যাকিং বাস্তবায়নের জন্য ন্যূনতম ভাষা বৈশিষ্ট্য যোগ করা

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

বাস্তবায়ন প্ল্যাটফর্ম

ভিত্তি: Scala 3 কম্পাইলারের শাখা বাস্তবায়ন
অবকাঠামো পুনর্ব্যবহার: ক্যাপচারিং প্রকার (capturing types) এর বিদ্যমান বাস্তবায়ন
মূল সম্প্রসারণ: বিনাশকারী প্রভাব চেকার + প্রকার-নির্দেশিত ANF রূপান্তর

মূল্যায়ন পদ্ধতি

এই পেপারটি ঐতিহ্যবাহী কর্মক্ষমতা বেঞ্চমার্কের পরিবর্তে কেস স্টাডি পদ্ধতি ব্যবহার করে সিস্টেমের প্রকাশনীয়তা এবং ব্যবহারিকতা যাচাই করে।

তুলনা ভিত্তিরেখা

ঐতিহ্যবাহী স্কোপ পদ্ধতি (যেমন Java synchronized ব্লক)
বিদ্যমান টাইপস্টেট সিস্টেম (যেমন Plaid)
সেশন প্রকার বাস্তবায়ন
রৈখিক প্রকার সিস্টেম

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

প্রধান কেস স্টাডি

1. ফাইল অপারেশন

val f = newFile("a.txt")
val fOpen = open(f)
write(fOpen, "Hello")
val fClosed = close(fOpen)
// write(fOpen, "World")  // সংকলন ত্রুটি: পুনরুদ্ধৃত ক্ষমতা ব্যবহার

যাচাইকরণ ফলাফল:

পুরানো ক্ষমতার ব্যবহার স্ট্যাটিকভাবে সনাক্ত করা
অ-LIFO সম্পদ জীবনচক্র সমর্থন করা
সম্পদ পরিচয়ের সংযোগ বজায় রাখা

2. হ্যান্ড-টু-হ্যান্ড লক প্রোটোকল

পেপারের শুরুতে উল্লেখ করা ডাটাবেস লেনদেন অপ্টিমাইজেশন দৃশ্য বাস্তবায়ন করা:

table.lock()
val row = locateRow(table)  
table.lockRow(row)
table.unlock()  // টেবিল লক প্রাথমিক রিলিজ
val result = computeOnRow(row)
row.unlock()

সুবিধা: নেস্টেড synchronized ব্লকের তুলনায়, টেবিল লকের প্রাথমিক রিলিজ অনুমতি দেয়, সমান্তরালতা উন্নত করে।

3. DOM গাছ নির্মাণ

প্রসঙ্গ-মুক্ত ব্যাকরণের টাইপস্টেট ট্র্যাকিং সমর্থন করা:

makeDom { tree =>
  tree.open(DIV())
  tree.open(P())
  tree.close(P())
  tree.close(DIV())
  // tree.close(DIV())  // ত্রুটি: অবস্থা Nil এবং (DIV, ...) নয়
}

4. সেশন প্রকার

দ্বিপক্ষীয় সেশন প্রকার বাস্তবায়ন করা, প্রোটোকল পুনরাবৃত্তি সমর্থন করা:

def echoServer(chan: Chan): chan.PCap[EmptyTuple, EchoServer] ?=!> Unit = {
  chan.recPush()
  // ... প্রোটোকল বাস্তবায়ন
}

পরীক্ষামূলক আবিষ্কার

প্রকাশনীয়তা যাচাইকরণ: একাধিক জটিল অবস্থা ব্যবস্থাপনা প্যাটার্ন সফলভাবে বাস্তবায়ন করা
নিরাপত্তা নিশ্চয়তা: বিভিন্ন ত্রুটিপূর্ণ ব্যবহার প্যাটার্ন সংকলন সময়ে সনাক্ত করা
মানব-কম্পিউটার ইন্টারঅ্যাকশন: অন্তর্নিহিত সমাধানের মাধ্যমে বয়লারপ্লেট কোড উল্লেখযোগ্যভাবে হ্রাস করা
ন্যূনতম আক্রমণাত্মকতা: বিদ্যমান Scala কোডের সাথে ভাল সামঞ্জস্যতা

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

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

একীকরণ অর্জন: স্কোপ নিরাপত্তা এবং আদেশমূলক প্রকাশনীয়তা সফলভাবে একীভূত করা
ন্যূনতম সম্প্রসারণ নীতি: বিদ্যমান ক্ষমতা সিস্টেমে অল্প বৈশিষ্ট্য যোগ করে শক্তিশালী টাইপস্টেট ট্র্যাকিং বাস্তবায়ন সম্ভব প্রমাণ করা
ব্যবহারিকতা যাচাইকরণ: একাধিক বাস্তব দৃশ্যের মাধ্যমে পদ্ধতির সম্ভাব্যতা এবং প্রকাশনীয়তা যাচাই করা

সীমাবদ্ধতা

Σ প্রকারের সীমাবদ্ধতা:
- তাৎক্ষণিক আনপ্যাকিং প্রয়োজন, ডেটা কাঠামোতে স্থায়ী সংরক্ষণ সমর্থন করে না
- নির্ভর প্রকার সমর্থনের অসম্পূর্ণতা
বাস্তবায়ন সীমাবদ্ধতা:
- বর্তমান প্রোটোটাইপ পরিবর্তনশীল চলক এবং বস্তু ক্ষেত্রের বিনাশকারী প্রভাব সমর্থন করে না
- Scala জেনেরিক্সের সাথে সম্পূর্ণ একীকরণ এখনও সীমাবদ্ধ
আনুষ্ঠানিক ফাঁক:
- Σ প্রকার পৌঁছানো-যোগ্যতা প্রকারে সরাসরি প্রতিনিধিত্ব নেই
- CPS রূপান্তরের আনুষ্ঠানিক প্রক্রিয়াকরণ প্রয়োজন

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

সম্পূর্ণ নির্ভর প্রকার সমর্থন: সম্পূর্ণ নির্ভর প্রকার সিস্টেমে প্রসারিত করা
আরও বিস্তৃত ভাষা সমর্থন: ক্ষমতা সমর্থনকারী অন্যান্য ভাষায় স্থানান্তর করা
অপ্টিমাইজেশন এবং সরঞ্জাম: কম্পাইলার অপ্টিমাইজেশন এবং ডিবাগিং সরঞ্জাম উন্নয়ন
তাত্ত্বিক পরিমার্জন: আনুষ্ঠানিক মডেলের আরও পরিমার্জন

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

শক্তি

তাত্ত্বিক উদ্ভাবনী:
- প্রথমবারের মতো প্রবাহ-অসংবেদনশীল ক্ষমতা প্রক্রিয়া সফলভাবে প্রবাহ-সংবেদনশীল টাইপস্টেট ট্র্যাকিংয়ে প্রসারিত করা
- তিনটি প্রযুক্তিগত স্তম্ভের জৈব সমন্বয় মূল উদ্ভাবনী
ব্যবহারিক মূল্য:
- প্রকৃত প্রোগ্রামিংয়ে গুরুত্বপূর্ণ সমস্যা সমাধান করা
- বিদ্যমান ভাষার ক্রমবর্ধমান আপগ্রেড পথ প্রদান করা
পরীক্ষা সম্পূর্ণতা:
- একাধিক জটিল কেস স্টাডি পদ্ধতির প্রকাশনীয়তা যাচাই করা
- সাধারণ ফাইল অপারেশন থেকে জটিল সেশন প্রকার পর্যন্ত বিস্তৃত পরিস্থিতি কভার করা
প্রকৌশল গুণমান:
- সম্পূর্ণ Scala 3 কম্পাইলার বাস্তবায়ন
- বিদ্যমান capture checker এর সাথে ভাল একীকরণ

অপূর্ণতা

তাত্ত্বিক ভিত্তির অসম্পূর্ণতা:
- Σ প্রকারের আনুষ্ঠানিক প্রক্রিয়াকরণ যথেষ্ট কঠোর নয়
- বিদ্যমান পৌঁছানো-যোগ্যতা প্রকার তত্ত্বের সাথে একীকরণে ফাঁক রয়েছে
বাস্তবায়ন সীমাবদ্ধতা:
- পরিবর্তনশীল অবস্থার সমর্থন অসম্পূর্ণ
- জেনেরিক সমর্থনের সীমাবদ্ধতা ব্যবহারিকতা প্রভাবিত করতে পারে
মূল্যায়ন পদ্ধতির সীমাবদ্ধতা:
- কর্মক্ষমতা মূল্যায়ন অনুপস্থিত
- বড় আকারের কোড বেসের যাচাইকরণ নেই
শিক্ষণীয়তা সমস্যা:
- ধারণা জটিলতা উচ্চ, গ্রহণকে প্রভাবিত করতে পারে
- ত্রুটি বার্তার বন্ধুত্ব যথেষ্ট আলোচনা করা হয়নি

প্রভাব

একাডেমিক অবদান:
- টাইপস্টেট গবেষণার জন্য নতুন দিকনির্দেশনা খোলা
- ক্ষমতা সিস্টেমের সম্প্রসারণ সম্ভাবনা প্রদর্শন করা
ব্যবহারিক প্রভাব:
- Scala ইকোসিস্টেমের জন্য মূল্যবান সম্প্রসারণ প্রদান করা
- অন্যান্য ভাষার ডিজাইন প্রভাবিত করতে পারে
পুনরুৎপাদনযোগ্যতা:
- সম্পূর্ণ বাস্তবায়ন প্রদান করা
- কেস কোড সংকলন এবং চালানো যায়

প্রযোজ্য দৃশ্য

সিস্টেম প্রোগ্রামিং: নির্ভুল সম্পদ ব্যবস্থাপনা প্রয়োজনীয় দৃশ্য
সমসাময়িক প্রোগ্রামিং: জটিল লক প্রোটোকল বাস্তবায়ন
প্রোটোকল বাস্তবায়ন: নেটওয়ার্ক প্রোটোকল এবং যোগাযোগ প্রোটোকল
DSL ডিজাইন: অবস্থা ট্র্যাকিং প্রয়োজনীয় ডোমেইন-নির্দিষ্ট ভাষা

তথ্যসূত্র

পেপারটি সমৃদ্ধ সম্পর্কিত কাজ উদ্ধৃত করে, প্রধানত অন্তর্ভুক্ত:

টাইপস্টেট ভিত্তি: Strom এবং Yemini (1986) - টাইপস্টেট ধারণার ভিত্তি কাজ
ক্ষমতা সিস্টেম: Dennis এবং Horn (1966), Miller এবং Shapiro (2003) - ক্ষমতা ধারণার তাত্ত্বিক ভিত্তি
পৌঁছানো-যোগ্যতা প্রকার: Bao ইত্যাদি (2021), Wei ইত্যাদি (2024) - এই কাজের সরাসরি তাত্ত্বিক ভিত্তি
Scala প্রকার সিস্টেম: Amin ইত্যাদি (2016) - DOT ক্যালকুলাস এবং পথ-নির্ভর প্রকার
সেশন প্রকার: Honda (1993), Takeuchi ইত্যাদি (1994) - সেশন প্রকারের তাত্ত্বিক ভিত্তি

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