文献

J-GLOBAL ID：201702258116135244   整理番号：17A0754914

キャッシュコヒーレンスプロトコルと通信構造のデッドロック検証【Powered by NICT】

Deadlock Verification of Cache Coherence Protocols and Communication Fabrics

著者 (4件)： Verbeek Freek (Open University of The Netherlands, Heerlen, DL, The Netherlands) ,  Yaghini Pooria M. (University of California, Irvine, CA) ,  Eghbal Ashkan (University of California, Irvine, CA) ,  Bagherzadeh Nader (University of California, Irvine, CA)
資料名： IEEE Transactions on Computers  (IEEE Transactions on Computers)
巻： 66  号： 2  ページ： 272-284  発行年： 2017年 
JST資料番号： C0233A  ISSN： 0018-9340  CODEN： ICTOB4  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： キャッシュコヒーレンスは,メニーコアシステムにおける主要な役割を果たしている。デッドロックの検証は,特に課題である,デッドロック自由度が新たな特性である。形式的手法はしばしば通信相互接続の検証からプロトコルの検証を分離。が,現代の通信織物はより高度になり,ネットワークトポロジー,経路選定,調停,同期,を含んでいる。本論文では,統合的アプローチは,キャッシュコヒーレンスプロトコルと通信布両方一度にすべてのクロスレイヤ検証を可能にすることを提案した。クロスレイヤ不変量を導出するための自動化方法論を提案した。これらの不変量は,アプリケーション層プロトコルの状態を関連通信ファブリックの途中パケット。不変量を用いて,二つの事例研究のためのデッドロック自由の形式的証明:2Dメッシュにおける登録ベースMIプロトコル,および2Dトーラスにおけるリングベーススヌープ・プロトコルを導出した。さらに,著者らは,この方法論はデッドロックが存在しないことを保証する最小可能待ち行列サイズを導出するために使用できることを示した。著者らの方法論は一般的に適用可能であり,有望なスケーラビリティを示した。Copyright 2017 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】

シソーラス用語： 相互接続 ,  待ち行列 ,  *通信 ,  パケット ,  *プロトコル ,  ネットワーク構造 ,  不変量 ,  *デッドロック ,  事例研究 ,  自動化 ,  自由度 ,  経路選定
準シソーラス用語： トーラス ,  アプリケーション層 ,  クロスレイヤ ,  ネットワークトポロジー , 【Automatic Indexing@JST】

分類 (1件)： 記憶方式  (JC02040V)

タイトルに関連する用語 (2件)： デッドロック ,  検証