WEKO3
アイテム
ハードウェアの振舞いを考慮したスピンロックのモデル検査
https://ipsj.ixsq.nii.ac.jp/records/74144
https://ipsj.ixsq.nii.ac.jp/records/74144efe1e1e4-98d7-4d5c-9ad4-b11e813a9641
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-SE11172002.pdf (273.5 kB)
|
Copyright (c) 2011 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2011-05-10 | |||||||
| タイトル | ||||||||
| タイトル | ハードウェアの振舞いを考慮したスピンロックのモデル検査 | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Model Checking of the Spin-lock in Consideration of Hardware Behavior | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 組込みシステム | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||
| 資源タイプ | technical report | |||||||
| 著者所属 | ||||||||
| 名古屋大学大学院情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学大学院情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学大学院情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学大学院情報科学研究科 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者名 |
加藤, 寿和
× 加藤, 寿和
|
|||||||
| 著者名(英) |
Toshikazu, Kato
× Toshikazu, Kato
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 本研究では，マルチプロセッサシステムで用いられるスピンロックアルゴリズムを複数種類のメモリコンシステンシモデルを含めてモデル化し，メモリバリア命令を加えた際の排他性に関して検証を行った．近年，組込みシステム向けのハードウェア（プロセッサ）においても，高速化のために，Total Store Ordering（TSO）やPartial Store Ordering（PSO）のようなメモリコンシステンシモデルを持つものがある．メモリアクセスの順序がソフトウェアの記述と入れ替わるため，メモリバリア命令を適切に使用する必要がある．モデルを用いて検証を行った結果，適切な位置にメモリバリア命令を挿入した場合に排他性が満たされることを確認できた．PSOのモデルでプロセッサ数が2個の条件での検証では，状態数は1.8×10<sup>9</sup>であった． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | We verified the exclusiveness of spin-lock algorithm with memory barrier instructions by modeling the algorithm with several kinds of memory consistency models. Recent hardware for embedded systems uses memory consistency models such as Total Store Ordering(TSO) and Partial Store Ordering(PSO). Since in these models the real order of memory access differs from the described order in software, it is necessary to insert memory barrier instruction to the software description appropriately. Our verification models confirm the satisfaction of exclusiveness when memory barrier instruction is inserted appropriately. The number of state was 1.8×10<sup>9</sup> on verifying PSO model with two processors. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AN10112981 | |||||||
| 書誌情報 |
研究報告ソフトウェア工学（SE） 巻 2011-SE-172, 号 2, p. 1-8, 発行日 2011-05-10 |
|||||||
| Notice | ||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
