* The first two authors contributed equally to this work.


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 abstractly expressing various kinds of fairness properties and reasoning about them are relatively underdeveloped compared to those for safety properties. In this paper, we propose FOS (Fair Operational Semantics), a theory for expressing arbitrary notions of custom fairness as an operational semantics and reasoning about them. In particular, FOS provides a thread-local simulation relation equipped with separation-logic-style resource algebras that gives a powerful reasoning principles both for proving and exploiting fairness, whose soundness is proven for every fairness definable in FOS. As an example, we verify a ticket lock implementation and a client of it under a relaxedmemory concurrency, which involves reasoning about notions of fairness capturing fairness of the thread scheduler, fairness the ticket lock and even fairness of relaxed memory, using FOS. Finally, we formalize the theory of FOS in Coq.


(The paper in this page is corrected)

  • Change "Note that [D'Osualdo et al. 2021]" on page 17 to "Note that [Rocha Pinto et al. 2016]"