{"id":4753,"date":"2015-02-04T07:03:13","date_gmt":"2015-02-04T06:03:13","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4753"},"modified":"2015-02-04T07:03:13","modified_gmt":"2015-02-04T06:03:13","slug":"resena-verifying-fast-and-sparse-ssa-based-optimizations-in-coq","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-verifying-fast-and-sparse-ssa-based-optimizations-in-coq\/","title":{"rendered":"Rese\u00f1a: Verifying fast and sparse SSA-based optimizations in Coq"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre<br \/>\ncompiladores titulado <a href=\"http:\/\/www.irisa.fr\/celtique\/pichardie\/papers\/cc15.pdf\">Verifying fast and sparse SSA-based optimizations in Coq <\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.irisa.fr\/celtique\/demange\/index.php\">Delphine Demange<\/a>, <a href=\"http:\/\/www.irisa.fr\/celtique\/pichardie\">David Pichardie<\/a> y L\u00e9o Stefanesco (del grupo <a href=\"http:\/\/www.irisa.fr\/celtique\">Celtique<\/a> en el INRIA Rennes, Francia).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  The Static Single Assignment (SSA) form is a predominant technology in modern compilers, enabling powerful and fast program optimizations. Despite its great success in the implementation of pro- duction compilers, it is only very recently that this technique has been introduced in verified compilers. As of today, few evidence exist on that, in this context, it also allows faster and simpler optimizations. This work builds on the CompCertSSA verified compiler (an SSA branch of the verified CompCert C compiler). We implement and verify two prevail- ing SSA optimizations: Sparse Conditional Constant Propagation and Global Value Numbering. For both transformations, we mechanically prove their soundness in the Coq proof assistant. Both optimization proofs are embedded in a single sparse optimization framework, factoring out many of the dominance-based reasoning steps required in proofs of SSA-based optimizations. Our experimental evaluations indicate both a better precision, and a significant compilation time speedup.\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 en  <a href=\"http:\/\/www.etaps.org\/index.php\/2015\/cc\">CC 2015<\/a> (<em>24th International Conference on Compiler Construction<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Coq se encuentra <a href=\"http:\/\/www.irisa.fr\/celtique\/ext\/ssa_opt\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre compiladores titulado Verifying fast and sparse SSA-based optimizations in Coq . Sus autores son Delphine Demange, David Pichardie y L\u00e9o Stefanesco (del grupo Celtique en el INRIA Rennes, Francia). Su resumen es The Static Single Assignment (SSA) form is a predominant technology in modern&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[45,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4753"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4753"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4753\/revisions"}],"predecessor-version":[{"id":4755,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4753\/revisions\/4755"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4753"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4753"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4753"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}