A formal proof of a necessary and sufficient condition for deadlock-free adaptive networks

F. Verbeek, J. Schmaltz

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    4 Citaten (Scopus)

    Samenvatting

    Deadlocks occur in interconnection networks as messages compete for free channels or empty buffers. Deadlocks are often associated with a circular wait between processes and resources. In the context of networks, Duato proved that for adaptive routing networks a cyclic dependency is not sufficient to create a deadlock. He proposed deadlock-free routing techniques allowing cyclic dependencies between channels or buffers. His work was a breakthrough. It was also counterintuitive and only a complex mathematical proof could convince his peers about the soundness of his theory. We define a necessary and sufficient condition that captures Duato’s intuition but that is more intuitive and leads to a simpler proof. However, our condition is logically equivalent to Duato’s one. We used the ACL2 theorem proving system to formalize our condition and its proof. In particular, we used two features of ACL2, namely the encapsulation principle and quantifiers, to perform an elegant formalization based on second order functions.
    Originele taal-2Engels
    TitelInteractive Theorem Proving (First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings)
    RedacteurenM. Kaufmann, L.C. Paulson
    Plaats van productieBerlin
    UitgeverijSpringer
    Pagina's67-82
    ISBN van geprinte versie978-3-642-14051-8
    DOI's
    StatusGepubliceerd - 2010

    Publicatie series

    NaamLecture Notes in Computer Science
    Volume6172
    ISSN van geprinte versie0302-9743

    Vingerafdruk Duik in de onderzoeksthema's van 'A formal proof of a necessary and sufficient condition for deadlock-free adaptive networks'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit