-
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
- تعداد بازدید: 957
- تعداد پرسش و پاسخ ها: 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.
مقالات جدیدترین رویدادها
-
استفاده از تحلیل اهمیت-عملکرد در ارائه الگوی مدیریت خلاقیت سازمانی و ارائه راهکار جهت بهبود
-
بررسی تاثیر ارزش وجوه نقد مازاد بر ساختار سرمایه شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر سطح افشای ریسک بر قرارداد بدهی شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی تأثیر رتبه بندی اعتباری مبتنی بر مدل امتیاز بازار نوظهور بر نقد شوندگی سهام با تأکید بر خصوصی سازی شرکت ها
-
تأثیر آمیخته بازاریابی پوشاک ایرانی بر تصویر ذهنی مشتری پوشاک ایرانی (هاکوپیان)
-
مدل سازی شکست هیدرولیکی سد ناشی از سیلاب ناگهانی با نرم افزار فلوئنت
-
تحلیل رفتار بازدیدکنندگان در مواجه با ایوان در بنای تاریخی (نمونه موردی: ایوان شاهنشین ارگ کریمخان زند شیراز)
-
شناسائی مشخصات دینامیکی سد شهید رجائی به روش زیر فضای تصادفی بر پایه تحلیل همبستگی استاندارد
-
ارزیابی پایداری و سلامت آبخیز
-
accelerated growth of calcium silicate hydrates: experiments and simulations
مقالات جدیدترین ژورنال ها
-
مدیریت و بررسی افسردگی دانش آموزان دختر مقطع متوسطه دوم در دروان کرونا در شهرستان دزفول
-
مدیریت و بررسی خرد سیاسی در اندیشه ی فردوسی در ادب ایران
-
واکاوی و مدیریت توصیفی قلمدان(جاکلیدی)ضریح در موزه آستان قدس رضوی
-
بررسی تاثیر خلاقیت، دانش و انگیزه کارکنان بر پیشنهادات نوآورانه کارکنان ( مورد مطالعه: هتل های 3 و 4 ستاره استان کرمان)
-
بررسی تاثیر کیفیت سیستم های اطلاعاتی بر تصمیم گیری موفق در شرکتهای تولیدی استان اصفهان (مورد مطالعه: مدیران شرکتهای تولیدی استان اصفهان)
-
بررسی نقش هویت اسلامی در ساخت مسکن و محلات مسکونی
-
بررسی تأثیر بازارگرایی و ابعاد آن بر عملکرد شرکتهای بیمه پاسارگاد در شهر تهران
-
تاثیر کنترل های داخلی بر پایداری سود در شرکت های پذیرفته شده در بورس اوراق بهادار تهران
-
بررسی نگرش ها و عوامل مؤثر بر استقرار و فرایند گذار به حسابداری تعهدی (مورد مطالعه: آموزش و پرورش استان سیستان و بلوچستان)
-
investigation on the corrosion of coated steel plates with impact defect using divided steel plates
سوال خود را در مورد این مقاله مطرح نمایید :