Mark Batty
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.
Supplemental Material
- M. Batty, M. Dodds, and A. Gotsman. Library abstraction for C/C++ concurrency (extended version). University of York Technical Report YCS-2012-479, 2012.Google Scholar
- M. Batty, S. Owens, S. Sarkar, P. Sewell, and T.Weber. Mathematizing C++ concurrency. In POPL, 2011. Google ScholarDigital Library
- H.-J. Boehm. Can seqlocks get along with programming language memory models? In MSPC, 2012. Google ScholarDigital Library
- H.-J. Boehm and S. V. Adve. Foundations of the C++ concurrency memory model. In PLDI, 2008. Google ScholarDigital Library
- S. Burckhardt, A. Gotsman, M. Musuvathi, and H. Yang. Concurrent library correctness on the TSO memory model. In ESOP, 2012. Google ScholarDigital Library
- S. Burckhardt, D. Leijen, M. Fahndrich, and M. Sagiv. Eventually consistent transactions. In ESOP, 2012. Google ScholarDigital Library
- I. Filipović, P. O'Hearn, N. Rinetzky, and H. Yang. Abstraction for concurrent objects. In ESOP, 2009. Google ScholarDigital Library
- I. Filipović, P. O'Hearn, N. Torp-Smith, and H. Yang. Blaiming the client: On data refinement in the presence of pointers. FAC, 22, 2010. Google ScholarCross Ref
- A. Gotsman and H. Yang. Liveness-preserving atomicity abstraction. In ICALP, 2011. Google ScholarDigital Library
- A. Gotsman and H. Yang. Linearizability with ownership transfer. In CONCUR, 2012. Google ScholarDigital Library
- M. P. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. TOPLAS, 12, 1990. Google ScholarDigital Library
- ISO/IEC. Programming Languages -- C++, 14882:2011.Google Scholar
- ISO/IEC. Programming Languages -- C, 9899:2011.Google Scholar
- M. Kuperstein,M. T. Vechev, and E. Yahav. Partial-coherence abstractions for relaxed memory models. In PLDI, 2011. Google ScholarDigital Library
- L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comp., 28, 1979. Google ScholarDigital Library
- J. Manson. The Java memory model. PhD Thesis. Department of Computer Science, University of Maryland, 2004. Google ScholarDigital Library
- M. M. Michael. Scalable lock-free dynamic memory allocation. In PLDI, 2004. Google ScholarDigital Library
- M. M. Michael, M. T. Vechev, and V. A. Saraswat. Idempotent work stealing. In PPOPP, 2009. Google ScholarDigital Library
- S. Owens, S. Sarkar, and P. Sewell. A better x86 memory model: x86- TSO. In TPHOLs, 2009.. Google ScholarDigital Library
- T. Ridge. A rely-guarantee proof system for x86-TSO. In VSTTE, 2010. Google ScholarDigital Library
- S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D.Williams. Understanding POWER multiprocessors. In PLDI, 2011. Google ScholarDigital Library
- R. K. Treiber. Systems programming: Coping with parallelism. Technical Report RJ 5118, IBM Almaden Research Center, 1986.Google Scholar
- . Wehrman and J. Berdine. A proposal for weak-memory local reasoning. In LOLA, 2011.Google Scholar
Index Terms
- Library abstraction for C/C++ concurrency
Recommendations
Foundations of the C++ concurrency memory model
PLDI '08Currently multi-threaded C or C++ programs combine a single-threaded programming language with a separate threads library. This is not entirely sound [7].
We describe an effort, currently nearing completion, to address these issues by explicitly ...
Library abstraction for C/C++ concurrency
POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWhen 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 ...
Certified concurrent abstraction layers
PLDI '18Concurrent abstraction layers are ubiquitous in modern computer systems because of the pervasiveness of multithreaded programming and multicore hardware. Abstraction layers are used to hide the implementation details (e.g., fine-grained synchronization) ...
Reviews
Andrea F Paramithiotti
Abstraction is a useful concept in programming, in that programmers often only need to know what a given module does without being concerned about the internals of that module. This is key to modularization, or building software applications by putting together pieces of existing code, saving time and effort. Modularization often involves building libraries, or sets of predefined functions. Libraries have been in use since the beginning in many programming languages, especially in C/C++. C/C++ libraries, however, usually provide sequentially consistent abstractions, where tasks are performed one after the other. On the other hand, many modern programs and applications require concurrency, enabling the performance of tasks in no particular order. Current libraries do not provide many such services. This paper proposes a model for such libraries. Of course, this is academic work. The authors describe a model, not a set of libraries readily downloadable from a website. It is part of ongoing work by the authors in response to challenges from the academic world at large. It also provides some practical advice about program verification: it should be used not to ensure that software behaves as expected (which is simply impossible!), but merely to determine if it conforms to its specifications. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments