محبوبترین نویسندگان :
نویسندگان مقالات پربازدید :
مجله استدلال خودکار 2013
جزئیات رویداد
اینستاگرام تی پی بین
همایش ، رویداد ، ژورنال

  • proof pearl: a formal proof of dally and seitz’ necessary and sufficient condition for deadlock-free routing in interconnection networks

    نویسندگان :
    کلمات کلیدی :
    جزئیات بیشتر مقاله
    • تاریخ ارائه: 1392/07/24
    • تاریخ انتشار در تی پی بین: 1392/07/24
    • تعداد بازدید: 898
    • تعداد پرسش و پاسخ ها: 0
    • شماره تماس دبیرخانه رویداد: -
     avoiding deadlock is crucial to interconnection networks. in ’87, 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.

سوال خود را در مورد این مقاله مطرح نمایید :

با انتخاب دکمه ثبت پرسش، موافقت خود را با قوانین انتشار محتوا در وبسایت تی پی بین اعلام می کنم
مقالات جدیدترین رویدادها
مقالات جدیدترین ژورنال ها