ePrints

Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example

Lookup NU author(s): Emeritus Professor Cliff JonesORCiD, Dr Nisansala Yatapanage

Downloads

• Published version [.pdf]

Licence

This work is licensed under a Creative Commons Attribution 4.0 International License (CC BY 4.0).

Abstract

© 2019, The Author(s). Decomposing the design (or documentation) of large systems is a practical necessity but finding compositional development methods for concurrent software is technically challenging. This paper includes the development of a difficult example in order to draw out lessons about such methods. The concurrent garbage collector development is interesting in several ways; in particular, the final step of its development appears to be just beyond what can be expressed by rely/guarantee relations. This prompts an exploration of the limitations of this well-known method. Although the rely/guarantee approach is used, most of the lessons are more general.

Publication metadata

Author(s): Jones CB, Yatapanage N

Publication type: Article

Publication status: Published

Journal: Formal Aspects of Computing

Year: 2019

Volume: 31

Pages: 353-374

Online publication date: 15/04/2019

Acceptance date: 14/03/2019

Date deposited: 30/04/2019

ISSN (print): 0934-5043

ISSN (electronic): 1433-299X

Publisher: Springer London

URL: https://doi.org/10.1007/s00165-019-00482-3

DOI: 10.1007/s00165-019-00482-3

Altmetrics

Share