Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Formal verification of object layout for C++ multiple inheritance
Ramananandro T., Dos Reis G., Leroy X.  ACM SIGPLAN Notices 46 (1): 67-80, 2011. Type: Article
Date Reviewed: Dec 13 2011

Efficient language translation, optimized code generation, and runtime memory layout are cornerstones of modern computer language compilers. Squeezing a user’s data structures, especially with C++ multiple inheritance, into fewer but efficiently accessed bits leads to smaller footprints needed for newer mobile and embedded applications. However, proving that the compiler is managing the correct bit layout has been lacking for C++.

This paper provides a formal verification approach based on semantic foundations that justify new layout optimizations. It introduces families of various memory layout algorithms and describes them by means of an operational semantics notation that is complex but still independent of the target architecture. These extensive formal layout details, provided using the Coq proof tools and the resulting semantic preservation correctness proofs, are a valuable contribution to the compiler field.

Compiler technology has come a long way from the classic optimization steps of the basic language for implementation of system software (BLISS) compiler or the famous Nicholas Wirth Pascal compilers (with comments written in German). Though this paper provides some overview of previous C++ memory layout solutions, the authors’ main contribution is their formal semantic proofs for complex multiple inheritance memory layouts.

Reviewer:  Scott Moody Review #: CR139669 (1205-0496)
Bookmark and Share
Compilers (D.3.4 ... )
Classes And Objects (D.3.3 ... )
Correctness Proofs (D.2.4 ... )
Data Storage Representations (E.2 )
Language Constructs and Features (D.3.3 )
Object Representation (E.2 ... )
Would you recommend this review?
Other reviews under "Compilers": Date
Introduction to compiler construction in a Java world
Campbell B., Iyer S., Akbal-Delibas B.,  Chapman & Hall/CRC, Boca Raton, FL, 2013. 381 pp. Type: Book (978-1-439860-88-5)
Sep 10 2013
Compiler design: analysis and transformation
Wilhelm R., Seidl H., Hack S.,  Springer Publishing Company, Incorporated, New York, NY, 2012. 189 pp. Type: Book (978-3-642175-47-3)
Apr 30 2013
A modular approach to on-stack replacement in LLVM
Lameed N., Hendren L.  VEE 2013 (Proceedings of the 9th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments, Houston, TX,  Mar 16-17, 2013) 143-154, 2013. Type: Proceedings
Apr 18 2013

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2014 ThinkLoud, Inc.
Terms of Use
| Privacy Policy