By the same authors

Library abstraction for C/C++ concurrency

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

Author(s)

Department/unit(s)

Publication details

Title of host publicationPOPL '13
DatePublished - 2013
Pages235-248
Number of pages14
PublisherACM
Place of PublicationNew York
Original languageEnglish
ISBN (Electronic)9781450318327

Abstract

When constructing complex concurrent systems, abstraction is vital:
programmers should be able to reason about concurrent libraries in terms of
abstract specifications that hide the implementation details. Relaxed memory
models present substantial challenges in this respect, as libraries need not
provide sequentially consistent abstractions: to avoid unnecessary
synchronisation, they may allow clients to observe relaxed memory effects, and
library specifications must capture these.

In this paper, we propose a criterion for sound library abstraction in the new
C11 and C++11 memory model, generalising the standard sequentially
consistent notion of linearizability. We prove that our criterion soundly
captures all client-library interactions, both through call and return values,
and through the subtle synchronisation effects arising from the memory
model. To illustrate our approach, we verify implementations against
specifications for the lock-free Treiber stack and a producer-consumer
queue. Ours is the first approach to compositional reasoning for concurrent
C11/C++11 programs.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations