paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom

假设恰好足够的公平性使会话类型对无锁性完备
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 1/10 · 该论文属于纯 PL/类型论与并发理论工作,研究会话类型、公平性假设与无锁性完备性,不涉及 LLM/Agent、静态分析在 ML 系统中的应用,也不涉及浮点或贝叶斯程序分析。虽然与形式化验证/类型系统相关,但未与用户当前关注的 AI 交叉方向产生直接联系。引用 4 inbox
Rob van Glabbeek, Peter Hofner, Ross Horne
crossref: 2026-09-12

AI 速览

一句话:系统刻画公平性假设下的三种无锁性语义,并给出仅假设 justness 时完备的会话类型系统。

会话类型系统常以无锁性等活性性质为目标,但此类结论高度依赖对并发执行路径的公平性假设。本文在一个最小会话演算上系统考察所有已知公平性假设,精确识别出三种语义上互异、且各自都有可靠(sound)会话类型系统的无锁性概念。随后,作者在标准全局会话类型方法中引入一个通用 merge 算子,得到对其中最强概念完备(complete)的会话类型系统,而该概念仅假设执行路径的 justness,即并发系统中最弱的公平性假设。该工作厘清了公平性假设与无锁性语义之间的关系,并在如此弱的公平性前提下首次实现会话类型的完备性。

问题
不同公平性假设如何影响会话类型系统关于无锁性(lock-freedom)的结论尚不清晰。
方法
固定一个最小会话演算,系统枚举已知公平性假设,识别出三种语义不同的无锁性概念,并在标准全局会话类型方法中引入通用 merge 算子。
评估
通过形式化证明进行论证:三种无锁性概念各存在可靠的会话类型系统,且带 merge 算子的新系统对最强概念(仅假设 justness)完备。
原文摘要(Abstract)

We investigate how different fairness assumptions affect results concerning lock-freedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lock-freedom, all of which having a sound session type system. We then show that, by using a general merge operator in an otherwise standard approach to global session types, we obtain a session type system complete for the strongest amongst those notions of lock-freedom, which assumes only justness of execution paths, a minimal fairness assumption for concurrent systems.

链接与引用

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

BibTeX
@inproceedings{paperbot6169,
  title = {Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom},
  author = {Rob van Glabbeek and Peter Hofner and Ross Horne},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470531}
}