Concurrent abstract predicates

Thomas Dinsdale-Young; Michael David Dodds; Philippa Gardner; Matthew J. Parkinson; Viktor Vafeiadis

doi:10.1007/978-3-642-14107-2_24

Concurrent abstract predicates

Thomas Dinsdale-Young, Michael David Dodds, Philippa Gardner, Matthew J. Parkinson, Viktor Vafeiadis

Computer Science

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

Abstract

Abstraction is key to understanding and reasoning about large computer systems. Abstraction is simple to achieve if the relevant data structures are disjoint, but rather difficult when they are partially shared, as is often the case for concurrent modules. We present a program logic for reasoning abstractly about data structures that provides a fiction of disjointness and permits compositional reasoning. The internal details of a module are completely hidden from the client by concurrent abstract predicates. We reason about a module’s implementation using separation logic with permissions, and provide abstract specifications for use by client programs using concurrent abstract predicates. We illustrate our abstract reasoning by building two implementations of a lock module on top of hardware instructions, and two implementations of a concurrent set module on top of the lock module.

Original language	English
Title of host publication	ECOOP 2010 – Object-Oriented Programming
Subtitle of host publication	24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings
Publisher	Springer
Pages	504-528
Number of pages	25
ISBN (Electronic)	978-3-642-14107-2
ISBN (Print)	978-3-642-14106-5
DOIs	https://doi.org/10.1007/978-3-642-14107-2_24
Publication status	Published - 2010
Event	24th European Conference on Object-Oriented Programming (ECOOP 2010) - Maribor, Slovenia Duration: 21 Jun 2010 → 25 Jun 2010

Publication series

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

Conference

Conference	24th European Conference on Object-Oriented Programming (ECOOP 2010)
Country/Territory	Slovenia
City	Maribor
Period	21/06/10 → 25/06/10

Access to Document

10.1007/978-3-642-14107-2_24

http://link.springer.com/chapter/10.1007%2F978-3-642-14107-2_24

Cite this

@inproceedings{4324cef35657407cba02c5de3b5c326e,

title = "Concurrent abstract predicates",

abstract = "Abstraction is key to understanding and reasoning about large computer systems. Abstraction is simple to achieve if the relevant data structures are disjoint, but rather difficult when they are partially shared, as is often the case for concurrent modules. We present a program logic for reasoning abstractly about data structures that provides a fiction of disjointness and permits compositional reasoning. The internal details of a module are completely hidden from the client by concurrent abstract predicates. We reason about a module{\textquoteright}s implementation using separation logic with permissions, and provide abstract specifications for use by client programs using concurrent abstract predicates. We illustrate our abstract reasoning by building two implementations of a lock module on top of hardware instructions, and two implementations of a concurrent set module on top of the lock module.",

author = "Thomas Dinsdale-Young and Dodds, {Michael David} and Philippa Gardner and Parkinson, {Matthew J.} and Viktor Vafeiadis",

year = "2010",

doi = "10.1007/978-3-642-14107-2_24",

language = "English",

isbn = "978-3-642-14106-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "504--528",

booktitle = "ECOOP 2010 – Object-Oriented Programming",

address = "Germany",

note = "24th European Conference on Object-Oriented Programming (ECOOP 2010) ; Conference date: 21-06-2010 Through 25-06-2010",

}

Dinsdale-Young, T, Dodds, MD, Gardner, P, Parkinson, MJ & Vafeiadis, V 2010, Concurrent abstract predicates. in ECOOP 2010 – Object-Oriented Programming : 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6183, Springer, pp. 504-528, 24th European Conference on Object-Oriented Programming (ECOOP 2010), Maribor, Slovenia, 21/06/10. https://doi.org/10.1007/978-3-642-14107-2_24

Concurrent abstract predicates. / Dinsdale-Young, Thomas; Dodds, Michael David; Gardner, Philippa et al.
ECOOP 2010 – Object-Oriented Programming : 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings. Springer, 2010. p. 504-528 (Lecture Notes in Computer Science; Vol. 6183).

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

TY - GEN

T1 - Concurrent abstract predicates

AU - Dinsdale-Young, Thomas

AU - Dodds, Michael David

AU - Gardner, Philippa

AU - Parkinson, Matthew J.

AU - Vafeiadis, Viktor

PY - 2010

Y1 - 2010

N2 - Abstraction is key to understanding and reasoning about large computer systems. Abstraction is simple to achieve if the relevant data structures are disjoint, but rather difficult when they are partially shared, as is often the case for concurrent modules. We present a program logic for reasoning abstractly about data structures that provides a fiction of disjointness and permits compositional reasoning. The internal details of a module are completely hidden from the client by concurrent abstract predicates. We reason about a module’s implementation using separation logic with permissions, and provide abstract specifications for use by client programs using concurrent abstract predicates. We illustrate our abstract reasoning by building two implementations of a lock module on top of hardware instructions, and two implementations of a concurrent set module on top of the lock module.

AB - Abstraction is key to understanding and reasoning about large computer systems. Abstraction is simple to achieve if the relevant data structures are disjoint, but rather difficult when they are partially shared, as is often the case for concurrent modules. We present a program logic for reasoning abstractly about data structures that provides a fiction of disjointness and permits compositional reasoning. The internal details of a module are completely hidden from the client by concurrent abstract predicates. We reason about a module’s implementation using separation logic with permissions, and provide abstract specifications for use by client programs using concurrent abstract predicates. We illustrate our abstract reasoning by building two implementations of a lock module on top of hardware instructions, and two implementations of a concurrent set module on top of the lock module.

UR - http://www.scopus.com/inward/record.url?scp=77955014696&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-14107-2_24

DO - 10.1007/978-3-642-14107-2_24

M3 - Conference contribution

SN - 978-3-642-14106-5

T3 - Lecture Notes in Computer Science

SP - 504

EP - 528

BT - ECOOP 2010 – Object-Oriented Programming

PB - Springer

T2 - 24th European Conference on Object-Oriented Programming (ECOOP 2010)

Y2 - 21 June 2010 through 25 June 2010

ER -

Concurrent abstract predicates

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this