Mark Batty
Scott Owens
Susmit Sarkar
Abstract
Shared-memory concurrency in C and C++ is pervasive in systems programming, but has long been poorly defined. This motivated an ongoing shared effort by the standards committees to specify concurrent behaviour in the next versions of both languages. They aim to provide strong guarantees for race-free programs, together with new (but subtle) relaxed-memory atomic primitives for high-performance concurrent code. However, the current draft standards, while the result of careful deliberation, are not yet clear and rigorous definitions, and harbour substantial problems in their details.
In this paper we establish a mathematical (yet readable) semantics for C++ concurrency. We aim to capture the intent of the current (`Final Committee') Draft as closely as possible, but discuss changes that fix many of its problems. We prove that a proposed x86 implementation of the concurrency primitives is correct with respect to the x86-TSO model, and describe our Cppmem tool for exploring the semantics of examples, using code generated from our Isabelle/HOL definitions.
Having already motivated changes to the draft standard, this work will aid discussion of any further changes, provide a correctness condition for compilers, and give a much-needed basis for analysis and verification of concurrent C and C++ programs.
Supplemental Material
- S. V. Adve and H.-J. Boehm. Memory models: A case for rethinking parallel languages and hardware. C. ACM, 2010. Google Scholar
Digital Library
- J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Fences in weak memory models. In Proc. CAV, 2010. Google ScholarDigital Library
- ARM. ARM Architecture Reference Manual (ARMv7-A and ARMv7-R edition). April 2008.Google Scholar
- H.-J. Boehm and S.V. Adve. Foundations of the C++ concurrency memory model. In Proc. PLDI, 2008. Google ScholarDigital Library
- P. Becker, editor. Programming Languages --- C++. Final Committee Draft. 2010. ISO/IEC JTC1 SC22 WG21 N3092.Google Scholar
- Jasmin Christian Blanchette and Tobias Nipkow. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In Proc. ITP, 2010. Google ScholarDigital Library
- www.cl.cam.ac.uk/users/pes20/cpp.Google Scholar
- JTC1/SC22/WG14 --- C. http://www.open-std.org/jtc1/sc22/wg14/.Google Scholar
- P. Cenciarelli, A. Knapp, and E. Sibilio. The Java memory model: Operationally, denotationally, axiomatically. In Proc. ESOP, 2007. Google ScholarDigital Library
- E. R. Gansner and S. C. North. An open graph visualization system and its applications to software engineering. Softw. Pract. Exper., 30(11):1203--1233, 2000. Google ScholarDigital Library
- Florian Haftmann. Code Generation from Specifications in Higher-Order Logic. PhD thesis, TU München, 2009.Google Scholar
- The HOL 4 system. http://hol.sourceforge.net/.Google Scholar
- Intel. A formal specification of Intel Itanium processor family memory ordering. http://www.intel.com/design/itanium/downloads/251429.htm, October 2002.Google Scholar
- Isabelle 2009-2. http://isabelle.in.tum.de/.Google Scholar
- L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput., C-28(9):690--691, 1979. Google ScholarDigital Library
- J. Manson,W. Pugh, and S.V. Adve. The Java memory model. In Proc. POPL, 2005. Google ScholarDigital Library
- P. E. McKenney and R. Silvera. Example POWER implementation for C/C++ memory model. http://www.rdrop.com/users/paulmck/scalability/paper/N2745r.2010.02.19a.html, 2010.Google Scholar
- P. E. McKenney and J. Walpole. What is RCU, fundamentally? Linux Weekly News, http://lwn.net/Articles/262464/.Google Scholar
- George C. Necula, Scott McPeak, Shree Prakash Rahul, and Westley Weimer. Cil: Intermediate language and tools for analysis and transformation of c programs. In Proc. CC, 2002. Google ScholarDigital Library
- M. Norrish. A formal semantics for C++. Technical report, NICTA, 2008.Google Scholar
- S. Owens, S. Sarkar, and P. Sewell. A better x86 memory model: x86-TSO. In Proc. TPHOLs, 2009. Google ScholarDigital Library
- S. Owens. Reasoning about the implementation of concurrency abstractions on x86-TSO. In Proc. ECOOP, 2010. Google ScholarDigital Library
- Power ISA Version 2.06. IBM, 2009.Google Scholar
- W. Pugh. The Java memory model is fatally flawed. Concurrency - Practice and Experience, 12(6), 2000.Google Scholar
- J. Ševçík and D. Aspinall. On validity of program transformations in the Java memory model. In ECOOP, 2008. Google ScholarDigital Library
- The SPARC architecture manual, v. 9. http://dev elopers.sun.com/solaris/articles/sparcv9.pdf. Google ScholarDigital Library
- P. Sewell, S. Sarkar, S. Owens, F. Zappa Nardelli, and M. O. Myreen. x86-TSO: A rigorous and usable programmer's model for x86 multiprocessors. C. ACM, 53(7):89--97, 2010. Google ScholarDigital Library
- S. Sarkar, P. Sewell, F. Zappa Nardelli, S. Owens, T. Ridge, T. Braibant, M. Myreen, and J. Alglave. The semantics of x86-CC multiprocessor machine code. In Proc. POPL, 2009. Google ScholarDigital Library
- A. Terekhov. Brief tentative example x86 implementation for C/C++ memory model. cpp-threads mailing list, http://www.decadent.org.uk/pipermail/cpp-threads/2008-December/001933.html, Dec. 2008.Google Scholar
- E. Torlak and D. Jackson. Kodkod: a relational model finder. In Proc. TACAS, 2007. Google ScholarDigital Library
- E. Torlak, M. Vaziri, and J. Dolby. MemSAT: checking axiomatic specifications of memory models. In PLDI, 2010. Google ScholarDigital Library
- Y. Yang, G. Gopalakrishnan, G. Lindstrom, and K. Slind. Nemos: A framework for axiomatic and executable specifications of memory consistency models. In IPDPS, 2004.Google ScholarCross Ref
- M. Zalewski. Generic Programming with Concepts. PhD thesis, Chalmers University, November 2008.Google Scholar
Index Terms
- Mathematizing C++ concurrency
Recommendations
Mathematizing C++ concurrency
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesShared-memory concurrency in C and C++ is pervasive in systems programming, but has long been poorly defined. This motivated an ongoing shared effort by the standards committees to specify concurrent behaviour in the next versions of both languages. ...
Clarifying and compiling C/C++ concurrency: from C++11 to POWER
POPL '12The upcoming C and C++ revised standards add concurrency to the languages, for the first time, in the form of a subtle *relaxed memory model* (the *C++11 model*). This aims to permit compiler optimisation and to accommodate the differing relaxed-memory ...
Synchronising C/C++ and POWER
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and ImplementationShared memory concurrency relies on synchronisation primitives: compare-and-swap, load-reserve/store-conditional (aka LL/SC), language-level mutexes, and so on. In a sequentially consistent setting, or even in the TSO setting of x86 and Sparc, these ...
Reviews
Wolfgang Schreiner
Integrating multi-threading into a programming language such as C++ is an error-prone task: the intuitive expectation of a "sequentially consistent" program that behaves as if concurrent memory reads and writes were put into some linear order cannot be satisfied, because modern compilers and processors need the flexibility to reorder instructions or delay memory updates. To support high-performance concurrent algorithms, the forthcoming C++0x standard defines atomic synchronization primitives with a weaker semantics, which is difficult to understand. Establishing the correctness of a compiler is thus a challenging task. This paper addresses the problem by providing a formal model of C++0x concurrency. A program is translated into the set of its possible executions, which are defined by mathematical relations among the program's memory actions and must satisfy certain correctness constraints such as freedom of data races. The authors give a detailed explanation of the formalization and present various examples that illustrate the semantics of typical programming patterns. The formalization is expressed in the proving environment Isabelle/HOL and automatically translated into the core of the CPPMEM tool, which produces from a C++0x program a visualization of its possible executions. Throughout the formalization process, the authors collaborated with the C++ standardization committee to clarify various subtle features, inconsistencies, and errors in the proposed standard and to prove the correctness of a proposed x86 implementation of the concurrency primitives. The presented formalization can thus provide a much-needed reference for the implementation of the standard and for the analysis of concurrent C++ programs. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments