Modelling mutual exclusion in a process algebra with time-outs

DOI10.1016/J.IC.2023.105079MaRDI QIDQ6053409zbMATH OpenOpenAlexFDO

Authors Rob van Glabbeek

Publication date 27 September 2023

Published in Information and Computation (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

asymmetric concurrency relationsatomicityblockingCCSfair schedulersfairnessjustnessKripke structureslabelled transition systemsmutual exclusionoverlapping reads and writesPeterson's protocolPetri netsprocess algebraprogressreactive temporal logicsafe registerssafety propertiesspeed independencetime-outs

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Abstract: I show that in a standard process algebra extended with time-outs one can correctly model mutual exclusion in such a way that starvation-freedom holds without assuming fairness or justness, even when one makes the problem more challenging by assuming memory accesses to be atomic. This can be achieved only when dropping the requirement of speed independence.

Recommendations

• Analysing mutual exclusion using process algebra with signals
• scientific article; zbMATH DE number 4064457
• scientific article; zbMATH DE number 4074455
• Revisiting timing in process algebra.
• scientific article; zbMATH DE number 7559462
• A process algebra for timed systems
• Time and Fairness in a Process Algebra with Non-blocking Reading
• Reactive bisimulation semantics for a process algebra with timeouts
• Formal Methods for the Design of Real-Time Systems
• scientific article; zbMATH DE number 1876862

Cites work

• A new solution of Dijkstra's concurrent programming problem
• A Theory of Communicating Sequential Processes
• Abstract processes of place/transition systems
• Analysing mutual exclusion using process algebra with signals
• Analysis of A time‐shared processor
• Appraising fairness in languages for distributed programming
• Automated analysis of mutual exclusion algorithms using CCS
• CCS: it's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions
• Concurrent programming: algorithms, principles, and foundations.
• Efficiency of asynchronous systems, read arcs, and the MUTEX-problem
• Ensuring liveness properties of distributed systems: open problems
• Failure trace semantics for a process algebra with time-outs
• Fairness of actions in system computations
• scientific article; zbMATH DE number 4018370 (Why is no real title available?)
• scientific article; zbMATH DE number 4164152 (Why is no real title available?)
• scientific article; zbMATH DE number 3896316 (Why is no real title available?)
• scientific article; zbMATH DE number 3940713 (Why is no real title available?)
• scientific article; zbMATH DE number 3972158 (Why is no real title available?)
• scientific article; zbMATH DE number 4030999 (Why is no real title available?)
• scientific article; zbMATH DE number 4035159 (Why is no real title available?)
• scientific article; zbMATH DE number 4037225 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 1142329 (Why is no real title available?)
• scientific article; zbMATH DE number 3995041 (Why is no real title available?)
• scientific article; zbMATH DE number 1412988 (Why is no real title available?)
• scientific article; zbMATH DE number 7317251 (Why is no real title available?)
• scientific article; zbMATH DE number 7453963 (Why is no real title available?)
• scientific article; zbMATH DE number 7559462 (Why is no real title available?)
• Justness. A completeness criterion for capturing liveness properties (extended abstract)
• Logic in Computer Science
• Modeling and analysis of communicating systems
• Mutex needs fairness
• Myths about the mutual exclusion problem
• Off-the-shelf automated analysis of liveness properties for just paths
• On interprocess communication. II: Algorithms
• Petri nets, event structures and domains. I
• Process Algebra
• Proving the Correctness of Multiprocess Programs
• The linear time -- branching time spectrum. I: The semantics of concrete, sequential processes.
• Three logics for branching bisimulation
• Time and Fairness in a Process Algebra with Non-blocking Reading
• Trapping mutual exclusion in the box calculus

Cited in

(4)

• Just testing
• Progress, justness and fairness in modal -calculus formulae
• Branching bisimilarity for processes with time-outs
• Just verification of mutual exclusion algorithms

This page was built for publication: Modelling mutual exclusion in a process algebra with time-outs

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