WEKO3
アイテム
TicklessカーネルにおけるWork Conservingスケジューラのモデル検査
https://ipsj.ixsq.nii.ac.jp/records/2006927
https://ipsj.ixsq.nii.ac.jp/records/2006927896ca68f-a272-4333-af06-6c16eeb1c8ef
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-OS26170004.pdf (1004.2 KB)
2028年2月9日からダウンロード可能です。
|
Copyright (c) 2026 by the Information Processing Society of Japan
|
|
| 非会員：¥660, IPSJ:学会員：¥330, OS:会員：¥0, DLIB:会員：¥0 | ||
| Item type | SIG Technical Reports(1) | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2026-02-09 | |||||||||||
| タイトル | ||||||||||||
| 言語 | ja | |||||||||||
| タイトル | TicklessカーネルにおけるWork Conservingスケジューラのモデル検査 | |||||||||||
| 言語 | ||||||||||||
| 言語 | jpn | |||||||||||
| キーワード | ||||||||||||
| 主題Scheme | Other | |||||||||||
| 主題 | OSカーネル | |||||||||||
| 資源タイプ | ||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||||||
| 資源タイプ | technical report | |||||||||||
| 著者所属 | ||||||||||||
| 株式会社ティアフォー | ||||||||||||
| 著者所属 | ||||||||||||
| 株式会社ティアフォー | ||||||||||||
| 著者所属 | ||||||||||||
| 株式会社ティアフォー | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| TIER IV, Inc. | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| TIER IV, Inc. | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| TIER IV, Inc. | ||||||||||||
| 著者名 |
高野,祐輝
× 高野,祐輝
× 今井,航一
× 神戸,隆太
|
|||||||||||
| 論文抄録 | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | Ticklessカーネルでは、アトミック命令やコア間割り込み（IPI）を適切に活用してタスクのスケジューリングを行う必要がある。スケジューラにバグがないかを測る指標の一つに、Work Conservation（WC）と呼ばれる性質がある。これは「実行可能なタスクが存在する限りCPUコアを常に稼働させる」というものである。もしアトミック命令やIPIを用いた処理にバグが混在すると、実行可能なタスクが存在しているにもかかわらずCPUがアイドル状態のままとなり、WCが満たされないことがある。B. Leperらは、単純なWCの定義がマルチコア環境には適用できないことを指摘し、Concurrent Work Conservation（CWC）という新たな概念を提唱し形式的に定義した。しかし、アトミック命令やIPIに関するバグは、CWCの枠組みだけでは発見できず、また、CWCはグローバルスケジューラに対して直接適用できないという課題がある。そこで本論文では、まずCWCがグローバルスケジューラに直接適用できない理由を明らかにし、その定義を拡張・改良する。次に、線形時相論理（LTL）を用いた、TicklessカーネルにおけるWork Conservingスケジューラの検証手法を提案する。この検証には、LTLを記述可能なモデル検査器であるSPINを利用する。検証対象とするTicklessカーネルは、現在研究開発中のAwkernelである。SPINを用いた検証の結果、CWCの枠組みで発見可能なバグと、CWCでは検出できずLTLによるモデル検査で初めて発見されるバグがそれぞれ存在することが明らかとなった。 | |||||||||||
| 書誌レコードID | ||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||
| 収録物識別子 | AN10444176 | |||||||||||
| 書誌情報 |
研究報告システムソフトウェアとオペレーティング・システム（OS） 巻 2026-OS-170, 号 4, p. 1-10, 発行日 2026-02-09 |
|||||||||||
| ISSN | ||||||||||||
| 収録物識別子タイプ | ISSN | |||||||||||
| 収録物識別子 | 2188-8795 | |||||||||||
| Notice | ||||||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||||||
| 出版者 | ||||||||||||
| 言語 | ja | |||||||||||
| 出版者 | 情報処理学会 | |||||||||||
