Abstract
The C11 standard of the C programming language describes dynamic typing restrictions on memory operations to make more effective optimizations based on alias analysis possible. These restrictions are subtle due to the low-level nature of C, and have not been treated in a formal semantics before. We present an executable formal memory model for C that incorporates these restrictions, and at the same time describes required low-level operations.
Our memory model and essential properties of it have been fully formalized using the Coq proof assistant.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Affeldt, R., Marti, N.: Towards formal verification of TLS network packet processing written in C. In: PLPV, pp. 35–46 (2013)
Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL, pp. 55–66 (2011)
Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533–544 (2012)
GNU. GCC, the GNU Compiler Collection (2011), http://gcc.gnu.org/
International Organization for Standardization. WG14 Defect Report Summary (2008), http://www.open-std.org/jtc1/sc22/wg14/www/docs/
International Organization for Standardization. ISO/IEC 9899-2011: Programming languages – C. ISO Working Group 14 (2012)
Krebbers, R.: An operational and axiomatic semantics for non-determinism and sequence points in C. To appear in: POPL 2014 (2013)
Krebbers, R., Wiedijk, F.: A Formalization of the C99 Standard in HOL, Isabelle and Coq. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus/MKM 2011. LNCS (LNAI), vol. 6824, pp. 301–303. Springer, Heidelberg (2011)
Krebbers, R., Wiedijk, F.: Separation Logic for Non-local Control Flow and Block Scope Variables. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol. 7794, pp. 257–272. Springer, Heidelberg (2013)
Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert Memory Model, Version 2. Research report RR-7987, INRIA (2012)
Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. JAR 41(1), 1–31 (2008)
Maclaren, N.: What is an Object in C Terms?, Mailing list message (2001), http://www.open-std.org/jtc1/sc22/wg14/9350
Nita, M., Grossman, D., Chambers, C.: A theory of platform-dependent low-level software. In: POPL, pp. 209–220 (2008)
Norrish, M.: C formalised in HOL. PhD thesis, University of Cambridge (1998)
Ramananandro, T., Dos Reis, G., Leroy, X.: Formal verification of object layout for C++ multiple inheritance. In: POPL, pp. 67–80 (2011)
Robert, V., Leroy, X.: A Formally-Verified Alias Analysis. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 11–26. Springer, Heidelberg (2012)
Rossie, J.G., Friedman, D.P.: An Algebraic Semantics of Subobjects. In: OOPSLA, pp. 187–199 (1995)
Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL, pp. 97–108 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Krebbers, R. (2013). Aliasing Restrictions of C11 Formalized in Coq. In: Gonthier, G., Norrish, M. (eds) Certified Programs and Proofs. CPP 2013. Lecture Notes in Computer Science, vol 8307. Springer, Cham. https://doi.org/10.1007/978-3-319-03545-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-03545-1_4
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-03544-4
Online ISBN: 978-3-319-03545-1
eBook Packages: Computer ScienceComputer Science (R0)