Generalised rely-guarantee concurrency: an algebraic foundation

DOI10.1007/S00165-016-0384-0zbMATH Open1348.68035arXiv1603.01776OpenAlexW2293609693MaRDI QIDQ333330FDOQ333330

Ian Hayes

Publication date: 28 October 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Abstract: The rely-guarantee technique allows one to reason compositionally about concurrent programs. To handle interference the technique makes use of rely and guarantee conditions, both of which are binary relations on states. A rely condition is an assumption that the environment performs only atomic steps satisfying the rely relation and a guarantee is a commitment that every atomic step the program makes satisfies the guarantee relation. In order to investigate rely-guarantee reasoning more generally, in this paper we allow interference to be represented by a process rather than a relation and hence derive more general rely-guarantee laws. The paper makes use of a weak conjunction operator between processes, which generalises a guarantee relation to a guarantee process, and introduces a rely quotient operator, which generalises a rely relation to a process. The paper focuses on the algebraic properties of the general rely-guarantee theory. The Jones-style rely-guarantee theory can be interpreted as a model of the general algebraic theory and hence the general laws presented here hold for that theory.

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

Recommendations

• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• On rely-guarantee reasoning
• scientific article; zbMATH DE number 3938541
• A Structural Proof of the Soundness of Rely/guarantee Rules
• An algebra of synchronous atomic steps

zbMATH Keywords

program verificationconcurrent Kleene algebraconcurrent programmingprogram algebrarely-guarantee concurrency

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Cites Work

• Title not available (Why is that?)
• Laws of programming
• Title not available (Why is that?)
• Refinement Calculus
• Title not available (Why is that?)
• Balancing expressiveness in formal approaches to concurrency
• An axiomatic basis for computer programming
• Concurrency verification. Introduction to compositional and noncompositional methods
• Reasoning algebraically about loops
• Towards a refinement algebra
• Title not available (Why is that?)
• The specification statement
• A Structural Proof of the Soundness of Rely/guarantee Rules
• Concurrent Kleene algebra and its foundations
• On correct refinement of programs
• A refinement calculus for shared-variable parallel and distributed programming
• Algebraic and coalgebraic methods in the mathematics of program construction. International summer school and workshop, Oxford, GB, April 10--14, 2000. Revised lectures
• Tentative steps toward a development method for interfering programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A theoretical basis for stepwise refinement and the programming calculus

Cited In (13)

• Encoding fairness in a synchronous concurrent program algebra
• Title not available (Why is that?)
• Unifying theories of reactive design contracts
• A Structural Proof of the Soundness of Rely/guarantee Rules
• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• Title not available (Why is that?)
• Title not available (Why is that?)
• Deny-Guarantee Reasoning
• Designing a semantic model for a wide-spectrum language with concurrency
• Title not available (Why is that?)
• A parametric rely-guarantee reasoning framework for concurrent reactive systems
• Specifying and reasoning about shared-variable concurrency
• Automated verification of reactive and concurrent programs by calculation

This page was built for publication: Generalised rely-guarantee concurrency: an algebraic foundation

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