ABSTRACT. メモリに制約のある組込みシステムにオブジェクト指向言語を実装する場合，メモリ効率の良いコンパクションが必須となる．Jonkersのスレッド化コンパクションはそのひとつである．Jonkersのアルゴリズムでは，オブジェクトのレイアウトが必要になる．レイアウト情報はメタオブジェクトに記録する技法がよく用いられる．しかしメタオブジェクト間にポインタがある場合，オブジェクトとメタオブジェクトを同じヒープ内に保持できない．コンパクション中はメタオブジェクト間のポインタを辿れないからである．本研究では，Jonkersのアルゴリズムを，オブジェクトとメタオブジェクトを同じヒープ内に保持できるよう改良した．提案手法は，Jonkersのスレッド化コンパクションと同等の空間効率を実現する．提案手法を，組み込みシステム向けJavaScript処理系に実装し，マークスイープ方式ごみ集めと比較した．その結果，提案手法はマークスイープ方式と比べ空間効率が向上し，現実的なヒープサイズではごみ集め時間は2.8倍以内であった．

ABSTRACT. Most virtual machines employ just-in-time (JIT) compilers to achieve high-performance. Trace-based compilation and method-based compilation are two major compilation strategies in JIT compilers. In general, the former excels in compiling programs with more in-depth method calls and more dynamic branches, while the latter is suitable for a wide range of programs. Some previous studies have suggested that each strategy has its advantages and disadvantages, and there is no clear winner.

In this paper, we present a new approach, namely, the meta-hybrid JIT compilation strategy. It combines trace-based and method-based compilations to utilize the advantages of both strategies. Moreover, it is realized as a meta JIT compiler framework; thus, we can generate a VM with a hybrid JIT compiler that can apply different program parts by merely writing an interpreter with our framework.

We chose to extend a meta-tracing JIT compiler and supported the two compilations on it. As a prototype, we implemented a simple meta-tracing JIT compiler framework called BacCaml based on the MinCaml compiler by following RPython’s architecture.

We evaluated its performance by creating a small functional programming language with BacCaml and running microbenchmark programs. Furthermore, we performed a synthetic experiment to confirm that there are programs that run faster by hybrid compilation.

出典: The 16th Dynamic Languages Symposium (DLS) at SPLASH 2020, 掲載済み

ABSTRACT. 限定継続演算子 control / prompt を含むλ計算の CPS インタプリタの定義は過去の研究で確立されている。本研究はこのインタプリタに対して CPS 変換や非関数化などのプログラム変換を施し、同等の動作をするコンパイラと仮想機械の導出を行なった。先行研究では shift / reset のインタプリタに対して仮想機械の導出がされている。control / prompt の実装のために新たに導入された trail があっても同様の変換方法で仮想機械を導出することができた。最終的には trail もスタックと同様のデータ構造になるが、途中で trail を合成する必要から単なる cons リストではなく append を伴う表現が必要であった。得られた仮想機械は control / prompt の実装におけるデータスタックの挙動やヒープへコピーするべき箇所を明確にモデル化している。

ABSTRACT. Invertibility is a fundamental concept in computer science, with various manifestations in software development (serializer/deserializer, parser/printer, redo/undo, compressor/decompressor, and so on). Full invertibility necessarily requires bijectivity, but the direct approach of composing bijective functions to develop invertible programs is too restrictive to be useful. In this paper, we take a different approach by focusing on partially-invertible functions—functions that become invertible if some of their arguments are fixed. The simplest example of such is addition, which becomes invertible when fixing one of the operands. More involved examples include entropy-based compression methods (e.g., Huffman coding), which carry the occurrence frequency of input symbols (in certain formats such as Huffman tree), and fixing this frequency information makes the compression methods invertible.

