Toggle Main Menu Toggle Search

ePrints

A structural proof of the soundness of rely/guarantee rules

Lookup NU author(s): Dr Joey Coleman, Professor Cliff Jones

Downloads


Abstract

The challenge of finding compositional ways of (formally) developing concurrent programs is considerable. Various forms of rely and guarantee conditions have been used to record and reason about interference in ways which do indeed provide compositional development methods for such programs. This paper presents a new approach to justifying the soundness of rely/guarantee inference rules. The underlying concurrent language is defined by an operational semantics which allows fine-grained interleaving and nested concurrency; the proof that the rely/guarantee rules are consistent with that semantics (including termination) is by a structural induction. A lemma which relates the states which can arise from the extra interference that results from taking a portion of the program out of context is key to our ability to do the proof without having to perform induction over the computation history. This lemma also offers a way to understand some elusive expressibility issues around rely/guarantee conditions.


Publication metadata

Author(s): Coleman JW, Jones CB

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2006

Pages: 28

Print publication date: 01/10/2006

Source Publication Date: October 2006

Report Number: 987

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/987.pdf


Share