Trustworthy Systems

Analysing mutual exclusion using process algebra with signals

Authors

Victor Dyseryn, Rob van Glabbeek and Peter Hoefner

DATA61

UNSW Sydney

Australian National University

Abstract

In contrast to common belief, the Calculus of Communicating Systems (CCS) and similar process algebras lack the expressive power to accurately capture mutual exclusion protocols without enriching the language with fairness assumptions. Adding a fairness assumption to implement a mutual exclusion protocol seems counter-intuitive. We employ a signalling operator, which can be combined with CCS, or other process calculi, and show that this minimal extension is expressive enough to model mutual exclusion: we confirm the correctness of Peterson's mutual exclusion algorithm for two processes, as well as Lamport's bakery algorithm, under reasonable assumptions on the underlying memory model. The correctness of Peterson's algorithm for more than two processes requires stronger, less realistic assumptions on the underlying memory model.

BibTeX Entry

  @inproceedings{Dyseryn_GH_17,
    address          = {Berlin},
    author           = {Dyseryn, Victor and van Glabbeek, Robert and H\"{o}fner, Peter},
    booktitle        = {Combined International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural
                        Operational Semantics (EXPRESS/SOS)},
    date             = {2017-8-31},
    doi              = {https://doi.org/10.4204/EPTCS.255.2},
    month            = aug,
    numpages         = {17},
    paperurl         = {https://trustworthy.systems/publications/full_text/Dyseryn_GH_17.pdf},
    publisher        = {Open Publishing Association},
    series           = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},
    title            = {Analysing Mutual Exclusion using Process Algebra with Signals},
    volume           = {255},
    year             = {2017}
  }

Download