Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Mathematizing C++ concurrency
Batty M., Owens S., Sarkar S., Sewell P., Weber T. ACM SIGPLAN Notices46 (1):55-66,2011.Type:Article
Date Reviewed: Apr 5 2011

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.

Reviewer:  Wolfgang Schreiner Review #: CR138958 (1110-1047)
Bookmark and Share
  Featured Reviewer  
 
Multiple Data Stream Architectures (Multiprocessors) (C.1.2 )
 
 
Concurrent Programming (D.1.3 )
 
 
Specifying And Verifying And Reasoning About Programs (F.3.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Multiple Data Stream Architectures (Multiprocessors)": Date
Cache-coherent multiprocessors
Baskett F., University Video Communications, Stanford, CA, 1991. Type: Book
Feb 1 1994
Multiple processor systems for real-time applications
Liebowitz B., Carson J., Prentice-Hall, Inc., Upper Saddle River, NJ, 1985. Type: Book (9789780136051145)
Jan 1 1986
Multicomputer networks: message-based parallel processing
Reed D., Fujimoto R., MIT Press, Cambridge, MA, 1988. Type: Book (9789780262181297)
Apr 1 1989
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy