Fair Operational Semantics - Theory for Expressing and Reasoning About Fairness Properties

Explore a groundbreaking 20-minute conference talk from PLDI 2023 that introduces Fair Operational Semantics (FOS), a novel theory for expressing and reasoning about fairness properties in program verification. Delve into the capabilities of FOS in representing arbitrary notions of fairness as operational semantics and enabling thread-local reasoning through simulation relations with separation-logic-style resource algebras. Examine a practical application of FOS in verifying a ticket lock implementation and its client under weak memory concurrency, demonstrating its versatility in handling various fairness concepts. Learn about the full Coq formalization of the FOS theory and accompanying examples, supported by available and reusable artifacts. Gain insights from researchers at Seoul National University, Inha University, and MPI-SWS as they present their innovative approach to addressing the challenges of fairness properties in program verification.