Trustworthy Systems

CCS: It's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions

Authors

Rob van Glabbeek and Peter Hoefner

NICTA

UNSW

Abstract

In the process algebra community it is sometimes suggested that, on some level of abstraction, any distributed system can be modelled in standard process algebraic specification formalisms like CCS. This sentiment is strengthened by results testifying that CCS, like many similar formalisms, is Turing powerful and provides a mechanism for interaction. This paper counters that sentiment by presenting a simple fair scheduler---one that in suitable variations occurs in many distributed systems---of which no implementation can be expressed in CCS, unless CCS is enriched with a fairness assumption.

Since Dekker's and Peterson's mutual exclusion protocols implement fair schedulers, it follows that these protocols cannot be rendered correctly in CCS without imposing a fairness assumption. Peterson expressed this algorithm correctly in pseudocode without resorting to a fairness assumption, so it furthermore follows that CCS lacks the expressive power to accurately capture such pseudocode.

BibTeX Entry

  @article{vanGlabbeek_Hfner_15,
    author           = {van Glabbeek, Robert and H\"ofner, Peter},
    doi              = {10.1007/s00236-015-0221-6},
    journal          = {Acta Informatica},
    keywords         = {process algebra, expressiveness, fair schedulers, progress, justness, fairness, ccs, petri nets,
                        mutual exclusion},
    month            = apr,
    number           = {2-3},
    pages            = {175--205},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/8302.pdf},
    title            = {{{CCS}}: It's not fair! {F}air schedulers cannot be implemented in {{CCS}}-like languages even under
                        progress and certain fairness assumptions},
    volume           = {52},
    year             = {2015}
  }

Download