University of Cambridge > > Semantics Lunch (Computer Laboratory) > Library Abstraction for C/C++ Concurrency

Library Abstraction for C/C++ Concurrency

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Peter Sewell.

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.

This talk describes a criterion for sound library abstraction in the new C11 memory model, generalising the standard sequentially consistent notion of linearizability. We have proved 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 the approach, a specification and verified implementation of the lock-free Treiber stack will be described. Ours is the first approach to compositional reasoning for concurrent C11 programs.

This is joint work with Mike Dodds and Alexey Gotsman.

This is a POPL practice talk, so should fit into a 30 minute slot. Comments are welcome!

This talk is part of the Semantics Lunch (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity