文献

J-GLOBAL ID：202002277504996848   整理番号：20A2374663

メッセージパッシングインタフェイスプログラムの記号検証【JST・京大機械翻訳】

Symbolic verification of message passing interface programs

著者 (8件)： Yu Hengbiao (National University of Defense Technology, Changsha, China) ,  Chen Zhenbang (National University of Defense Technology, Changsha, China) ,  Fu Xianjin (National University of Defense Technology, Changsha, China) ,  Wang Ji (National University of Defense Technology, Changsha, China) ,  Su Zhendong (ETH Zurich, Switzerland) ,  Sun Jun (Singapore Management University, Singapore) ,  Huang Chun (National University of Defense Technology, Changsha, China) ,  Dong Wei (National University of Defense Technology, Changsha, China)
資料名： ACM Proceedings  (ACM Proceedings)
号： ICSE ’20  ページ： 1248-1260  発行年： 2020年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： メッセージ通過は,高性能コンピューティングにおけるプログラミングの標準パラダイムである。しかしながら,メッセージパッシングインタフェイス(MPI)プログラムの検証は,複雑なプログラム特徴(非決定および非ブロッキング操作のような)のため,困難である。本研究では,非ブロッキング操作によるMPIプログラムの自動検証のために,MPI記号検証器(MPI-SV),最初の記号実行ベースツールを提示した。MPI-SVは,MPIプログラム検証における課題に取り組むために,相乗的方法で記号実行とモデル検査を組み合わせる。相乗作用はスケーラビリティを改善し,検証可能な特性の範囲を拡大する。MPI-SV1を実装し,111の実世界MPI検証タスクで評価した。純粋記号実行ベース技法は1時間以内で111のタスクのうち61(55%)を成功裏に検証でき,一方,MPI-SVは100のタスク(90%)を検証した。平均して,純粋記号実行と比較して,MPI-SVは,19x高速化を達成し,臨界特性と5x高速化の満足度を,違反を見つける上で検証した。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 相乗作用 ,  臨界 ,  *ブロッキング ,  プログラム検証 ,  高速化 ,  モデル検査
準シソーラス用語： 高性能コンピューティング ,  *MPI【インタフェイス】 , 【Automatic Indexing@JST】

著者キーワード (5件)： メッセージパッシングインタフェイス ,  モデル検査 ,  記号実行 ,  記号検証 ,  相乗作用

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (3件)： メッセージパッシングインタフェイス ,  記号 ,  検証