COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |
University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > A Verified CompCert Front-End for a Memory Model supporting Pointer Arithmetic and Uninitialised Data
A Verified CompCert Front-End for a Memory Model supporting Pointer Arithmetic and Uninitialised DataAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Dominic Mulligan. The CompCert C compiler guarantees that the target program behaves as the source program. Yet, source programs without a defined semantics do not benefit from this guarantee and could therefore be miscompiled. To reduce the possibility of a miscompilation, we propose a novel memory model for CompCert which gives a defined semantics to challenging features such as bitwise pointer arithmetics and access to uninitialised data. We evaluate our memory model both theoretically and experimentally. In our experiments, we identify pervasive low-level C idioms that require the additional expressiveness provided by our memory model. We also show that our memory model provably subsumes the existing CompCert memory model thus cross-validating both semantics. Our memory model relies on the core concepts of symbolic value and normalisation. A symbolic value models a delayed computation and the normalisation turns, when possible, a symbolic value into a genuine value. We show how to tame the expressive power of the normalisation so that the memory model fits the proof framework of CompCert. We also adapt the proofs of correctness of the compiler passes performed by CompCert’s front-end, thus demonstrating that our model is well-suited for proving compiler transformations. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsPersian Society talks The obesity epidemic: Discussing the global health crisis Cambridge Victorian Studies Group Cambridge Assessment Network ELCF - Engineering for a Low Carbon Future (seminar series) Cambridge Network Healthcare SIGOther talksThe Beginning of Our Universe and what we don't know about Physics Eurostar with Philippe Mouly Big and small history in the Genizah: how necessary is the Cairo Genizah to writing the history of the Medieval Mediterranean? MRI in large animals: a new imaging model Finding meaning in English writing |