BCS FACS - Separating the concerns of rely and guarantee in reasoning about concurrent programs

Date/Time: Wednesday 16 September 2015, 6.00pm-9.00pm

BCS, 1st Floor, The Davidson Building, 5 Southampton Street, London, WC2E 7HA | Maps



The rely-guarantee approach to reasoning about concurrent programs  pioneered by Cliff Jones makes use of a rely condition r (a binary relation) to record the expected interference from the environment: the interference steps must satisfy r between their before and after states. Complementing the rely assumption is a guarantee condition g (a binary relation) that the process ensures holds for all its program steps.

This talk looks at considering rely and guarantee conditions as separate concerns.

Separate laws are developed for guarantees and relies in isolation and then these are combined to build general laws for refining concurrent programs.

Generalisation of relies and guarantees from binary relations to processes is then considered.

Taking an algebraic perspective allows one to apply the laws to a range of concurrency models including shared-memory, event-based and hybrid systems.

Ian Hayes (home page)

Ian Hayes (Newcastle University)

PDF Icon Presentation - Ian Hayes