University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > A structural proof of the soundness of rely/guarantee rules

A structural proof of the soundness of rely/guarantee rules

Add to your list(s) Download to your calendar using vCal

  • UserCliff Jones, Newcastle University
  • ClockFriday 27 October 2006, 14:00-15:00
  • HouseFW11.

If you have a question about this talk, please contact Tom Ridge.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity