第155回プログラミング研究発表会

2025年並列/分散/協調処理に関する サマー・ワークショップ (SWoPP2025)

日程:2025年8月4日(月)〜 8月5日(水)
会場:サンポートホール高松 (香川県高松市)  6F 62会議室
   およびオンラインのハイブリッド開催を予定

  • 発表募集
  • 発表申込期間:2025年5月13日(火曜日) 〜 5月19日(月曜日)
  • 投稿論文原稿提出締切:2025年6月30日(月曜日)
  • 発表予稿提出締切:2025年7月30日(水曜日)
  • 参加申込
    • 参加申込をされた方に予稿やオンライン参加方法をご案内いたします
    • 参加申込は当日も受けつけおります
    • 参加費は無料です

担当:加藤 弘之(国立情報学研究所)、新屋 良磨(秋田大学)
発表申込送信ページ:https://forms.gle/KHZbZ8Bt2wtbuUwq7
問い合わせ先:加藤 弘之(E-mail: kato [at] nii.ac.jp)

プログラム

  • 1件あたり45分(発表25分,質疑・討論20分)(短い発表は発表20分,質疑・討論10分)
  • ◯印が登壇者です.

8月4日(月曜日)

*セッション1(14:10-15:00):座長 平石 拓 (京都橘大学)
2025-2-(1): 14:10–14:55
Entity Component Systemアーキテクチャに基づいたプロセッサシミュレータの開発
◯前川 隼輝 (名古屋工業大学)
小田喜 陽彦 (東京大学)
小泉 透 (名古屋工業大学)
塩谷 亮太 (東京大学)
津邑 公暁 (名古屋工業大学)

プロセッサアーキテクチャの研究に使われるプロセッサシミュレータは,プロセッサ動作のモデル化にC++等のオブジェクト指向言語を用いることが多い.
新たな手法を評価するためには,これの改造が必要となるが,様々なオブジェクトが絡み合う動作を解読しなければならず,修正後のコードも見通しが悪くなりがちである.
これに対し我々は,これらの問題がゲーム開発における問題と類似していることに着想を得て,ゲーム開発で用いられることの多いEntity Component System (ECS)と呼ばれるソフトウェアアーキテクチャをプロセッサシミュレータの記述へ導入した.
ECSは,データ指向的かつコンポジションにより機能を拡張する記述方式である.
本発表では,オブジェクト指向での記述と比べ,ECSでの記述がプロセッサアーキテクチャ研究で頻出の状況に無理なく対応できることを示す.
さらに,ECSの導入により生じる課題と我々の対処法を紹介する.

*セッション2(15:10-16:50):座長 安部 達也(千葉工業大学)
2025-2-(2): 15:10–15:55
Putbackベースの双方向変換言語BiGULの更新ベース化と移行後の性質について
◯豊田 雅希 (法政大学)
日高 宗一郎 (法政大学)

モデル駆動工学等で用いられる同期手法の一つに,ラウンドトリップ性に基づき一貫性を保証する双方向変換がある.双方向変換言語BiGULでは,本質的に曖昧な逆方向変換をユーザがPutback方式により明確にできるが,更新伝播が状態ベースで行われるため,大規模なデータを扱う際に更新ベース化による処理速度向上も期待できる.本研究では,更新ベースの双方向変換言語Edit Lenses を参考に,双方向変換言語Xの汎用的な型Valを取り入れることで,BiGUL の Haskell実装の更新ベース化を行っているが,実装した更新ベースのBiGULについて,状態ベースの BiGULとの意味的同一性,更新ベースの双方向変換として振る舞いが良いことの確認は,具体例と実験に基づくものに留まっていた.本発表では,これらの性質の証明も含めて報告する.

2025-2-(3): 16:00–16:45
Introducing Linear Implication Types to λGT for Computing With Incomplete Graphs
◯Jin Sano (Waseda University)
Kazunori Ueda (Waseda University)

Designing programming languages that enable intuitive and safe manipulation of
data structures is a critical research challenge. Conventional destructive memory
operations using pointers are complex and prone to errors. Existing type systems, such as
affine types, fail to ensure the safety of structures and operations that involve
data with shared references or cycles. The λGT language, a purely functional
programming language that treats hypergraphs (hereafter referred to as graphs) as
first-class citizens, addresses some of these challenges. By abstracting data with shared
references and cycles as graphs, it enables declarative operations through pattern
matching and leverages its type system to guarantee safety of these operations.
Nevertheless, the previously proposed type system of λGT leaves two significant open
challenges. First, the type system does not support incomplete graphs, that is, graphs in
which some elements are missing from the graphs of user-defined types. Second, the
type system relies on dynamic type checking during pattern matching. This study
addresses these two challenges by incorporating linear implication into the λGT type
system, while introducing new constraints to ensure its soundness.

*編集委員会 17:10-18:40(@4階第11楽屋)

8月5日(火曜日)

