Authors
- Dongjae Lee*, Seoul National University, Korea
- Minki Cho*, Seoul National University, Korea
- Jinwoo Kim, Seoul National University, Korea
- Soonwon Moon, Inha University, Korea
- Youngju Song, MPI-SWS, Germany
- Chung-Kil Hur, Seoul National University, Korea
* The first two authors contributed equally to this work.
Abstract
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.
Errata
(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]"