| 研究課題/領域番号 |
21K11822
|
|---|
| 研究機関 | 東京工業大学 |
|---|
研究代表者 |
渡部 卓雄 東京工業大学, 情報理工学院, 教授 (20222408)
|
|---|
| 研究分担者 |
森口 草介 東京工業大学, 情報理工学院, 助教 (60733409)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2024-03-31
|
| キーワード | 関数リアクティブプログラミング / サイバーフィジカルシステム / アクターモデル / 非同期処理 / 型システム |
|---|
| 研究実績の概要 |
(a) 小規模組込みシステム向け関数リアクティブプログラミング(FRP)言語Emfrpのための非同期処理機構を提案した．Emfrpではプログラム実行時に必要なメモリ量が静的に決定され，時変値更新処理の停止性も保証されている．これにより，メモリやCPUなどのリソースが制限された組込みシステムにおいて（実行時検査に頼らずに）メモリ安全性や応答性が担保できるようになっている．しかしこれらは言語設計上の制限によって実現されており，例えばグラフ構造の構築やその上の探索など，時間のかかる処理の記述は想定されていない．また，Emfrpプログラムの実行は同期的に行われるため，こういった処理を外部関数呼び出しとしてナイーブに実現すると応答性が悪化する．そこで，我々は一般的な並行プログラミングに用いられるfutureやpromiseに相当する機構のEmfrpへの導入方式を提案した．これにより，時変値更新による動作の応答性の高さを維持しながら，時間のかかる処理の非同期的な実行を純粋な関数リアクティブプログラミングの枠組み内で可能にしている．
(b) データの大きさを静的に規定できる型システムBCTを導入したEmfrpの拡張言語EmfrpBCTのためのパラメータ型多相の仕組みを提案した．EmfrpBCTでは，リストや木のような再帰的かつ動的に構築されるデータ構造について，それらの大きさを型の中で明記することで，プログラムが利用するメモリ量を静的に規定できる．今年度は，EmfrpBCTへのパラメタ型多相の導入方式を提案し，それにもとづく言語EmfrpPBCTの構文，操作的意味，型システム，使用メモリ量決定アルゴリズムを形式的に定義し，健全性を証明した．
(c) Emfrpのための，時間制約を持つイベント列のための言語拡張を提案した．これにより，時系列を持つ入力の検出等を簡潔に記述できることを示した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
研究成果概要の(a)に述べた成果は効率的な非同期実行方式の提案であり，本研究課題の目的であるアクターモデルにもとづくCPS向けFRP言語の実行基盤となるべきものであり，その点では研究はおおむね順調に進展していると言える．
しかし，メモリやCPUといった計算リソースに関する言語機構および実験のうち，当初予定していた組込みシステムの消費電力への影響の調査については，昨今の半導体不足による機材調達の遅れによりまだ取り組めていない．これについては次年度（2022年度）以降，引き続き調達を試み，代替手法も視野に入れて早急に実験に着手する．
もう一つの，実行時の使用メモリに関連する研究成果は研究成果概要の(b)であり，こちらはおおむね順調に進展していると言える．
全体としては，上記理由によりFRP言語による実行時リソースの制御についての研究は十分進展したとは言えず，その点でやや遅れていると判断したが，これらは調達が遅れた機材が入手でき次第実験ができるので，次年度以降に十分リカバーできると考える．
|
| 今後の研究の推進方策 |
研究成果概要の(a)で述べた非同期実行方式を実機（組込み機器）において評価を行い，それをもとにアクターモデルを実行系とするCPS向けFRP言語の設計・実装を行う．特に実際の分散型計算機（センサやアクチュエータを備えた小型のLinuxボード数台〜20台程度を想定）で動作するWSAN等のアプリケーションを用いた実験を通して，導入した言語機構の評価を行い，その知見を言語設計にフィードバックする．
また，計算リソース，特にシステムの消費電力をモニタしつつ実行する方式や，CPUのDeep Sleep機構を用いた間欠計算の導入による消費電力の低減方式を検討する．コードと実行時メモリそれぞれの大きさと実行速度，および間欠実行のオーバーヘッドについて評価を行う．
加えて，研究成果概要の(b)で述べた組込みシステム向けFRP言語におけるメモリ制約を型システムによって強制する手法をもとに，実際の組込みシステムやCPSを対象としたメモリ制約の制御方式を提案し，その評価を行う．また，型システムではカバーできないプログラムの性質について検証を行うための形式的検証手法についても検討する．
|
| 次年度使用額が生じた理由 |
COVID-19の影響で参加した学会・国際会議の現地開催が行われなくなり，旅費の支出が抑えられた．加えて，昨今の半導体不足の影響により購入を予定していた実験用機材の年度内に調達できなくなった．
次年度（2022年度）は参加を予定している会議のいくつかが対面での実施をアナウンスしているため，そのための旅費を支出する．また，今年度入手できなかった機材については，引き続き（代用となる機材を含めた）調達を試みる．
|
