Deny-Guarantee Reasoning

Michael David Dodds; Xinyu Feng; Matthew J. Parkinson; Viktor Vafeiadis

doi:10.1007/978-3-642-00590-9_26

Deny-Guarantee Reasoning

Michael David Dodds, Xinyu Feng, Matthew J. Parkinson, Viktor Vafeiadis

Computer Science

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

Abstract

Rely-guarantee is a well-established approach to reasoning about concurrent
programs that use parallel composition. However, parallel composition is not how concurrency is structured in real systems. Instead, threads are started by ‘fork’ and collected with ‘join’ commands. This style of concurrency cannot be
reasoned about using rely-guarantee, as the life-time of a thread can be scoped
dynamically. With parallel composition the scope is static.
In this paper, we introduce deny-guarantee reasoning, a reformulation of relyguarantee that enables reasoning about dynamically scoped concurrency.We build on ideas from separation logic to allow interference to be dynamically split and recombined, in a similar way that separation logic splits and joins heaps. To allow this splitting, we use deny and guarantee permissions: a deny permission specifies that the environment cannot do an action, and guarantee permission allow us to do an action. We illustrate the use of our proof system with examples, and show that it can encode all the original rely-guarantee proofs.We also present the semantics and soundness of the deny-guarantee method.

Original language	English
Title of host publication	Programming Languages and Systems, 18th European Symposium on Programming
Subtitle of host publication	ESOP 2009
Place of Publication	Springer New York
Publisher	Springer
Pages	363-377
Number of pages	15
Volume	5502
ISBN (Electronic)	978-3-642-00590-9
ISBN (Print)	978-3-642-00589-3
DOIs	https://doi.org/10.1007/978-3-642-00590-9_26
Publication status	Published - 2009
Event	Programming Languages and Systems : 18th European Symposium on Programming - York (UK), United Kingdom Duration: 22 Mar 2009 → 29 Mar 2009

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	5502

Conference

Conference	Programming Languages and Systems : 18th European Symposium on Programming
Country/Territory	United Kingdom
City	York (UK)
Period	22/03/09 → 29/03/09

Access to Document

10.1007/978-3-642-00590-9_26

http://link.springer.com/chapter/10.1007%2F978-3-642-00590-9_26

Cite this

@inproceedings{4ae5604e262b4c09ba705c4b184136d5,

title = "Deny-Guarantee Reasoning",

abstract = "Rely-guarantee is a well-established approach to reasoning about concurrentprograms that use parallel composition. However, parallel composition is not how concurrency is structured in real systems. Instead, threads are started by {\textquoteleft}fork{\textquoteright} and collected with {\textquoteleft}join{\textquoteright} commands. This style of concurrency cannot bereasoned about using rely-guarantee, as the life-time of a thread can be scopeddynamically. With parallel composition the scope is static. In this paper, we introduce deny-guarantee reasoning, a reformulation of relyguarantee that enables reasoning about dynamically scoped concurrency.We build on ideas from separation logic to allow interference to be dynamically split and recombined, in a similar way that separation logic splits and joins heaps. To allow this splitting, we use deny and guarantee permissions: a deny permission specifies that the environment cannot do an action, and guarantee permission allow us to do an action. We illustrate the use of our proof system with examples, and show that it can encode all the original rely-guarantee proofs.We also present the semantics and soundness of the deny-guarantee method.",

author = "Dodds, {Michael David} and Xinyu Feng and Parkinson, {Matthew J.} and Viktor Vafeiadis",

year = "2009",

doi = "10.1007/978-3-642-00590-9_26",

language = "English",

isbn = "978-3-642-00589-3",

volume = "5502",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "363--377",

booktitle = "Programming Languages and Systems, 18th European Symposium on Programming",

address = "Germany",

note = "Programming Languages and Systems : 18th European Symposium on Programming ; Conference date: 22-03-2009 Through 29-03-2009",

}

Dodds, MD, Feng, X, Parkinson, MJ & Vafeiadis, V 2009, Deny-Guarantee Reasoning. in Programming Languages and Systems, 18th European Symposium on Programming: ESOP 2009. vol. 5502, Lecture Notes in Computer Science, vol. 5502, Springer, Springer New York, pp. 363-377, Programming Languages and Systems : 18th European Symposium on Programming, York (UK), United Kingdom, 22/03/09. https://doi.org/10.1007/978-3-642-00590-9_26

Deny-Guarantee Reasoning. / Dodds, Michael David; Feng, Xinyu; Parkinson, Matthew J. et al.
Programming Languages and Systems, 18th European Symposium on Programming: ESOP 2009. Vol. 5502 Springer New York: Springer, 2009. p. 363-377 (Lecture Notes in Computer Science; Vol. 5502).

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

TY - GEN

T1 - Deny-Guarantee Reasoning

AU - Dodds, Michael David

AU - Feng, Xinyu

AU - Parkinson, Matthew J.

AU - Vafeiadis, Viktor

PY - 2009

Y1 - 2009

N2 - Rely-guarantee is a well-established approach to reasoning about concurrentprograms that use parallel composition. However, parallel composition is not how concurrency is structured in real systems. Instead, threads are started by ‘fork’ and collected with ‘join’ commands. This style of concurrency cannot bereasoned about using rely-guarantee, as the life-time of a thread can be scopeddynamically. With parallel composition the scope is static. In this paper, we introduce deny-guarantee reasoning, a reformulation of relyguarantee that enables reasoning about dynamically scoped concurrency.We build on ideas from separation logic to allow interference to be dynamically split and recombined, in a similar way that separation logic splits and joins heaps. To allow this splitting, we use deny and guarantee permissions: a deny permission specifies that the environment cannot do an action, and guarantee permission allow us to do an action. We illustrate the use of our proof system with examples, and show that it can encode all the original rely-guarantee proofs.We also present the semantics and soundness of the deny-guarantee method.

AB - Rely-guarantee is a well-established approach to reasoning about concurrentprograms that use parallel composition. However, parallel composition is not how concurrency is structured in real systems. Instead, threads are started by ‘fork’ and collected with ‘join’ commands. This style of concurrency cannot bereasoned about using rely-guarantee, as the life-time of a thread can be scopeddynamically. With parallel composition the scope is static. In this paper, we introduce deny-guarantee reasoning, a reformulation of relyguarantee that enables reasoning about dynamically scoped concurrency.We build on ideas from separation logic to allow interference to be dynamically split and recombined, in a similar way that separation logic splits and joins heaps. To allow this splitting, we use deny and guarantee permissions: a deny permission specifies that the environment cannot do an action, and guarantee permission allow us to do an action. We illustrate the use of our proof system with examples, and show that it can encode all the original rely-guarantee proofs.We also present the semantics and soundness of the deny-guarantee method.

U2 - 10.1007/978-3-642-00590-9_26

DO - 10.1007/978-3-642-00590-9_26

M3 - Conference contribution

SN - 978-3-642-00589-3

VL - 5502

T3 - Lecture Notes in Computer Science

SP - 363

EP - 377

BT - Programming Languages and Systems, 18th European Symposium on Programming

PB - Springer

CY - Springer New York

T2 - Programming Languages and Systems : 18th European Symposium on Programming

Y2 - 22 March 2009 through 29 March 2009

ER -