Explicit Stabilisation for Modular Rely-Guarantee Reasoning

John Wickerson; Mike Dodds; Matthew J. Parkinson

doi:10.1007/978-3-642-11957-6_32

Explicit Stabilisation for Modular Rely-Guarantee Reasoning

John Wickerson, Mike Dodds, Matthew J. Parkinson

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We propose a new formalisation of stability for Rely-Guarantee, in which an assertion’s stability is encoded into its syntactic form. This allows two advances in modular reasoning. Firstly, it enables Rely-Guarantee, for the first time, to verify concurrent libraries independently of their clients’ environments. Secondly, in a sequential setting, it allows a module’s internal interference to be hidden while verifying its clients. We demonstrate our approach by verifying, using RGSep, the Version 7 Unix memory manager, uncovering a twenty-year-old bug in the process.

Original language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings
Publisher	Springer
Pages	610-629
Number of pages	20
Volume	6012 LNCS
ISBN (Electronic)	978-3-642-11957-6
ISBN (Print)	978-3-642-11956-9
DOIs	https://doi.org/10.1007/978-3-642-11957-6_32
Publication status	Published - 2010
Event	19th European Symposium on Programming (ESOP), ETAPS 2010 - Paphos, Cyprus Duration: 20 Mar 2010 → 28 Mar 2010

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	6012
ISSN (Print)	0302-9743

Conference

Conference	19th European Symposium on Programming (ESOP), ETAPS 2010
Country/Territory	Cyprus
City	Paphos
Period	20/03/10 → 28/03/10

Access to Document

10.1007/978-3-642-11957-6_32

http://link.springer.com/chapter/10.1007/978-3-642-11957-6_32

Cite this

Wickerson, J., Dodds, M., & Parkinson, M. J. (2010). Explicit Stabilisation for Modular Rely-Guarantee Reasoning. In Programming Languages and Systems: 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings (Vol. 6012 LNCS, pp. 610-629). (Lecture Notes in Computer Science; Vol. 6012). Springer. https://doi.org/10.1007/978-3-642-11957-6_32

Wickerson, John ; Dodds, Mike ; Parkinson, Matthew J. / Explicit Stabilisation for Modular Rely-Guarantee Reasoning. Programming Languages and Systems: 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. Vol. 6012 LNCS Springer, 2010. pp. 610-629 (Lecture Notes in Computer Science).

@inproceedings{9ee70d834b7146f7bf2c59ea30e879bc,

title = "Explicit Stabilisation for Modular Rely-Guarantee Reasoning",

abstract = "We propose a new formalisation of stability for Rely-Guarantee, in which an assertion{\textquoteright}s stability is encoded into its syntactic form. This allows two advances in modular reasoning. Firstly, it enables Rely-Guarantee, for the first time, to verify concurrent libraries independently of their clients{\textquoteright} environments. Secondly, in a sequential setting, it allows a module{\textquoteright}s internal interference to be hidden while verifying its clients. We demonstrate our approach by verifying, using RGSep, the Version 7 Unix memory manager, uncovering a twenty-year-old bug in the process.",

author = "John Wickerson and Mike Dodds and Parkinson, {Matthew J.}",

year = "2010",

doi = "10.1007/978-3-642-11957-6_32",

language = "English",

isbn = "978-3-642-11956-9",

volume = "6012 LNCS",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "610--629",

booktitle = "Programming Languages and Systems",

address = "Germany",

note = "19th European Symposium on Programming (ESOP), ETAPS 2010 ; Conference date: 20-03-2010 Through 28-03-2010",

}

Wickerson, J, Dodds, M & Parkinson, MJ 2010, Explicit Stabilisation for Modular Rely-Guarantee Reasoning. in Programming Languages and Systems: 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. vol. 6012 LNCS, Lecture Notes in Computer Science, vol. 6012, Springer, pp. 610-629, 19th European Symposium on Programming (ESOP), ETAPS 2010, Paphos, Cyprus, 20/03/10. https://doi.org/10.1007/978-3-642-11957-6_32

Explicit Stabilisation for Modular Rely-Guarantee Reasoning. / Wickerson, John; Dodds, Mike; Parkinson, Matthew J.
Programming Languages and Systems: 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. Vol. 6012 LNCS Springer, 2010. p. 610-629 (Lecture Notes in Computer Science; Vol. 6012).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Explicit Stabilisation for Modular Rely-Guarantee Reasoning

AU - Wickerson, John

AU - Dodds, Mike

AU - Parkinson, Matthew J.

PY - 2010

Y1 - 2010

N2 - We propose a new formalisation of stability for Rely-Guarantee, in which an assertion’s stability is encoded into its syntactic form. This allows two advances in modular reasoning. Firstly, it enables Rely-Guarantee, for the first time, to verify concurrent libraries independently of their clients’ environments. Secondly, in a sequential setting, it allows a module’s internal interference to be hidden while verifying its clients. We demonstrate our approach by verifying, using RGSep, the Version 7 Unix memory manager, uncovering a twenty-year-old bug in the process.

AB - We propose a new formalisation of stability for Rely-Guarantee, in which an assertion’s stability is encoded into its syntactic form. This allows two advances in modular reasoning. Firstly, it enables Rely-Guarantee, for the first time, to verify concurrent libraries independently of their clients’ environments. Secondly, in a sequential setting, it allows a module’s internal interference to be hidden while verifying its clients. We demonstrate our approach by verifying, using RGSep, the Version 7 Unix memory manager, uncovering a twenty-year-old bug in the process.

U2 - 10.1007/978-3-642-11957-6_32

DO - 10.1007/978-3-642-11957-6_32

M3 - Conference contribution

SN - 978-3-642-11956-9

VL - 6012 LNCS

T3 - Lecture Notes in Computer Science

SP - 610

EP - 629

BT - Programming Languages and Systems

PB - Springer

T2 - 19th European Symposium on Programming (ESOP), ETAPS 2010

Y2 - 20 March 2010 through 28 March 2010

ER -

Wickerson J, Dodds M, Parkinson MJ. Explicit Stabilisation for Modular Rely-Guarantee Reasoning. In Programming Languages and Systems: 19th European Symposium on Programming, ESOP 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. Vol. 6012 LNCS. Springer. 2010. p. 610-629. (Lecture Notes in Computer Science). doi: 10.1007/978-3-642-11957-6_32