Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks
Se ha publicado un nuevo artículo de formalización: Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks
Los autores del artículo son Freek Verbeek y Julien Schmaltz de la Universiad de Radboud en Nimega (en neerlandés: Nijmegen), Paises Bajos.
El artículo se publicó ayer (18 de Septiembre de 2010) en el Journal of Automated Reasoning.
Una versión preliminar del artículo puede leerse aquí y el código ACL2 correspondiente puede obtenerse aquí
El artículo es una demostración en ACL2 de una condición necesaria y suficiente para enrutamiento sin estancamiento introducida por William J. Dally y Charles L. Seitz en su artículo Deadlock Free Message Routing in Multiprocessor Interconnection Networks de 1987.
Read More “Proof Pearl: A Formal Proof of Dally and Seitz’ Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks”