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

• Published in: Acta informatica 2015-04, Vol.52 (2-3), p.175-205
• Main Authors: van Glabbeek, Rob J., Höfner, Peter
• Format: Article
• Language: English
• Subjects: Algebra; Algorithms; Communities; Computer networks; Computer Science; Computer Systems Organization and Communication Networks; Data Structures and Information Theory; Enrichment; Formalism; Information Systems and Communication Service; Logics and Meanings of Programs; Mathematical analysis; Original Article; Software Engineering/Programming and Operating Systems; Specifications; Studies; System theory; Theory of Computation
• ISSN: 0001-5903; 1432-0525
• DOI: 10.1007/s00236-015-0221-6

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.