{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:17:50Z","timestamp":1762521470006},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The standard implementation of mutual exclusion by means of a semaphore allows starvation of processes. Between 1979 and 1986, three algorithms were proposed that preclude starvation. These algorithms use a special kind of semaphore. We model this so-called buffered semaphore rigorously and provide mechanized proofs of the algorithms. We prove that the algorithms are three implementations of one abstract algorithm in which every competing process is overtaken not more than once by any other process. We also consider a so-called polite semaphore, which is weaker than the buffered one and is strong enough for one of the three algorithms. Refinement techniques are used to compare the algorithms and the semaphores.<\/jats:p>","DOI":"10.1007\/s00165-011-0219-y","type":"journal-article","created":{"date-parts":[[2011,12,15]],"date-time":"2011-12-15T18:48:56Z","timestamp":1323974936000},"page":"947-969","source":"Crossref","is-referenced-by-count":6,"title":["Starvation-free mutual exclusion with semaphores"],"prefix":"10.1145","volume":"25","author":[{"given":"Wim H.","family":"Hesselink","sequence":"first","affiliation":[{"name":"Department of Computing Science, University of Groningen, P.O. Box 407, 9700 AK, Groningen, The Netherlands"}]},{"given":"Mark","family":"IJbema","sequence":"additional","affiliation":[{"name":"Department of Computing Science, University of Groningen, P.O. Box 407, 9700 AK, Groningen, The Netherlands"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.5555\/1642724"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_1_2_3_2","volume-title":"Foundations of multithreaded, parallel, and distributed programming","author":"Andrews GR","year":"2000"},{"key":"e_1_2_1_2_4_2","unstructured":"Butenhof DR (1997) Programming with POSIX threads. Addison-Wesley"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Chandy KM Misra J (1988) Parallel program design: a foundation. Addison-Wesley","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/365559.365617"},{"key":"e_1_2_1_2_7_2","first-page":"43","volume-title":"Programming languages NATO Advanced Study Institute","author":"Dijkstra EW","year":"1968"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/363095.363143"},{"key":"e_1_2_1_2_9_2","unstructured":"Dijkstra EW (1977) A strong P\/V-implementation of conditional critical regions. Tech rept Tech Univ Eindhoven EWD 651. www.cs.utexas.edu\/users\/EWD"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Francez N (1986) Fairness. Springer","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-006-0007-y"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.10.003"},{"key":"e_1_2_1_2_13_2","unstructured":"Hesselink WH (2011) Starvation-free mutual exclusion with semaphores. http:\/\/www.cs.rug.nl\/~wim\/mechver\/fairMXsema.html"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"ESOP 86. LNCS vol 213","author":"He J","year":"1986"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"key":"e_1_2_1_2_16_2","unstructured":"Herlihy M Shavit N (2008) The art of multiprocessor programming. Morgan Kaufmann"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/361082.361093"},{"key":"e_1_2_1_2_18_2","unstructured":"Lea D (2000) Concurrent programming in Java. Addison-Wesley"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115370"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Lehmann D Pnueli A Stavi J (1981) Impartiality justice and fairness: the ethics of concurrent termination. In: Proc 8th ICALP. LNCS vol 115. Springer Berlin pp 264\u2013277","DOI":"10.1007\/3-540-10843-2_22"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90041-9"},{"key":"e_1_2_1_2_23_2","unstructured":"Milner R (1971) An algebraic definition of simulation between programs. In: Proc 2nd int joint conf on artificial intelligence. British Comp Soc pp 481\u2013489"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(79)90147-9"},{"key":"e_1_2_1_2_25_2","first-page":"445","volume-title":"Constructive methods in computing science","author":"Martin AJ","year":"1989"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_2_27_2","unstructured":"Owre S Shankar N Rushby JM Stringer-Calvert DWJ (2001) PVS version 2.4 system guide prover guide PVS language reference. http:\/\/pvs.csl.sri.com"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.003"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Szymanski BK (1990) Mutual exclusion revisited. In: Proceedings of the fifth Jerusalem conference on information technology. IEEE Computer Society pp 110\u2013117","DOI":"10.1109\/JCIT.1990.128275"},{"key":"e_1_2_1_2_30_2","unstructured":"Tanenbaum AS (2008) Modern operating systems 3rd edn. Pearson Education\/Prentice Hall"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90117-1"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0219-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:55:36Z","timestamp":1641484536000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0219-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":31,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1007\/s00165-011-0219-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0219-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,11]]}}}