Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Formal verification of object layout for C++ multiple inheritance
Ramananandro T., Dos Reis G., Leroy X. ACM SIGPLAN Notices46 (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
  Featured Reviewer  
 
Compilers (D.3.4 ... )
 
 
Classes And Objects (D.3.3 ... )
 
 
Correctness Proofs (D.2.4 ... )
 
 
Object Representation (E.2 ... )
 
 
Object-Oriented Constructs (F.3.3 ... )
 
 
Language Constructs and Features (D.3.3 )
 
  more  
Would you recommend this review?
yes
no
Other reviews under "Compilers": Date
An architecture for combinator graph reduction
Philip John J., Academic Press Prof., Inc., San Diego, CA, 1990. Type: Book (9780124192409)
Feb 1 1992
Crafting a compiler with C
Fischer C., Richard J. J., Benjamin-Cummings Publ. Co., Inc., Redwood City, CA, 1991. Type: Book (9780805321661)
Feb 1 1992
A methodology and notation for compiler front end design
Brown C., Paul W. J. Software--Practice & Experience 14(4): 335-346, 1984. Type: Article
Jun 1 1985
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