paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Prioritise the Best Variation

优先化最佳变体
LMCS vol.Volume 19, Issue 42023匹配度 2/10 · 该论文是纯 PL/类型论工作,研究通道会话类型、优先级与死锁自由,未涉及 LLM/Agent、静态分析在 ML/Agentic 程序中的应用、浮点程序分析或贝叶斯程序分析,与用户画像的核心交叉方向无直接关联。引用 5 inbox
Wen Kokke, Ornela Dardha
crossref: 2026-09-10

AI 速览

一句话:提出 Priority GV,将通道创建与线程生成解耦,用优先级类型系统恢复环状进程的死锁自由,并给出 PCP 编码。

二元会话类型可保证通信安全与会话保真,但无法排除不同会话交错导致的死锁。经典进程 CP 与 Good Variation(GV)通过把通道创建与并行/线程生成绑定在同一逻辑规则或 fork 操作中保证无死锁,代价是只允许树状结构进程。本文提出 Priority GV(PGV),将通道创建与线程生成解耦,并借鉴 Priority CP 用优先级对环状结构进程进行类型化,从而恢复死锁自由。作者证明类型系统可靠,包括 subject reduction 与 progress,并定义从 PCP 到 PGV 的编码,证明该编码保持类型化,且相对于操作语义既可靠又完备。

问题
二元会话类型无法排除不同会话交错产生的死锁;CP 与 GV 虽通过绑定通道创建与线程生成保证无死锁,但只允许树状结构进程,牺牲了表达力。
方法
提出 Priority GV:把通道创建与线程生成解耦,借鉴 Priority CP 引入优先级来类型化环状进程;定义从 PCP 到 PGV 的编码。
评估
通过证明 subject reduction 与 progress 说明类型系统可靠,并证明 PCP 到 PGV 编码保持类型化且对操作语义可靠、完备。
原文摘要(Abstract)

Binary session types guarantee communication safety and session fidelity, but alone they cannot rule out deadlocks arising from the interleaving of different sessions. In Classical Processes (CP)$-$a process calculus based on classical linear logic$-$deadlock freedom is guaranteed by combining channel creation and parallel composition under the same logical cut rule. Similarly, in Good Variation (GV)$-$a linear concurrent $\lambda$-calculus$-$deadlock freedom is guaranteed by combining channel creation and thread spawning under the same operation, called fork. In both CP and GV, deadlock freedom is achieved at the expense of expressivity, as the only processes allowed are tree-structured. Dardha and Gay define Priority CP (PCP), which allows cyclic-structured processes and restores deadlock freedom by using priorities, in line with Kobayashi and Padovani. Following PCP, we present Priority GV (PGV), a variant of GV which decouples channel creation from thread spawning. Consequently, we type cyclic-structured processes and restore deadlock freedom by using priorities. We show that our type system is sound by proving subject reduction and progress. We define an encoding from PCP to PGV and prove that the encoding preserves typing and is sound and complete with respect to the operational semantics.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2166,
  title = {Prioritise the Best Variation},
  author = {Wen Kokke and Ornela Dardha},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 19, Issue 4},
  year = {2023},
  doi = {10.46298/lmcs-19(4:28)2023}
}