The rely-guarantee method for verifying shared variable concurrent programs

doi:10.1007/bf01211617

The rely-guarantee method for verifying shared variable concurrent programs

1997-03-01

0

OA

AI

DOI：10.1007/bf01211617

Original

Original request for help

Save

Abstract

En 中文

Abstract Compositional proof systems for shared variable concurrent programs can be devised by including the interference information in the specifications. The formalism falls into a category called rely-guarantee (or assumption-commitment) , in which a specification is explicitly (syntactically) split into two corresponding parts. This paper summarises existing work on the rely-guarantee method and gives a systematic presentation. A proof system for partial correctness is given first, thereafter it is demonstrated how the relevant rules can be adapted to verify deadlock freedom and convergence. Soundness and completeness, of which the completeness proof is new, are studied with respect to an operational model. We observe that the rely-guarantee method is in a sense a reformulation of the classical non-compositional Owicki & Gries method, and we discuss throughout the paper the connection between these two methods.

The rely-guarantee method for verifying shared variable concurrent programs

Abstract

Journal

Organization

Cited Papers