Tahina Ramananandro
Xavier Leroy
ABSTRACT
Object layout - the concrete in-memory representation of objects - raises many delicate issues in the case of the C++ language, owing in particular to multiple inheritance, C compatibility and separate compilation. This paper formalizes a family of C++ object layout schemes and mechanically proves their correctness against the operational semantics for multiple inheritance of Wasserrab et al. This formalization is flexible enough to account for space-saving techniques such as empty base class optimization and tail-padding optimization. As an application, we obtain the first formal correctness proofs for realistic, optimized object layout algorithms, including one based on the popular "common vendor" Itanium C++ application binary interface. This work provides semantic foundations to discover and justify new layout optimizations; it is also a first step towards the verification of a C++ compiler front-end.
Supplemental Material
- S. Blazy and X. Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263--288, 2009.Google Scholar
Cross Ref
- J. Chen. A typed intermediate language for compiling multiple inheritance. In 34th symp. Principles of Programming Languages, pages 25--30. ACM, 2007. Google ScholarDigital Library
- CodeSourcery, Compaq, EDG, HP, IBM, Intel, Red Hat, and SGI. Itanium C++ ABI, 2001. URL http://www.codesourcery.com/public/cxx-abi.Google Scholar
- B. Dawes. PODs Revisited; Resolving Core Issue 568 (Revision 2). Technical report, ISO/IEC SC22/JTC1/WG21, March 2007. URL http://www.open-std.org/JTC1/SC22/WG21/docs/papers/2007/n2172.html.Google Scholar
- M. A. Ellis and B. Stroustrup. The Annotated C++ Reference Manual. Addison-Wesley, 1990. Google ScholarDigital Library
- J. Gil and P. F. Sweeney. Space and time-efficient memory layout for multiple inheritance. In 14th conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 1999), pages 256--275. ACM, 1999. Google ScholarDigital Library
- J. Y. Gil, W. Pugh, G. E. Weddell, and Y. Zibin. Two-dimensional bidirectional object layout. ACM Trans. Program. Lang. Syst., 30(5): 1--38, 2008. Google ScholarDigital Library
- International Standard ISO/IEC 14882:2003. Programming Languages C++. International Organization for Standards, 2003.Google Scholar
- G. Klein and T. Nipkow. A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Prog. Lang. Syst., 28(4):619--695, 2006. Google ScholarDigital Library
- D. Leinenbach, W. Paul, and E. Petrova. Towards the formal verification of a C0 compiler: Code generation and implementation correctness. In Int. Conf. on Software Engineering and Formal Methods (SEFM 2005), pages 2--11. IEEE, 2005. Google ScholarDigital Library
- X. Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107--115, 2009. Google ScholarDigital Library
- C. Luo and S. Qin. Separation Logic for Multiple Inheritance. Electron. Notes Theor. Comput. Sci., 212:27--40, 2008. Google ScholarDigital Library
- N. Myers. The empty member C++ optimization. Dr Dobbs Journal, Aug. 1997. URL http://www.cantrip.org/emptyopt.html.Google Scholar
- G. Ramalingam and H. Srinivasan. A member lookup algorithm for C++. In Programming Language Design and Implementation (PLDI97), pages 18--30. ACM, 1997. Google ScholarDigital Library
- T. Ramananandro. Formal verification of object layout for C++ multiple inheritance Coq development and supplementary material, 2010. URL http://gallium.inria.fr/~tramanan/cxx/. Google ScholarDigital Library
- J. G. Rossie and D. P. Friedman. An algebraic semantics of subobjects. In 10th conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 1995), pages 187--199. ACM, 1995. Google ScholarDigital Library
- P. F. Sweeney and M. G. Burke. Quantifying and evaluating the space overhead for alternative C++ memory layouts. Software: Practice and Experience, 33(7):595--636, 2003. Google ScholarDigital Library
- H. Tuch. Formal verification of C systems code: Structured types, separation logic and theorem proving. Journal of Automated Reasoning, 42(2):125--187, 2009. Google ScholarDigital Library
- D. Wasserrab, T. Nipkow, G. Snelting, and F. Tip. An operational semantics and type safety proof for multiple inheritance in C++. In 21st conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2006), pages 345--362. ACM, 2006. Google ScholarDigital Library
Index Terms
- Formal verification of object layout for c++ multiple inheritance
Recommendations
An operational semantics and type safety prooffor multiple inheritance in C++
OOPSLA '06: Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applicationsWe present an operational semantics and type safety proof for multiple inheritance in C++. The semantics models the behaviour of method calls, field accesses, and two forms of casts in C++ class hierarchies exactly, and the type safety proof was ...
Formal verification of object layout for c++ multiple inheritance
POPL '11Object layout - the concrete in-memory representation of objects - raises many delicate issues in the case of the C++ language, owing in particular to multiple inheritance, C compatibility and separate compilation. This paper formalizes a family of C++ ...
An operational semantics and type safety prooffor multiple inheritance in C++
Proceedings of the 2006 OOPSLA ConferenceWe present an operational semantics and type safety proof for multiple inheritance in C++. The semantics models the behaviour of method calls, field accesses, and two forms of casts in C++ class hierarchies exactly, and the type safety proof was ...
Reviews
Scott Arthur Moody
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. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments