{"id":658,"date":"2010-09-19T08:08:56","date_gmt":"2010-09-19T08:08:56","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=658"},"modified":"2010-12-22T17:05:23","modified_gmt":"2010-12-22T17:05:23","slug":"proof-pearl-a-formal-proof-of-dally-and-seitz%e2%80%99-necessary-and-sufficient-condition-for-deadlock-free-routing-in-interconnection-networks","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/proof-pearl-a-formal-proof-of-dally-and-seitz%e2%80%99-necessary-and-sufficient-condition-for-deadlock-free-routing-in-interconnection-networks\/","title":{"rendered":"Proof Pearl: A Formal Proof of Dally and Seitz\u2019 Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks"},"content":{"rendered":"

\nSe ha publicado un nuevo art\u00edculo de formalizaci\u00f3n: Proof Pearl: A Formal Proof of Dally and Seitz\u2019 Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks<\/a><\/p>\n

\nLos autores del art\u00edculo son Freek Verbeek<\/a> y Julien Schmaltz<\/a> de la Universiad de Radboud en Nimega<\/a> (en neerland\u00e9s: Nijmegen), Paises Bajos.<\/p>\n

\nEl art\u00edculo se public\u00f3 ayer (18 de Septiembre de 2010) en el Journal of Automated Reasoning<\/i>.<\/p>\n

\nUna versi\u00f3n preliminar del art\u00edculo puede leerse aqu\u00ed<\/a> y el c\u00f3digo ACL2 correspondiente puede obtenerse aqu\u00ed<\/a><\/p>\n

\nEl art\u00edculo es una demostraci\u00f3n en ACL2<\/a> de una condici\u00f3n necesaria y suficiente para enrutamiento sin estancamiento introducida por William J. Dally y Charles L. Seitz en su art\u00edculo Deadlock Free Message Routing in Multiprocessor Interconnection Networks<\/a> de 1987.
\n<\/p>\n

\nEl art\u00edculo se desarrolla dentro del proyecto Formal Verification of Deadlock Avoidance Mechanisms (FVDAM)<\/a>. La memoria de la propuesta del proyecto puede leerse aqu\u00ed<\/a>.<\/p>\n

\nEl resumen del art\u00edculo es<\/p>\n

\nAvoiding deadlock is crucial to interconnection networks. In \u201987, Dally and Seitz proposed a necessary and sufficient condition for deadlock-free routing. This condition states that a routing function is deadlock-free if and only if its channel dependency graph is acyclic. We formally define and prove a slightly different condition from which the original condition of Dally and Seitz can be derived. Dally and Seitz prove that a deadlock situation induces cyclic dependencies by reductio ad absurdum. In contrast we introduce the notion of a waiting graph from which we explicitly construct a cyclic dependency from a deadlock situation. Moreover, our proof is structured in such a way that it only depends on a small set of proof obligations associated to arbitrary routing functions and switching policies. Discharging these proof obligations is sufficient to instantiate our condition for deadlock-free routing on particular networks. Our condition and its proof have been formalized using the ACL2 theorem proving system.\n<\/p><\/blockquote>\n

\nOtro trabajo de los mismos autores donde explican y aplican esta formalizaci\u00f3n es Proof Pearl: A formal proof of Duato\u2019s condition for deadlock-free adaptive networks<\/a> presentado en la 1st International Conference on Interactive Theorem Proving (ITP\u201910)<\/i>.<\/p>\n","protected":false},"excerpt":{"rendered":"

Se ha publicado un nuevo art\u00edculo de formalizaci\u00f3n: Proof Pearl: A Formal Proof of Dally and Seitz\u2019 Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks Los autores del art\u00edculo son Freek Verbeek y Julien Schmaltz de la Universiad de Radboud en Nimega (en neerland\u00e9s: Nijmegen), Paises Bajos. El art\u00edculo se public\u00f3 ayer (18…<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"closed","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":[49,20,89,275],"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\/658"}],"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=658"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/658\/revisions"}],"predecessor-version":[{"id":1053,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/658\/revisions\/1053"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=658"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=658"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=658"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}