We develop a language Sparcl for programming such functions in a natural way, where partial-invertibility is the norm and bijectivity is a special case, hence gaining significant expressiveness without compromising correctness. The challenge in designing such a language is to allow ordinary programming (the “partially” part) to interact with the invertible part freely, and yet guarantee invertibility by construction. The language Sparcl is linear-typed, and has a type constructor to distinguish data that are subject to invertible computation and those that are not. We present the syntax, type system, and semantics of the language, and prove that Sparcl correctly guarantees invertibility for its programs. We demonstrate the expressiveness of Sparcl with examples including tree rebuilding from preorder and inorder traversals and Huffman coding.

ICFP 2020（2020年8月開催）で発表済

ABSTRACT. IoT（Internet of Things）は情報科学の総合格闘技である．多様かつ大量の計算機器がネットワークを介して密接に絡み合い，様々な分野の技術領域を結集させて，大規模かつ複雑なIoTシステムが構築される．講演者は，IoTシステム分野におけるElixirの可能性に着目している．Elixirは2012年に登場した関数型言語であり，処理の振る舞いではなくデータの扱いを直接的に操作するためのライブラリや記法が豊富に整備されている．加えて記述容易で開発生産性が高く，並行／並列システムを容易に実現できるという特徴がある．本講演では，Elixirの特徴をIoTシステム開発に展開するための取り組みについて紹介する．関数を部品と捉えてその間の接続関係と並行処理を表現した処理フローは，データフロー型のシステムアーキテクチャの設計と親和性が高い．これを活かしたFPGA設計の最適化手法を提案する．また，アクターベースの軽量かつ頑強なプロセスモデルをIoTシステム通信機構に応用する試みを紹介する．元来の組込みシステム研究者が考えるプログラミング言語のIoTシステム分野への可能性について，PPLの参加者の皆さまとともに議論したい．

ABSTRACT. プログラミング初学者がどのようなプロセスを経てプログラムを書くのかということは、あまり理解されていない。そこで、2015年から2020年におけるOCaml初学者のプログラミング学習データを分析し、初学者のプログラミング行動について分析を行なった。 コーディングの進捗状態、コンパイル結果ごとのエラー状態やエラー原因を探ることで、初学者がどのように学習を進めるのか、また、どのようなプログラミング概念が初学者を悩ませているのか明らかにする。また、ビジュアルプログラミングエディタOCaml Blocklyが初学者に与えた影響についても、データに基づき考察する。 ここで得られた知見は、今後のプログラミング教育において、改善すべき問題点や教育姿勢を考える際に有用であると考える。

ABSTRACT. 2020年よりプログラミング教育が小学校で必修化され，多くの現場では教材としてブロック型言語のプログラミング環境が用いられている．今後増えるであろうブロック型言語学習者が，テキスト型言語を学習する際のハードルを低くすることを目標に，本論文では，ブロック型言語からテキスト型言語への移行を補助するプログラミング学習環境の設計と実装を行う．本環境では，プログラムコードのブロックを組み合わせる動作と，テキストによるコード編集の2つの動作を同期的に採り入れることで，ブロック型言語とテキスト型言語の対応の把握を容易にし，両者の両立を目指した．また，対象とするテキスト型言語に相当するBNF（Backus Naur Form）を与えることで，その言語に合うブロックを生成し，どのようなテキスト型言語にも対応できる汎用性を実現した．

ABSTRACT. グラフ描画アルゴリズムを用いてデータ構造を図示するライブプログラミング環境で大規模データ構造をプログラムするとき、２つの問題点がある。図が画面に収まるように縮小表示されるのでプログラマが注目している箇所の発見・認識が困難になる点と、プログラマがデータの参照関係を把握する上で不要なノードやエッジが増えてしまう点である。 これらの問題点を解決するため、プログラマの注目点を自動推定し、注目点からの参照距離やクラス・フィールドの重要度を使ってグラフ内のそれぞれの箇所の拡大率を変更・決定する手法を提案する。 この提案手法によりプログラマはコードを編集するだけで、注目したい箇所付近のグラフが拡大表示・注目されていない不要な箇所が縮小表示あるいは抽象化され、データ構造の変化を観察しやすくなる。 我々はライブデータ構造プログラミング環境Kanonのユーザーインターフェースを拡張し、新たなレイアウトアルゴリズムを実装・導入することで提案手法を実現した。 また、この提案手法の有用性を示すためにプログラミング経験者数名を対象としたユーザー実験を実施する。

