一句话：提出支持选择性通信与一等通信协议的同步消息传递分层优先级方案，并在 CML 中实现验证。
该论文研究同步消息传递语言中线程优先级机制的表达能力问题：经典优先级方案禁止不同优先级线程间可能阻塞的交互，因而排除了高优先级线程与低优先级线程通信的程序。作者提出一种分层优先级方案，支持选择性通信和一等通信协议，并在以动作为核心的新语义框架中形式化，证明若干期望性质。原型集成到 MLton SML 编译器与运行时中的 Concurrent ML。通过有序买卖协议、Swerve Web 服务器可预测关闭和 eXene 窗口工具包三个案例评估，表明可便捷地为现有 CML 程序添加优先级且性能开销可忽略。
Abstract In this paper, we introduce a tiered-priority scheme for a synchronous message-passing language with support for selective communication and first-class communication protocols. Crucially, our scheme allows higher priority threads to communicate with lower priority threads, providing the ability to express programs that would be rejected by classic priority mechanisms that disallow any (potentially) blocking interactions between threads of differing priorities. We formalize our scheme in a novel semantic framework featuring a collection of actions to represent possible communications. Utilizing our formalism, we prove several important and desirable properties of our priority scheme. We also provide a prototype implementation of our tiered-priority scheme capable of expressing Concurrent ML and built in the MLton SML compiler and runtime. We evaluate the viability of our implementation through three case studies: a prioritized buyer-seller protocol and predictable shutdown mechanisms in the Swerve web server and eXene windowing toolkit. Our experiments show that priority can be easily added to existing CML programs without degrading performance. Our system exhibits negligible overheads on more modest workloads.
@article{paperbot1623,
title = {Send to me first: Priority in synchronous message-passing},
author = {CHENG-EN CHUANG and GRANT IRACI and LUKASZ ZIAREK},
journal = {Journal of Functional Programming},
volume = {32},
year = {2022},
doi = {10.1017/s0956796822000119}
}