paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Competitive parallelism: getting your priorities right

竞争式并行:正确设置优先级
ICFP 2(ICFP)2018匹配度 2/10 · 论文研究并发/并行程序的模态类型系统与成本模型,属于纯 PL 形式化与类型系统工作,未涉及机器学习系统、Agentic/LLM 程序、浮点程序分析或贝叶斯程序分析。仅与静态分析/形式化方法有间接关联,与用户当前核心的 PL×AI 交叉方向匹配度很低。引用 15 inbox
Stefan K. Muller, Umut A. Acar, Robert Harper
crossref: 2026-09-10

AI 速览

一句话:提出模态类型系统与成本模型,统一协作式与竞争式并行,静态防止优先级反转。

多线程程序传统上分为协作式与竞争式两类,前者提升计算吞吐,后者提升交互响应性,但两者长期分离。随着多核普及,混合交互与计算的应用需要统一这两类线程。本文提出编写和推理并行交互程序的技术:程序员可按需创建和同步线程,并为线程指定用户定义的偏序优先级。为确保响应性,作者设计了一个类比 S4 模态逻辑的模态类型系统,静态禁止低优先级线程延迟高优先级线程,从而防止关键的优先级反转错误。文中还给出成本模型,将传统 work-span 模型扩展到竞争调度,以推理良类型程序的响应性与完成时间。最后,通过将技术实现为 Standard ML 扩展,证明了其实用性。

问题
传统协作式与竞争式多线程彼此分离,难以同时支持既有交互又有计算的并行程序,并容易引入优先级反转等响应性缺陷。
方法
支持按需创建/同步线程和用户定义偏序优先级,并设计类比 S4 模态逻辑的模态类型系统来静态排除低优先级线程拖延高优先级线程;同时扩展 work-span 成本模型以纳入竞争调度。
评估
将所提技术实现为 Standard ML 语言的扩展,以说明其现实可行性。
原文摘要(Abstract)

Multi-threaded programs have traditionally fallen into one of two domains: cooperative and competitive. These two domains have traditionally remained mostly disjoint, with cooperative threading used for increasing throughput in compute-intensive applications such as scientific workloads and cooperative threading used for increasing responsiveness in interactive applications such as GUIs and games. As multicore hardware becomes increasingly mainstream, there is a need for bridging these two disjoint worlds, because many applications mix interaction and computation and would benefit from both cooperative and competitive threading.In this paper, we present techniques for programming and reasoning about parallel interactive applications that can use both cooperative and competitive threading. Our techniques enable the programmer to write rich parallel interactive programs by creating and synchronizing with threads as needed, and by assigning threads user-defined and partially ordered priorities. To ensure important responsiveness properties, we present a modal type system analogous to S4 modal logic that precludes low-priority threads from delaying high-priority threads, thereby statically preventing a crucial set of priority-inversion bugs. We then present a cost model that allows reasoning about responsiveness and completion time of well-typed programs. The cost model extends the traditional work-span model for cooperative threading to account for competitive scheduling decisions needed to ensure responsiveness. Finally, we show that our proposed techniques are realistic by implementing them as an extension to the Standard ML language.

链接与引用

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

BibTeX
@article{paperbot270,
  title = {Competitive parallelism: getting your priorities right},
  author = {Stefan K. Muller and Umut A. Acar and Robert Harper},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {2},
  number = {ICFP},
  year = {2018},
  doi = {10.1145/3236790}
}