ABSTRACT. これまでMizar言語の記述を補助するエディタ拡張機能は，Emacsプラグインとして開発が行われてきた．しかし，Emacsは独特のキーバインドから初学者にとって学習の敷居が高く，利用者が減少傾向にある．このため，定理証明支援系の統合開発環境としては，Visual Studio Codeへの関心が高まっており，すでにLeanやPVSをサポートする拡張機能が開発されている．これらの状況を踏まえ，本研究では，Visual Studio Code上でMizar言語の記述を補助するための拡張機能の開発を行った．

ABSTRACT. メモリ領域及びその参照はグラフ理論におけるグラフに抽象化できる． 従って複雑なデータ構造を扱う言語処理系の実装は，グラフ書き換え言語の応用分野として高い期待が持てる． 木に限らない，より一般のグラフであるヒープを必要とする仮想機械として，Haskell などの言語の処理系の実装の基盤となっている G-machine がある. そこで本研究ではグラフ書き換え言語 HyperLMNtal を用いて，G-machine 及びソース言語から G-machine の命令列を得るコンパイラの実装を行い，グラフ書き換え言語で複雑なデータ構造を扱う言語処理系が非常に簡潔に実装できることを示した．

ABSTRACT. 本研究では，並列プログラムに対する逆向き実行環境を実装した．Hoey らは，ブロック構造，手続き呼び出しを持つ並列プログラムの実行を逆向き に辿るために必須の情報を記録しながら実行し，その実行を逆向きに辿る手 法を提案している． ここでは，同様の並列プログラムを３番地コードにコンパイルする．順方 向の実行時は逆向き実行に必要な情報をスタックに保存し，その実行を逆向 きに辿る実行環境を実装した．この実行環境では，順方向の抽象命令を変換 することで逆方向の抽象命令を作成し逆向き実行を実現する．複数の抽象機 械を並列に実行するために抽象機械はpython のmultiprocessing モジュール を用いて実装した．

ABSTRACT. GPUで並列処理を実現するSIMD実行は，高い演算能力を実現する一方で，異なるスレッドが異なる分岐を生じた際に，全ての分岐経路を逐次的に実行する分岐発散という問題を生じる．分岐発散が生じる場合，部分冗長除去のような，特定の経路に式を挿入するコード最適化は，分岐発散を高める可能性があり，適用が難しい．部分冗長除去を，異なる繰返し間の冗長性を解析するように拡張したスカラ置換も同様にGPU向けプログラムへの適用は難しい．本研究では，分岐発散を考慮したスカラ置換と投機的コード移動を組み合わせることで，分岐発散の増大を抑えながら多くの冗長性を除去するだけでなく，分岐発散も低減する手法を提案する．本手法を．分岐発散を生じるプログラムに適用した結果，1.2倍の実行効率を実現できることを確認した．

ABSTRACT. 様々な高階プログラムの検証問題は HFL(N) 論理式の妥当性検査問題に帰着できる．郡らは HFL(N) 論理式の妥当性証明のための循環証明体系を提案した．本研究では，郡らの循環証明体系に基づいた，HFL(N) 論理式の妥当性の半自動証明の手法を提案する．郡らの証明体系では global trace condition と呼ばれる条件の検査が必要であり，半自動化における主要な課題となる．郡らの，Büchi オートマトンの包含判定問題への帰着による手法の代わりに，我々は Lee らが導入した size-change termination に基づく global trace condition の検査方法を提案する．我々の手法の最悪計算量は郡らの手法と同じだが，我々の手法の方が実践上より効率的に動作すると期待される．我々は提案手法に基づいた半自動化ツールを実装し，その有効性を評価した．

ABSTRACT. 本研究では, 2次元作図問題のための VPython ライブラリ draw2d を作成し，これを用いてガウスの正17角形の作図方法を実装した．正多角形の作図問題は正n角形の頂点の1つ (cos(2pi/n)，sin(2pi/n))の作図，特に cos(2pi/n) を作図すればよい．ガウスの定理より cos(2pi/17) が作図可能数であることが知られているが，これを作図するには二次方程式の解相当の点を求める作業を何度かくり返す必要がある.draw2d により定規とコンパスのみを使った作図を計算機上で再現することで正17角形の作図を完成させた.

ABSTRACT. 継続をプログラム中で扱うには control/prompt や shift/reset など継続を切り取って扱う限定継続演算子が使われる。その意味論は継続渡し形式(continuation-passing style; CPS)に変換することで与えられるが、これまでCPS変換の正当性はshift/reset入りの体系において議論されてきた。また、型システムにおいては、control/promptが含まれる体系は、shift/resetが含まれる体系と違い、継続が連なっているtrailという新しい概念を取り入れなければならない。そのためCPS変換においても扱う型が増え、正当性の証明は複雑になる。本研究では、定理証明支援系言語であるAgdaにおいてcontrol/promptが含まれた体系でのCPS変換を定式化し、正当性の証明を目指す。

ABSTRACT. 配列言語APLは配列の処理に長けており、例えばライフゲームや画像処理のような複雑な配列処理を簡潔に表現できる。一方でAPLは可読性に問題があり、そのため学習コストが高い。本研究ではAPLのアイデアを受け継ぎつつ、容易に理解できる表記の配列言語をOCaml上の埋め込みDSLとして実現する。デモではこのDSLを用いたライフゲームの簡潔な実装を実演する。

ABSTRACT. Rust言語における参照は生存期間が借用システムにより厳格に規定されている。 通常のRustプログラムでは参照の有効性を型システムが検査するものの、unsafe操作によって検査を迂回できる。 実世界ではunsafe Rustプログラムにおける無効な参照の使用に由来する未定義動作が報告されている。 この研究では、定理証明支援系Isabelle/HOL上で形式化されたRust意味論に基づくunsafe Rustプログラムの安全性の形式検証を提案する。 ケーススタディとして標準ライブラリ関数を含めたunsafe Rustプログラムの自動証明機構を活用した安全性および機能正当性の証明を紹介する。

ABSTRACT. 本研究では，50000×500行列と500×50000行列の行列積（結果は50000×50000行列で約20GBと大規模）を非同期I/Oにより同期の待ち時間を減らしつつout-of-core実行する逐次プログラムを開発するとともに，タスク並列言語Tascellによる並列化を行った．Tascellのワークスティールでは，一時的バックトラックに基づくことで優れた負荷分散が達成される．4台の計算ノードとして，ホストに接続された4基の57コアIntel Xeon Phi coprocessorを用いるとともに，非同期I/OによりNFSアクセスするデータの保存先にはホストのramdiskを利用した．性能評価の結果，ノード内32ワーカ利用時に逐次プログラムの約14倍の速度向上が得られた．これにより，Tascellを用いることでout-of-core行列積の並列化が可能なことを確認した．

ABSTRACT. 計算状態操作機構は，呼び出し元に眠る変数の値へのアクセスとして安全な合法的実行スタックアクセスを提供するもので，平常時の実行性能を保ちつつ，動的負荷分散などに利用できる．実装方式や得意とする利用法が異なる様々な計算状態操作機構がある．並列言語であるTascellやHOPEの並列言語処理系では，入れ子関数を備え，後に様々な計算状態操作機構が選べる中間言語が用いられている．本研究では，移植性に優れた変換に基づく計算状態操作機構を，2つ新たに並列言語処理系で利用可能とした．性能評価の結果，遅延判定コスト不要でそれ以外のコストも中庸なときに性能改善が得られた．

