Library Abstraction for C/C++ Concurrency

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

• Mark Batty
• Monday 03 December 2012, 13:00-14:00
• FW26.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.