Tournaments for mutual exclusion: verification and concurrent complexity

被引：5
|
作者：
Hesselink, Wim H. [1 ]
机构：
[1] Univ Groningen, Johann Bernoulli Inst Math & Comp Sci, POB 407, NL-9700 AK Groningen, Netherlands
来源：
FORMAL ASPECTS OF COMPUTING | 2017年 / 29卷 / 05期
关键词：
Mutual exclusion; UNITY; Concurrency; Shared variables; Concurrent complexity; ALGORITHM;
D O I：
10.1007/s00165-016-0407-x
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Given a mutual exclusion algorithm MXd for threads, a mutual exclusion algorithm for threads can be built in a tree of degree d with 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. If moreover MXd satisfies FCFS (first-come first-served), the worst case individual delay of the tournament algorithm is of order N. This is optimal.
引用
收藏
页码：833 / 852
页数：20
相关论文
共 50 条
  • [1] Closing the complexity gap between FCFS mutual exclusion and mutual exclusion
    Robert Danek
    Wojciech Golab
    Distributed Computing, 2010, 23 : 87 - 111
  • [2] Closing the complexity gap between FCFS mutual exclusion and mutual exclusion
    Danek, Robert
    Golab, Wojciech
    DISTRIBUTED COMPUTING, 2010, 23 (02) : 87 - 111
  • [3] A HIGHLY CONCURRENT GROUP MUTUAL l-EXCLUSION ALGORITHM
    Vidyasankar, K.
    PARALLEL PROCESSING LETTERS, 2006, 16 (04) : 467 - 483
  • [4] Verification of a hierarchical generic mutual exclusion algorithm
    Baarir, Souheib
    Sopena, Julien
    Legond-Aubry, Fabrice
    FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2008, 2008, 5048 : 99 - +
  • [5] An improved lower bound for the time complexity of mutual exclusion
    Anderson, JH
    Kim, YJ
    DISTRIBUTED COMPUTING, 2002, 15 (04) : 221 - 253
  • [6] A fair distributed mutual exclusion algorithm
    Lodha, S
    Kshemkalyani, A
    IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS, 2000, 11 (06) : 537 - 549
  • [7] Mutual Exclusion Verification of Peterson's solution in Isabelle/HOL
    Ji, Xiaojun
    Song, Lihua
    PROCEEDINGS 2016 THIRD INTERNATIONAL CONFERENCE ON TRUSTWORTHY SYSTEMS AND THEIR APPLICATIONS (TSA), 2016, : 81 - 86
  • [8] When does a correct mutual exclusion algorithm guarantee mutual exclusion?
    Lamport, L
    Perl, S
    Weihl, W
    INFORMATION PROCESSING LETTERS, 2000, 76 (03) : 131 - 134
  • [9] Randomized Mutual Exclusion with Constant Amortized RMR Complexity on the DSM
    Giakkoupis, George
    Woelfel, Philipp
    2014 55TH ANNUAL IEEE SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE (FOCS 2014), 2014, : 504 - 513
  • [10] Recoverable mutual exclusion
    Golab, Wojciech
    Ramaraju, Aditya
    DISTRIBUTED COMPUTING, 2019, 32 (06) : 535 - 564
12345