The context of this work is cooperative scheduling, a concurrency paradigm, where task execution is not arbitrarily preempted. Instead, language constructs exist that let a task voluntarily yield the right to execute to another task. The inquiry is the design of provably fair schedulers and suitable notions of fairness for cooperative scheduling languages. To the best of our knowledge, this problem has not been addressed so far. Our approach is to study fairness independently from syntactic constructs or environments, purely from the point of view of the semantics of programming languages, i.e., we consider fairness criteria using the formal definition of a program execution. We develop our concepts for classic structural operational semantics (SOS) as well as for the recent locally abstract, globally concrete (LAGC) semantics. The latter is a highly modular approach to semantics ensuring the separation of concerns between local statement evaluation and scheduling decisions. The new knowledge contributed by our work is threefold: first, we show that a new fairness notion, called quiescent fairness, is needed to characterize fairness adequately in the context of cooperative scheduling; second, we define a provably fair scheduler for cooperative scheduling languages; third, a qualitative comparison between the SOS and LAGC versions yields that the latter, while taking higher initial effort, is more amenable to proving fairness and scales better under language extensions than SOS. The grounding of our work is a detailed formal proof of quiescent fairness for the scheduler defined in LAGC semantics. The importance of our work is that it provides a formal foundation for the implementation of fair schedulers for cooperative scheduling languages, an increasingly popular paradigm (for example: akka/Scala, JavaScript, async Rust). Being based solely on semantics, our ideas are widely applicable. Further, our work makes clear that the standard notion of fairness in concurrent languages needs to be adapted for cooperative scheduling and, more generally, for any language that combines atomic execution sequences with some form of preemption.

翻译：本文研究合作调度这一并发范式，其中任务执行不会被随意抢占，而是通过语言构造使任务自愿将执行权交给其他任务。我们探究可证明公平的调度器设计及适用于合作调度语言的公平性概念。据我们所知，该问题此前尚未得到解决。我们的方法是独立于语法构造或运行环境，仅从编程语言语义的角度研究公平性，即利用程序执行的正式定义来考量公平性准则。我们针对经典的结构化操作语义（SOS）以及近期提出的局部抽象全局具体（LAGC）语义分别发展相关概念。后者是一种高度模块化的语义方法，可确保局部语句求值与调度决策的关注点分离。本工作的新贡献体现在三方面：首先，证明需要一种名为“静止公平”的新公平性概念来恰当刻画合作调度中的公平性；其次，为合作调度语言定义了一个可证明公平的调度器；第三，通过SOS与LAGC版本的定性比较表明，尽管LAGC初始投入更高，但其更有利于证明公平性，且在语言扩展下比SOS更具扩展性。本工作的基础是基于LAGC语义所定义调度器的静止公平性详细形式化证明。本工作的重要性在于为合作调度语言（一种日益流行的范式，例如akka/Scala、JavaScript、async Rust）中公平调度器的实现提供了形式化基础。由于完全基于语义，我们的思想具有广泛适用性。此外，本工作明确指出，并发语言中的标准公平性概念需要针对合作调度进行适配，更广泛而言，需要适用于任何将原子执行序列与某种抢占形式相结合的语言。