Concurrent abstract predicates

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 languageEnglish
Title of host publicationECOOP 2010 – Object-Oriented Programming
Subtitle of host publication24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings
Number of pages25
ISBN (Electronic)978-3-642-14107-2
ISBN (Print)978-3-642-14106-5
Publication statusPublished - 2010
Event24th European Conference on Object-Oriented Programming (ECOOP 2010) - Maribor, Slovenia
Duration: 21 Jun 201025 Jun 2010

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conference24th European Conference on Object-Oriented Programming (ECOOP 2010)

Cite this