Trustworthy Systems

Is speed-independent mutual exclusion implementable?

Authors

Rob van Glabbeek

DATA61

UNSW Sydney

Abstract

A mutual exclusion algorithm is called speed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker's, Peterson's and Lamport's bakery are meant to be speed independent. In this talk I argue that speed-independent mutual exclusion may not be implementable on standard hardware, depending on how we believe reading and writing to a memory location is really carried out. It can be implemented on electrical circuits, however. This builds on previous work showing that mutual exclusion cannot be accurately modelled in standard process algebras.

BibTeX Entry

  @inproceedings{vanGlabbeek_18_3,
    address          = {Beijing, China},
    author           = {van Glabbeek, Robert},
    booktitle        = {International Conference on Concurrency Theory (CONCUR)},
    date             = {2018-9-4},
    doi              = {https://doi.org/10.4230/LIPIcs.CONCUR.2018.3},
    editor           = {{Sven Schewe and Lijun Zhang}},
    issn             = {18688969},
    keywords         = {Mutual exclusion; speed independence; concurrent reading and writing; liveness; justness.},
    month            = sep,
    numpages         = {3 p.},
    paperurl         = {https://trustworthy.systems/publications/full_text/vanGlabbeek_18_3.pdf},
    publisher        = {Schloss Dagstuhl},
    series           = {Leibniz International Proceedings in Informatics (LIPIcs) 118:3},
    title            = {Is Speed-Independent Mutual Exclusion Implementable?},
    volume           = {118},
    year             = {2018}
  }

Download