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.
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.
| Original language | English |
|---|---|
| Title of host publication | POPL '13 |
| Subtitle of host publication | Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages |
| Place of Publication | New York |
| Publisher | ACM |
| Pages | 235-248 |
| Number of pages | 14 |
| ISBN (Electronic) | 9781450318327 |
| DOIs | |
| Publication status | Published - 2013 |
| Event | 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '13) - Rome, Italy Duration: 23 Jan 2013 → 25 Jan 2013 |
Conference
| Conference | 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '13) |
|---|---|
| Country/Territory | Italy |
| City | Rome |
| Period | 23/01/13 → 25/01/13 |