*セッション3(9:15-10:55):座長 加藤 弘之(国立情報学研究所)
2025-2-(4): 9:15–10:00
Babylonを用いたPIM向けJavaオフロードAPIの設計と実装
◯佐藤 重幸 (電気通信大学)
鵜川 始陽(東京大学)


メモリ内のプロセッサを用いる計算パラダイムであるProcessing-in-Memory(PIM)は,近年注目を集めている.
我々は,Javaによるオブジェクト指向プログラミングとPIMの統合を目指して,商用PIMシステムUPMEM PIM上で動作するJava VMを開発している.
しかし,現状のオフロードAPIは,並列計算を抽象化しておらず,静的型検査も機能しない,原始的なものである.
そこで本研究では,PIM向けJavaオフロードの高水準APIを提案する.
本論文では,APIの設計とJavaリフレクション機能Babylonを用いた実装法の概要を紹介する.

2025-2-(5): 10:05–10:50
RL78マイコンのレジスタバンクの呼出先で退避する記憶領域としての活用
◯千葉 雄司 (ルネサス エレクトロニクス株式会社)


RL78マイコンはレジスタバンクを4つ備えるが,4つ全て使うアプリケーションは多くなく,残りの活用法が課題になってきた.RL78のレジスタバンクを低消費電力な記憶領域として使えることに着目し,我々は,過去の研究で,割込の受付を禁止している間,実行コンテキストの保存先として活用する技法を検討したが,当該技法では,割込の受付を許可している間,消費電力を削減できない.そこで,我々は,割込の受付を許可している間の消費電力削減を目指し,呼出先で退避する記憶領域として活用する技法の有用性を評価した.EEMBCの超低消費電力ベンチマークULP-CPを使って評価した結果,消費電力を6.1%削減する効果があることが判った.

*セッション4(11:05-11:55):座長 佐藤 亮介(東京農工大学)
2025-2-(6): 11:05–11:50
Maudeによる測定型量子計算の自動検証
◯名越 龍一 (北陸先端科学技術大学院大学)
髙木 翼 (北陸先端科学技術大学院大学)


本研究は,測定型量子計算の自動検証を目的とし,仕様記述言語 Maude による形式検証手法を提案する.本研究では,行列を記号的な項として表現し,計算手順を Measurement Calculus に基づき形式化した.Maude の記号的推論機能を用いて,測定によって生じる全分岐を網羅し,自動検証する枠組みを開発した.本手法を量子テレポーテーションと GHZ 状態生成に適用した結果,すべての分岐で所望の性質が得られることを確認し、MBQC プロトコルの網羅的な検証における本手法の有効性を示した.

*セッション5(13:20-14:50):座長 鵜川 始陽(東京大学)
2025-2-(7): 13:20–14:05
入出力整合性を満たすSFQ回路を記述するためのRustを用いたドメイン固有言語
◯大石 芽吹 (東京大学)
田中 燦 (東京大学)
高前田 伸也 (東京大学・理化学研究所)


超伝導状態を利用して極めて高速、低消費電力で動作可能な単一磁束量子(SFQ)回路への関心が高まっている。電圧駆動のCMOS回路とは異なり、SFQ回路はパルス駆動であることから入力と出力を一対一に接続する必要があり、これを入出力整合性と呼ぶ。現在のSFQ回路の開発はセルライブラリやシミュレーションツールが利用可能であるが、それらを用いて効率的に設計するためのツールは整っておらず、設計者は回路を正しく記述することにも労力を割く必要がある。
そこで我々はRustの所有権システムを利用してSFQ回路の入出力整合性を保証するドメイン固有言語のRustSFQを提案する。ゲートレベルでの回路記述により表現力を保ちつつ、ネット名の自動生成により従来のネットリスト記述の手間を削減する。またデジタルとアナログの2種類のシミュレーション用ファイルを出力可能で、これらを併用した効果的な開発にも貢献する。

2025-2-(8): 14:10–14:40
Rust製TLSFアロケータの形式検証
◯柿下 シナイ (北陸先端科学技術大学院大学)
長谷川 央 (北陸先端科学技術大学院大学)
青木 利晃 (北陸先端科学技術大学院大学)
神戸 隆太 (株式会社ティアフォー)
高野 祐輝 (株式会社ティアフォー)


Programming with versions (PWV) introduces the notions of versions into the 
language semantics and allows for version-safe multi-version programming. BatakJava is an object-oriented implementation of PWV that adds versions 
as an attribute of a class, where different versions of a class can coexist and 
interact with each other in the same program. To ensure version safety, BatakJava uses a constraint-based type system during compilation that solves for a fixed version assignment for every type instance in the program. However, this compilation scheme significantly reduces the flexibility of multi-version programming that may require type instances to be used with different version assignments. To solve this problem, we propose the use of parameterized versions to allow version polymorphic definitions. This paper presents the design for a version polymorphic extension of BatakJava, its implementation that modifies the original type analysis and code generation, and a case study to demonstrate the improved flexibility of multi-version programming with version polymorphism.

*編集委員会(15:10-16:50)(@4階第11楽屋)

関連リンク