{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T22:45:04Z","timestamp":1774046704207,"version":"3.50.1"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,4,1]],"date-time":"2016-04-01T00:00:00Z","timestamp":1459468800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Lamport\u2019s Bakery Algorithm (Commun ACM 17:453\u2013455,\n            <jats:xref ref-type=\"bibr\">1974<\/jats:xref>\n            ) implements mutual exclusion for a fixed number of threads with the first-come first-served property. It has the disadvantage, however, that it uses integer communication variables that can become arbitrarily large. Taubenfeld\u2019s Black-White Bakery Algorithm (Proceedings of the DISC. LNCS, vol 3274, pp 56\u201370,\n            <jats:xref ref-type=\"bibr\">2004<\/jats:xref>\n            ) keeps the integers bounded, and is adaptive in the sense that the time complexity only depends on the number of competing threads, say\n            <jats:italic>N<\/jats:italic>\n            . The present paper offers an assertional proof of correctness and shows that the concurrent complexity for throughput is linear in\n            <jats:italic>N<\/jats:italic>\n            , and for individual progress is quadratic in\n            <jats:italic>N<\/jats:italic>\n            . This is proved with a bounded version of UNITY, i.e., by assertional means.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0364-4","type":"journal-article","created":{"date-parts":[[2016,3,29]],"date-time":"2016-03-29T07:12:11Z","timestamp":1459235531000},"page":"325-341","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Correctness and concurrent complexity of the Black-White Bakery Algorithm"],"prefix":"10.1145","volume":"28","author":[{"given":"Wim H.","family":"Hesselink","sequence":"first","affiliation":[{"name":"Johann Bernoulli Institute, University of Groningen, Groningen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"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\/j.jpdc.2013.03.009"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Afek Y Stupp G Touitou D (1999) Long-lived adaptive collect with applications. In: Proceedings 40th IEEE symp. on foundations of computer science pp 262\u2013272","DOI":"10.1109\/SFFCS.1999.814598"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Buhr PA Dice D Hesselink WH (2015) High-performance N -thread software solutions for mutual exclusion. Concurr Comput Pract Exp 27:651\u2013701. doi:10.1002\/cpe.3263","DOI":"10.1002\/cpe.3263"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.5555\/59087"},{"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","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/s004460050066","article-title":"Progress under bounded fairness","volume":"12","author":"Hesselink WH","year":"1988","journal-title":"Distrib Comput"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.03.003"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-013-0181-7"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Hesselink WH (2015) Mutual exclusion by four shared bits with not more than quadratic complexity. Sci Comput Program 102:57\u201375. doi:10.1016\/j.scico.2015.01.001","DOI":"10.1016\/j.scico.2015.01.001"},{"key":"e_1_2_1_2_11_2","unstructured":"Hesselink WH (2015) PVS proof scripts for four Bakery Algorithms. http:\/\/wimhesselink.nl\/mechver\/bakery\/index.html. Accessed 17 March 2016"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/361082.361093"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/5383.5384"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01786227"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Lycklama EA Hadzilacos V. (1991) A first-come-first-served mutual-exclusion algorithm with small communication variables. ACM Trans Program Lang Syst 13:558\u2013576","DOI":"10.1145\/115372.115370"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8528-6"},{"key":"#cr-split#-e_1_2_1_2_17_2.1","doi-asserted-by":"crossref","unstructured":"Nanevski A Ley-Wild R Sergey I Delbianco GA (2014) Communicating state transition systems for fine-grained concurrent resources. In: Shao Z","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"#cr-split#-e_1_2_1_2_17_2.2","unstructured":"(ed) ESOP 2014. LNCS vol 8410 pp 290-310"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_2_19_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. Accessed 17 March 2016"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Taubenfeld G (2004) The Black-White Bakery Algorithm and related bounded-space adaptive local-spinning and FIFO algorithms. In: Proceedings of the DISC. LNCS vol 3274 pp 56\u201370","DOI":"10.1007\/978-3-540-30186-8_5"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0364-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0364-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0364-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:55:10Z","timestamp":1641538510000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0364-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["10.1007\/s00165-016-0364-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0364-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4]]}}}