English

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

Logic in Computer Science 2015-05-25 v1

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.

Keywords

Cite

@article{arxiv.1505.05964,
  title  = {CCS: It's not Fair! Fair Schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions},
  author = {Rob van Glabbeek and Peter Höfner},
  journal= {arXiv preprint arXiv:1505.05964},
  year   = {2015}
}