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