一句话：提出 FOS，把任意公平性概念编码为操作语义，并用资源代数实现线程局部公平性推理。
公平性属性断言坏事件不会在好事件发生前无限延续，在程序验证中很关键；但相比安全性属性，通用表达与推理方法仍不足。本文提出 FOS（Fair Operational Semantics），一种可将任意公平性概念表述为操作语义并据此推理的理论。FOS 通过线程局部模拟关系及分离逻辑风格资源代数，支持对公平性的线程局部推理。作者在弱内存并发下验证票据锁实现及其客户端，该案例需同时推理调度器公平性、票据锁公平性和弱内存公平性。FOS 理论及示例均在 Coq 中完整形式化。
Fairness properties, which state that a sequence of bad events cannot happen infinitely before a good event takes place, are often crucial in program verification. However, general methods for expressing and reasoning about various kinds of fairness properties are relatively underdeveloped compared to those for safety properties. This paper proposes FOS (Fair Operational Semantics), a theory capable of expressing arbitrary notions of fairness as an operational semantics and reasoning about these notions of fairness. In addition, FOS enables thread-local reasoning about fairness by providing thread-local simulation relations equipped with separation- logic-style resource algebras. We verify a ticket lock implementation and a client of the ticket lock under weak memory concurrency as an example, which requires reasoning about different notions of fairness including fairness of a scheduler, fairness of the ticket lock implementation, and even fairness of weak memory. The theory of FOS, as well as the examples in the paper, are fully formalized in Coq.
@article{paperbot2012,
title = {Fair Operational Semantics},
author = {Dongjae Lee and Minki Cho and Jinwoo Kim and Soonwon Moon and Youngju Song and Chung-Kil Hur},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591253}
}