WEKO3
アイテム
型エラースライシングによるデッドロックの原因特定
https://ipsj.ixsq.nii.ac.jp/records/16438
https://ipsj.ixsq.nii.ac.jp/records/16438bb86da6d-04b0-479a-93fe-e900be5d86cf
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO0102007.pdf (290.8 kB)
|
Copyright (c) 2008 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2008-09-26 | |||||||
| タイトル | ||||||||
| タイトル | 型エラースライシングによるデッドロックの原因特定 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Identifying Deadlock Errors by Type Error Slicing | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 通常論文 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| 東北大学大学院情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 東北大学大学院情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 東京大学大学院情報理工学系研究科 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Sciences, TOHOKU University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Sciences, TOHOKU University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science and Technology, The University of Tokyo | ||||||||
| 著者名 |
飯村, 枝里
× 飯村, 枝里
|
|||||||
| 著者名(英) |
Eri, Iimura
× Eri, Iimura
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 並行プログラムは，実行の非決定性などのために，バグが混入しやすく，またそのバグの発見が難しい．そこで，並行プログラムを静的かつ網羅的に検証するための手法として，型システムを用いた手法が近年注目されている．小林らはπ計算を対象としてデッドロックの検証を行う型システムを提案し，それに基づく自動検証器を実装している．しかしながら，型システムとそれに基づく検証アルゴリズムの複雑さのため，検証に失敗した場合に具体的にプログラムのどの部分に誤りがあるのかをユーザが判断するのは困難であった．本研究では，関数型言語を対象として提案されている型エラースライシングの考え方を，小林らの型システムに適用することにより，デッドロックの可能性がある場合にその原因個所を具体的に提示するアルゴリズムを与える．さらに小林の検証器に提案手法の実装を組み込み，その有効性を確認した． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | It is difficult to find bugs in concurrent programs because of non-determinism. Recently, various type systems have been proposed for detecting bugs in concurrent programs. For instance, Kobayashi et al. present type systems for checking deadlock freedom, livelock freedom, and other properties of the π-calculus. Their type systems are implemented in the tool TyPiCal. However, it is sometimes difficult for the users to understand the reason for a type error reported by TyPiCal. In this paper, drawing on research in type error slicing for functional languages, we propose a slicing algorithm for identifying deadlock type errors reported by TyPiCal. We have implemented our slicing algorithm as an extension to TyPiCal, and verified its correctness on a small number of examples. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464814 | |||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 1, 号 2, p. 71-84, 発行日 2008-09-26 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7802 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
