{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:06Z","timestamp":1775873406138,"version":"3.50.1"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>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. \nThis 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.<\/jats:p>","DOI":"10.1145\/3591253","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"811-834","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Fair Operational Semantics"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2576-1220","authenticated-orcid":false,"given":"Dongjae","family":"Lee","sequence":"first","affiliation":[{"name":"Seoul National University, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6684-0921","authenticated-orcid":false,"given":"Minki","family":"Cho","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3897-1828","authenticated-orcid":false,"given":"Jinwoo","family":"Kim","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2750-5221","authenticated-orcid":false,"given":"Soonwon","family":"Moon","sequence":"additional","affiliation":[{"name":"Inha University, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7093-3824","authenticated-orcid":false,"given":"Youngju","family":"Song","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1656-0913","authenticated-orcid":false,"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2026","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . The MIT Press . isbn:026 2026 49X Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press. isbn:026202649X"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523718"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/362759.362813"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477082"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_36"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_1_9_1","volume-title":"Principles of Distributed Systems, Antonio Fern\u00e0ndez Anta","author":"Herlihy Maurice","unstructured":"Maurice Herlihy and Nir Shavit . 2011. On the Nature of Progress . In Principles of Distributed Systems, Antonio Fern\u00e0ndez Anta , Giuseppe Lipari, and Matthieu Roy (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 313\u2013328. isbn:978-3-642-25873-2 Maurice Herlihy and Nir Shavit. 2011. On the Nature of Progress. In Principles of Distributed Systems, Antonio Fern\u00e0ndez Anta, Giuseppe Lipari, and Matthieu Roy (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 313\u2013328. isbn:978-3-642-25873-2"},{"key":"e_1_2_1_10_1","unstructured":"Gerhard Hessenberg. 1906. Grundbegriffe der mengenlehre. 1 Vandenhoeck & Ruprecht. \t\t\t\t  Gerhard Hessenberg. 1906. Grundbegriffe der mengenlehre. 1 Vandenhoeck & Ruprecht."},{"key":"e_1_2_1_11_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung , Robbert Krebbers , Jacques-Henri Jourdan , Ale\u0161 Bizjak , Lars Birkedal , and Derek Dreyer . 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 ( 2018 ). Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28 (2018)."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_2_1_14_1","volume-title":"25th International Colloquium, ICALP\u201998 Aalborg, Denmark, July 13\u201317, 1998 Proceedings 25","author":"Kesten Yonit","year":"1998","unstructured":"Yonit Kesten , Amir Pnueli , and Li-on Raviv. 1998 . Algorithmic verification of linear temporal logic specifications. In Automata, Languages and Programming : 25th International Colloquium, ICALP\u201998 Aalborg, Denmark, July 13\u201317, 1998 Proceedings 25 . 1\u201316. Yonit Kesten, Amir Pnueli, and Li-on Raviv. 1998. Algorithmic verification of linear temporal logic specifications. In Automata, Languages and Programming: 25th International Colloquium, ICALP\u201998 Aalborg, Denmark, July 13\u201317, 1998 Proceedings 25. 1\u201316."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485475"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7711063"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_2_1_20_1","unstructured":"D. Lehmann A. Pnueli and J. Stavi. 1981. Impartiality justice and fairness: The ethics of concurrent termination. In Automata Languages and Programming Shimon Even and Oded Kariv (Eds.). Springer Berlin Heidelberg Berlin Heidelberg. 264\u2013277. isbn:978-3-540-38745-9 \t\t\t\t  D. Lehmann A. Pnueli and J. Stavi. 1981. Impartiality justice and fairness: The ethics of concurrent termination. In Automata Languages and Programming Shimon Even and Oded Kariv (Eds.). Springer Berlin Heidelberg Berlin Heidelberg. 264\u2013277. isbn:978-3-540-38745-9"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837635"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158108"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_17"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357178"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_8"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_1_30_1","unstructured":"The Coq Development Team. 2021. The Coq Proof Assistant 8.13.2 Reference Manual.  https:\/\/coq.github.io\/doc\/V8.13.2\/refman\/ \t\t\t\t  The Coq Development Team. 2021. The Coq Proof Assistant 8.13.2 Reference Manual.  https:\/\/coq.github.io\/doc\/V8.13.2\/refman\/"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439931"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591253","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591253","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:47Z","timestamp":1750178867000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591253"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":32,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591253"],"URL":"https:\/\/doi.org\/10.1145\/3591253","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}