{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T22:45:45Z","timestamp":1774046745096,"version":"3.50.1"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2017,9,1]],"date-time":"2017-09-01T00:00:00Z","timestamp":1504224000000},"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":[[2017,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Given a mutual exclusion algorithm\n            <jats:italic>MXd<\/jats:italic>\n            for\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>d<\/mml:mi>\n                    <mml:mo>\u2265<\/mml:mo>\n                    <mml:mn>2<\/mml:mn>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            threads, a mutual exclusion algorithm for\n            <jats:inline-formula>\n              <jats:alternatives>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>N<\/mml:mi>\n                    <mml:mo>&gt;<\/mml:mo>\n                    <mml:mi>d<\/mml:mi>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>\n            threads can be built in a tree of degree\n            <jats:italic>d<\/jats:italic>\n            with\n            <jats:italic>N<\/jats:italic>\n            leaves, with the critical section at the root of the tree. This tournament solution seems obviously correct and efficient. The present note proves the correctness, and formalizes the efficiency in terms of concurrent complexity by means of Bounded Unity. If the tree is balanced, the throughput is logarithmic in\n            <jats:italic>N<\/jats:italic>\n            . If moreover\n            <jats:italic>MXd<\/jats:italic>\n            satisfies FCFS (first-come first-served), the worst case individual delay of the tournament algorithm is of order\n            <jats:italic>N<\/jats:italic>\n            . This is optimal.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0407-x","type":"journal-article","created":{"date-parts":[[2017,1,27]],"date-time":"2017-01-27T13:51:44Z","timestamp":1485525104000},"page":"833-852","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Tournaments for mutual exclusion: verification and concurrent complexity"],"prefix":"10.1145","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1413-4320","authenticated-orcid":false,"given":"Wim H.","family":"Hesselink","sequence":"first","affiliation":[{"name":"Johann Bernoulli Institute for Mathematics and Computer Science University of Groningen, P.O.Box 407, 9700 AK, Groningen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Apt KR de Boer FS Olderog E-R (2009) Verification of sequential and concurrent programs. Springer New York","DOI":"10.1007\/978-1-84882-745-5"},{"key":"e_1_2_1_2_2_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 Exper. 27:651\u2013701. doi:10.1002\/cpe.3263","DOI":"10.1002\/cpe.3263"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Buhr PA Dice D Hesselink WH (2016) Dekker\u2019s mutual exclusion algorithm made RW-safe. Concurr Comput Pract Exp 28:144\u2013165. doi:10.1002\/cpe.3659","DOI":"10.1002\/cpe.3659"},{"key":"e_1_2_1_2_4_2","unstructured":"Burns JE (1981) Complexity of communication among asynchronous parallel processes Ph.D. thesis School of Information and Computer Science Georgia Institute of Technology"},{"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":"crossref","unstructured":"de Bruijn NG (1967) Additional comments on a problem in concurrent programming control. Commun ACM 10:137\u2013138 (Letter to the Editor)","DOI":"10.1145\/363162.363167"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/365559.365617"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050066"},{"key":"e_1_2_1_2_9_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_10_2","doi-asserted-by":"crossref","unstructured":"Hesselink WH (2016) Correctness and concurrent complexity of the Black-White Bakery algorithm. Formal Aspects Comput 28:325\u2013341. doi:10.1007\/s00165-016-0364-4","DOI":"10.1007\/s00165-016-0364-4"},{"key":"e_1_2_1_2_11_2","unstructured":"Hesselink WH (2016) PVS proof script for: tournaments for mutual exclusion. http:\/\/wimhesselink.nl\/mechver\/tournaments (Accessed 8 Aug 2016)"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Kessels DE (1982) Arbitration without common modifiable variables. Acta Inf 17:135\u2013141","DOI":"10.1007\/BF00288966"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Knuth DE (1966) Additional comments on a problem in concurrent programming control. Commun ACM 9:321\u2013322 (Letter to the Editor)","DOI":"10.1145\/355592.365595"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/361082.361093"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/5383.5384"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115370"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8528-6"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_2_20_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_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Peterson GL Fischer MJ (1977) Economical solutions for the critical section problem in a distributed system (extended abstract). In: STOC \u201977: Proceedings of the 9th annual ACM symposium on theory of computing New York. ACM pp 91\u201397","DOI":"10.1145\/800105.803398"},{"key":"e_1_2_1_2_23_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"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Xu Q de Roever W-P He J (1997) The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects Comput 9:149\u2013174","DOI":"10.1007\/BF01211617"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Zhang X Yan Y Castenada R (1996) Evaluating and designing software mutual exclusion algorithms on shared memory multiprocessors. IEEE Parallel Distrib Technol Syst Appl 4:25\u201342","DOI":"10.1109\/88.481663"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0407-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0407-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0407-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0407-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:54:01Z","timestamp":1641538441000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0407-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9]]},"references-count":25,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["10.1007\/s00165-016-0407-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0407-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,9]]}}}