WEKO3
アイテム
π計算による優先度継承プロトコルの形式的記述
https://ipsj.ixsq.nii.ac.jp/records/16787
https://ipsj.ixsq.nii.ac.jp/records/1678750bb4075-1912-4915-ba34-f0d0cb585bbf
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO4308019.pdf (36.5 kB)
|
Copyright (c) 2002 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2002-09-15 | |||||||
| タイトル | ||||||||
| タイトル | π計算による優先度継承プロトコルの形式的記述 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | A Formal Description of the Priority Inheritance Protocol by the π- calculus | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 発表概要 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| 名古屋大学大学院工学研究科計算理工学専攻 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学大学院工学研究科情報工学専攻 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学大学院工学研究科情報工学専攻 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Department of Computational Science and Engineering, School of Engineering, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Department of Information Engineering, School of Engineering, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Department of Information Engineering, School of Engineering, Nagoya University | ||||||||
| 著者名 |
桑原, 寛明
× 桑原, 寛明
|
|||||||
| 著者名(英) |
Hiroaki, Kuwabara
× Hiroaki, Kuwabara
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 本発表では優先度方式スケジューリングにおける優先度逆転問題を解消する手法である優先度継承プロトコルのπ計算を用いた形式的な記述について述べる．π計算におけるプロセスの優先度の取扱いについて定義し，ブロックしたプロセスがブロックされたプロセスの優先度を継承する際に発生する優先度の通信の記述方法を決定する．継承により動的に変化するプロセスの優先度のある時点における高さを，そのときの各プロセスの共有資源に対するアクセス状況から決定する手法を示す．優先度継承プロトコルに沿って動作するプロセス，共有資源，スケジューラをπ計算によって記述することで，優先度継承プロトコルの形式的記述とする．形式的に記述することで動作の機械的な確認が容易になる．最後に形式的記述を用いた具体的な記述例を示す． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | In this presentation, we mention a formal description of the priority inheritance protocol which is the method to solve a priority inversion by the π-calculus. We define how to handle the priority of a process in the π-calculus, and determine the description of communications that arise when a blocked process inherits a priority of the blocking process. It is shown that the method to determine the priority which is changed dynamically from the access situation over the shared resources. We regard a formal description of the priority inheritance protocol as the description by the π-calculus of the processes, the shared resources and the scheduler which operate with the priority inheritance protocol. A formal description facilitate checking of the operations. Finally, we illustrate our formal description of the priority inheritance protocol by a concrete example. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464814 | |||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 43, 号 SIG08(PRO15), p. 118-118, 発行日 2002-09-15 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7802 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