ABSTRACT. π計算は並行・分散計算の代表的なモデルである。石川はπ計算の停止性検証問題を逐次計算のものへ帰着させる健全な手法を提案した。彼はまずチャネルをサーバ用チャネルとそうでないものに分けた。次にサーバ用チャネルに対する受信（送信）を関数定義（呼出）に変換し、それ以外の送受信を削除した。この受信の削除のせいで受信する値に関する情報を失いその値を非決定的な値に置換したため、停止性検証能力は不十分だった。本研究では、篩型を用いて受信する値に関する情報を静的に解析し変換後のプログラムに反映させることで、石川の手法を改良する。またCHCの充足問題への帰着による型推論手続きを提案し、停止性検証器を実装した。

ABSTRACT. 分離論理はポインタ操作を含むプログラムの性質を証明するための体系である．分離論理において，再帰的データ構造を表す帰納的述語を無条件に許すと，エンテイルメント（論理式間の含意関係）の妥当性判定問題が決定不能になることが，ポストの対応問題からの帰着を用いて証明されている．本発表では，この決定不能性に対し，文脈自由文法の包含問題からの帰着による新しい証明を与える．さらに，文脈自由文法のGreibach標準形をエンコードする帰納的述語を考えることにより，Iosifらが与えたエンテイルメント判定問題を決定可能にする3条件，確立性，接続性，進行性のうち，接続性を弱めるだけで決定不能になることを証明する．

ABSTRACT. C/C++では，1つのメモリ区間に対して大きさが異なるロードとストアを実行する混合サイズアクセスが可能であり，実世界のソフトウェアで広く用いられている．しかし既存のC/C++向けのステートレスモデル検査器では，各ロードがただ1つのストアから値を読むことが仮定されており，混合サイズアクセスのあるプログラムを正しく検査できない．そこで本研究では，最新のステートレスモデル検査器GenMCにおいてロードを分割することで混合サイズアクセスに拡張する手法を提案する．提案手法はGenMCの最適性と漸近計算量を保存し，拡張したGenMCは合理的なオーバーヘッドで付属ベンチマークを全て検査できた．

ABSTRACT. 本研究の目的は，プログラム例を用いた文法の生成による，構文解析器を作成する手間や学習コストの削減と，言語の文法の設計の補助である． また，対話的に用いることを想定しており，対話的に用いるのに適した時間で計算できることも目的としている．

関連研究に対する本研究の特徴は，既存の言語の特徴などを考慮した文法の規則集を用い，プログラム例を構文解析できるように，規則集を編集することで，文法を生成することである． これによって，ユーザの操作回数の削減や，よく使われる形の規則の提示を狙う． 提案手法の実装によって判明した，規則集の編集において実行時間などの観点から有効だった工夫などについても発表する．

ABSTRACT. 代数的エフェクトとハンドラは、例外や副作用などの様々な計算効果を統一的かつ安全に実装することを可能にする。しかし、一般の代数的エフェクトで表現できるのは例外処理などの単方向フローを含むプログラムに限られており、ジェネレータや通信などの双方向フローを含むプログラムは表現できない。その問題を解決するために双方向性代数的エフェクトが提案された。 一方、Effektは代数的エフェクトを持つ言語である。Effektは代数的エフェクトをcapability渡しという独自の技法によって実現することで、型システムを簡素化している。 本研究ではEffektで双方向フローを含むプログラムを記述できるようにするためにEffektを双方向性代数的エフェクトで拡張する。具体的にはその実装、および形式化を行う。

ABSTRACT. 暗号通貨Tezos向けストレージシステムPlebeiaのデータ永続化処理の正しさを、プログラム検証用プログラミング言語F*を用いて検証した。F*はバックエンドにSMTソルバであるZ3を使用し、半自動的なプログラム検証を可能にする。本研究では、Plebeiaの内部データAをエンコードしてディスクに書き込み、その後ディスクから読み込みを行って内部データBを再構築した際に、AとBが等価であるための十分条件を明らかにした。検証には約17,000行のF*コードを要した。F*コードからコード抽出を行って得られたOCamlコードは、検証前の実装と同程度の速度で動作した。

