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

DOI10.1007/S00236-015-0221-6zbMATH Open1327.68171arXiv1505.05964OpenAlexW2081455126MaRDI QIDQ2340255FDOQ2340255

Authors: Peter Höfner, Rob van Glabbeek 

Publication date: 16 April 2015

Published in: Acta Informatica (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1505.05964

Recommendations

• Weak and strong fairness in CCS
• A fair calculus of communicating systems
• Appraising fairness in languages for distributed programming
• scientific article; zbMATH DE number 1330452
• scientific article; zbMATH DE number 3926216

zbMATH Keywords

fairnessdistributed systemfair scheduler

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• COSY - a system specification language based on paths and processes
• Title not available (Why is that?)
• Title not available (Why is that?)
• Myths about the mutual exclusion problem
• A calculus of mobile processes. I
• Reactive Systems
• Appraising fairness in languages for distributed programming
• Comparing the worst-case efficiency of asynchronous systems with PAFAS
• A process algebra for timed systems
• Mutex needs fairness
• A process algebra for wireless mesh networks
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Trapping mutual exclusion in the box calculus
• Abstract processes of place/transition systems
• A Theory of Communicating Sequential Processes
• Title not available (Why is that?)
• Nets, Terms and Formulas
• On the consistency of Koomen's fair abstraction rule
• Towards a unified approach to encodability and separation results for process calculi
• Expressiveness of process algebras
• Reactive Turing machines
• Title not available (Why is that?)
• Title not available (Why is that?)
• Turing machines, transition systems, and interaction
• Priority in process algebra.
• Title not available (Why is that?)
• Discrete time process algebra
• Title not available (Why is that?)
• Title not available (Why is that?)
• Ready-Trace Semantics for Concrete Process Algebra with the Priority Operator
• Title not available (Why is that?)
• A fair calculus of communicating systems
• Efficiency of asynchronous systems, read arcs, and the MUTEX-problem
• Analysis of A time‐shared processor
• Title not available (Why is that?)
• Automated analysis of mutual exclusion algorithms using CCS
• Title not available (Why is that?)
• Weak and strong fairness in CCS
• Liveness of a mutex algorithm in a fair process algebra
• Fairness of actions in system computations
• Title not available (Why is that?)
• Time and Fairness in a Process Algebra with Non-blocking Reading
• On Specifying Timeouts

Cited In (17)

• Off-the-shelf automated analysis of liveness properties for just paths (extended abstract)
• Structure preserving bisimilarity, supporting an operational Petri net semantics of CCSP
• Off-the-shelf automated analysis of liveness properties for just paths
• Analysing mutual exclusion using process algebra with signals
• Title not available (Why is that?)
• Global types with internal delegation
• Keep it fair: equivalence and composition
• Modelling mutual exclusion in a process algebra with time-outs
• A case in point: verification and testing of a EULYNX interface
• Explicit Identifiers and Contexts in Reversible Concurrent Calculus
• Just testing
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Reactive bisimulation semantics for a process algebra with timeouts
• Weak and strong fairness in CCS
• Ensuring liveness properties of distributed systems: open problems

Uses Software

• LOTOS
• COSY

This page was built for publication: CCS: it's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2340255)