Tournaments for mutual exclusion: verification and concurrent complexity

Research output: Contribution to journalArticleAcademicpeer-review

1 Citation (Scopus)
196 Downloads (Pure)

Abstract

Given a mutual exclusion algorithm MXd for d≥2d≥2 threads, a mutual exclusion algorithm for N>dN>d 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.
Original languageEnglish
Pages (from-to)833-852
Number of pages19
JournalFormal Aspects of Computing
Volume29
Issue number5
Early online date27-Jan-2017
DOIs
Publication statusPublished - Sep-2017

Keywords

  • PROGRAMMING CONTROL
  • SHARED-MEMORY MULTIPROCESSORS
  • WHITE BAKERY ALGORITHM
  • Shared variables
  • Concurrent complexity
  • Mutual exclusion
  • UNITY
  • Concurrency

Cite this