ABSTRACT. プログラムの等価性の証明は，プログラムの正当性や，コンパイルや最適化といったプログラム変換の正しさを検証する上で重要である．一方，プログラムを書く上で，関数を引数とする関数（高階関数）は，プログラムの再利用性や抽象性を高める目的に有用である．高階関数の等価性証明は論理関係や双模倣等多くの既存手法があるが，自動化は難しい．一方，SMTソルバーは実用上重要な算術式に関する自動証明をある程度行うことができるが，高階関数を扱うことができない．そこで本研究では，算術式を扱えるよう拡張したλ計算を考え，SMTソルバーをオラクルとして用いて，拡張されたλ式の等価性を検証する手続きを提案する．

ABSTRACT. 本研究ではKoka言語のためのコンパイラ最適化として open floating を提案する。 Koka言語は代数的エフェクトとそれを解析するエフェクトシステムを備えた関数型言語である。 それらを備えることで例外や非決定計算などの計算エフェクトを使ったプログラムを安全かつ柔軟に書くことができる。 代数的エフェクトを効率よく実現するためには、言語の意味論やコンパイラの実装方式を工夫する必要があり、 Koka言語ではエフェクト割り当てに基づいた変換であるエビデンス変換をコンパイラに採用している。 本研究では、エビデンス変換を施す前の中間表現のエフェクト割り当てを最適化することで、コンパイラの生成コードの実行速度を向上させる。

ABSTRACT. 複数のエージェントが通信し合うことで計算を行うマルチエージェントシステムにおいて，エージェントからの通信を待たずにその時点での解を得る投機的計算を行うことができる．発表者らはこれまでにエージェントの構成や通信の方法が異なる複数の枠組みに関して，制約論理プログラミングに基づく投機的計算の手法を提案しているが，デフォルトの知識を表現する柔らかい制約を全て同程度のものとして扱っていた．本発表では，このような柔らかい制約の間に階層的な優先度を導入する方法を議論する．

ABSTRACT. 分散メモリ環境向けのプログラミングモデルとして、リモートのメモリ空間を明示的に読み書きするMPI-3 RMAと、ページ保護機能を用いてそれを隠蔽するページベース分散共有メモリ (PDSM) がある。PDSMが提供するより高水準の抽象化は、生産性を高める一方、キャッシュコヒーレンスに由来した通信とトラップが暗黙的に生じるため、MPI-3 RMAよりもコストが分かりにくく分散メモリ環境に適応したプログラミングが行いにくい。そこで本研究はPDSMの上での実行時コストの見積もりを助けるため、 MPI-3 RMA上の最新のPDSMであるArgoを性能解析し、PDSMのコストモデルを示す。これによってMPI-3 RMAを基準としたPDSMの追加コストが定量的に見積もれるようになった。

ABSTRACT. 逆コンパイラとは機械語を高級言語に変換するプログラムである。逆コンパイラの主要なフェーズは制御フローグラフから制御構造を復元することであるが、既存研究では復元結果の読みやすさを考慮していなかった。特に、gotoを用いた方が読みやすい場合があるにもかかわらず、gotoの少ない出力結果を目指していた。本研究では、逆コンパイラは元のソースコードと近い結果を出力すべきだという考えの下、制御構造を正確に復元するアルゴリズムを提案する。また、アルゴリズムの一部にグラフニューラルネットワークを用いることを提案する。実験の結果、goto 文判定の性能において提案手法が既存の逆コンパイラを上回った。

ABSTRACT. ライブプログラミング環境は，編集中のプログラムを継続的に実行し，プログラムの変更を即座にプログラマへフィードバックする機構である。特に我々が開発するKanonは，オブジェクトの参照関係をグラフとして表示する，データ構造に特化した実用的なライブプログラミング環境である。現在数多くのプログラミング言語が実用される一方，既存のライブプログラミング環境の多くは，特定のプログラミング言語に特化して実装されてきた。本研究では，汎言語的なデータ構造特化ライブプログラミング環境実現のための，メタJITコンパイラフレームワークであるGraal/Truffleを用いた汎言語的なデータ構造解析手法を提案する。