Encoding fairness in a synchronous concurrent program algebra

DOI10.1007/978-3-319-95582-7_13MaRDI QIDQ2024348zbMATH OpenOpenAlexFDO

Authors Ian Hayes, Larissa A. Meinicke

Publication date 4 May 2021

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Concurrent program refinement algebra provides a suitable basis for supporting mechanised reasoning about shared-memory concurrent programs in a compositional manner, for example, it supports the rely/guarantee approach of Jones. The algebra makes use of a synchronous parallel operator motivated by Aczel's trace model of concurrency and with similarities to Milner's SCCS. This paper looks at defining a form of fairness within the program algebra. The encoding allows one to reason about the fair execution of a single process in isolation as well as define fair-parallel in terms of a base parallel operator, of which no fairness properties are assumed. An algebraic theory to support fairness and fair-parallel is developed.

Recommendations

• An algebraic approach to refinement with fair choice
• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• scientific article; zbMATH DE number 1612489
• Fairness, resources, and separation
• A fair calculus of communicating systems

Cites work

• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• An algebra of synchronous atomic steps
• Calculi for synchrony and asynchrony
• Concurrency verification. Introduction to compositional and noncompositional methods
• Designing a semantic model for a wide-spectrum language with concurrency
• Encoding fairness in a synchronous concurrent program algebra
• Fixed-point calculus
• Generalised rely-guarantee concurrency: an algebraic foundation
• scientific article; zbMATH DE number 3714908 (Why is no real title available?)
• scientific article; zbMATH DE number 3735115 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1487492 (Why is no real title available?)
• Tentative steps toward a development method for interfering programs

Cited in

(7)

• Encoding fairness in a synchronous concurrent program algebra
• scientific article; zbMATH DE number 1612489 (Why is no real title available?)
• Fairness, resources, and separation
• scientific article; zbMATH DE number 7167584 (Why is no real title available?)
• An algebraic approach to refinement with fair choice
• Specifying and reasoning about shared-variable concurrency
• Promptness and bounded fairness in concurrent and parameterized systems

This page was built for publication: Encoding fairness in a synchronous concurrent program algebra

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