--- marp: true title: GearsOSのメタ計算 paginate: true --- # GearsOSのメタ計算 - 清水 隆博 - 琉球大学理工学研究科 - 198584B - 河野研 --- # 研究発表の構成 - 研究目的 - CbC、GearsOSの基礎概念 - GearsOSの新機能 - 本研究での新たなGearsOSのシステムの解説 - GearsOSのInterfaceシステムの改善 - Perlトランスパイラの改善 --- # 研究目的 - OSとアプリケーションの信頼性の保証したい - OSそのものも巨大なプログラム - プログラムの信頼性の保証にはテストが使われる - 並列並行処理などのバグや、そもそもOSを構成する処理が巨大 - テストコードで信頼性を保証しきれない - 形式手法を用いてテストに頼らず信頼性を保証したい - 既存のソースコードに形式手法を導入できるフレームワークを構築したい --- # ノーマルレベルとメタレベルを用いた信頼性の向上 - プログラムの実行部分は以下の2つからなる - 入力と出力の関係を決める計算(ノーマルレベル) - プログラムを実行したり、 信頼性を保証するために必要な計算(メタレベル) - メタレベルの例 - メモリやCPUの資源管理 - システムコールの動作(副作用) - 並行実行(他のプロセスとの干渉) - モデル検査(可能な実行を列挙する方式の実行) - 証明(入力時と出力時の論理的な条件)、(invariant) - メタレベルの計算として信頼性を保証する --- # メタレベルの計算とGearsOS - ノーマルレベル、メタレベルを一貫して記述できる言語CbCを用いてGearsOSを開発している - CbCを使うとメタレベルの処理を分離して書ける - メタレベルの処理を全部手で書くのは面倒 - メタレベルの処理を自動生成してくれるフレームワークを導入したい - フレームワークに乗って実装すると等価なCbCに変換される - CbCレベルではメタレベルの処理とノーマルレベルの処理が見れる - メタ計算を自分で定義できるようにしたい - 実装のコードをほとんど変えずにモデル検査を導入できるようにしたい --- # GearsOSのメタ計算フレームワーク - 従来もPerlを中心としたメタコード生成のフレームワークを構築していた - 計算に必要なデータの入出力のメタ計算を主に生成していた - しかしGearsOSのメタレベルの処理は従来のものは手動で行う方が多かった - 計算で使うすべてのデータ構造の管理 - 別のInterfaceの出力を受けるメタレベルのデータ管理など - Perlでメタレベルに変換された後で気づくエラーも多い - 変換する前の時点でコード自体は間違えている - 変換されてしまった後なのでコードを見比べないと原因が不明 --- # GearsOSのプログラミングフレームワーク - GearsOSはCbCには無いモジュール化の仕組みとしてInterfaceがある - Perlフレームワーク上に構築されている - 変換時に等価な純粋なCbCに変換される - Interfaceの機能が他の言語のInterfaceの機能とギャップがあった - 実装していないAPIがあっても、変換前の時点でエラーが出ない - 引数の値が揃っていなくても、変換前の時点でエラーが出ない - 存在していないAPIを呼んでも、変換前の時点でエラーが出ない - Interfaceの定義ファイルもあるものと無いものがあった - トランスパイラで統一な処理が出来ない --- # Perlを中心としたフレームワークによるメタ計算の生成 - GearsOSの例題を作製する場合も、コピペや手書きが多発していた - フレームワークに実装したAPIを使って自動生成に変更したい - Interfaceの機能充実も、 メタ計算の生成もCbCで行うのは難しい - Perlを中心としたフレームワークを活用したい - コード変換(トランスパイル)を行うために必要な環境の整備もする必要がある - 本研究ではPerlを中心としたトランスパイルシステムの整備、拡張を行った - GearsOSのメタ計算の生成がより柔軟かつ高い信頼性で可能となった --- # GearsOSの基礎概念 - CodeGear、DataGear - Interface - par goto - GearsOSのビルドシステム - cmake - Perlトランスパイラ --- # CbCとCodeGear(ノーマルレベル) - 軽量継続で表現する単位をCodeGearと呼ぶ - CodeGearはCの関数とアセンブラの中間の様に使える - CodeGearは返り値の型の代わりに`__code`で宣言する --- # DataGear - GearsOSで扱うデータの単位 - Cの構造体の形でメタレベルでは表現される - GearsOS自体の処理にかかわるMetaDataGearが存在する - Context(プロセス) - TaskManager - Worker - ... - DataGearの定義ではInterfaceシステムが使用できる --- # Context(1) - 従来のOSのプロセスに相当する機能(MetaDataGear) - GearsOSでcontextを触るのはメタ計算部分だけ - ノーマルレベルではcontextに降れない - 従来は手書きでヘッダファイルの中に定義 - context.h - Context自体は構造体で定義されている - Contextの要素にDataGearの型がすべてはいった共用体がある - context.hで同様に定義 --- # Context(2) - GearsOSでのプログラム実行に必要な情報を持っている - DataGearの型定義 - CodeGearの名前とStubCodeGearへの対応 - goto時に引数を書き込むDataGearごとの場所 - DataGearを管理するヒープ情報 ![w:532 h:10cm](./context.svg) --- # StubCodeGear - 実行したいCodeGearの直前に実行されるMetaCodeGear - contextからDataGearを取り出す操作をする - すべてのノーマルレベルのCodeGearに付随する - Perlトランスパイラでビルド時に自動生成 ![w:532 h:10cm](./stubCodeGear.svg) --- # Interface - GearsOSのモジュール化の仕組み - Interface はある Data Gear と、それに対する操作(API)を行う Code Gear とその操作に用いる Data Gear の集合を表現する。 - JavaのInteface、Haskellの型クラスに相当する - ContextにInterfaceの引数の保存場所がある - goto時にStubCodeGearでデータをとってくる --- # GearsOSのビルドシステム - CMakeとPerlを使ってビルドする - CMakeはMakefileやbuild.ninjaを生成する - Perlは2種類のスクリプトが自動的に呼ばれる - Perlでエラーを出すとCMakeがビルドを止める - 従来はエラーを出していなかったので怪しいコードを生成しても止まらない ![w:632 h:10cm](./geasflow1.svg) --- # GearsOSのビルドシステム - generate_stub.pl - GearsOSで拡張したCbCを受け取り、純粋なCbCに変形したものを生成する - CbCコンパイラがコンパイルする前にコードを変換する - ユーザーが書いたGearsOSのソースコードにメタ情報をつける - コードからコードを生成するので、トランスパイラと言える - generate\_context.pl - Contextに関係するファイルを生成する - Contextの初期化ルーチン - CodeGear/DataGearの番号(enum) - 変換したプロジェクトで使うすべてのCbCファイルを入力で受け取る - すべてのCbCファイルを読み込み、使用しているCodeGearなどの情報を取得 --- # GearsOSに導入された新機能 - ARMクロスコンパイル用のCMakeの定義 - ARM用のアーキテクチャに向けてクロスコンパイルするCMakeを定義 - GearsOSのビルドシステムに手を加えずにクロスコンパイルが可能 - **Interface構文の簡素化** - より簡潔に明確に記述できるように定義した - **Interfaceの実装の型の導入** - GearsOSでの型定義の方法に一貫性が生まれた --- # GearsOSに導入された新機能 ## Interfaceシステムの強化 - Interface構文の簡素化 - より簡潔に明確に記述できるように定義した。 - Interfaceの実装の型の導入 - GearsOSでの型定義の方法に一貫性が生まれた - Interfaceの引数の確認 - Interfaceで未定義のAPIの検知 - InterfaceにないAPIの呼び出しの検知 - コード変換前にPerlレベルでエラーを発生させた --- # GearsOSに導入された新機能 ## 手書きからの解放 - Interfaceの雛形ファイルの作製スクリプトの導入 - 別のInterfaceからの出力を取得するStubの自動生成 - 実装のCodeGear名からメタ情報の切り離し - メタな型情報はビルド時に付与される - DataGearの型集合ファイルであるcontext.hの自動生成 - GearsOSの初期化ルーチンの自動生成 --- # GearsOSの新機能 - **自由なMetaCodeGearの作製、継続の入れ替え機能** - Perlトランスパイラの変換ルーチンのデバッグ機能の追加 - ジェネリクスのサポート --- # Interfaceの改良 - 従来のInterfaceにまつわるPerlのフレームワークを改良した - CbCの変換後のコードでなく、Perlレベルでエラー検知可能になった --- # Interfaceの定義構文の改良 - 従来は引数とCodeGearの定義を別けて記述していた - Interfaceの宣言なので、書ける変数は引数/出力のもののみ - Javaのクラス変数やインスタンス変数のようなものだと思われてしまった - GearsOSに慣れてない - シンタックスが問題 - シンタックスをgolangやJavaのInterfaceを参考に簡潔なものにした --- # 従来のInterface - 引数の組とAPI(CodeGear)は別けて記述する必要があった ```c typedef struct Stack{ union Data* stack; union Data* data; union Data* data1; __code whenEmpty(...); __code clear(Impl* stack,__code next(...)); __code push(Impl* stack,Type* data, __code next(...)); __code pop(Impl* stack, __code next(Type* data, ...)); __code pop2(Impl* stack, __code next(Type* data, Type* data1, ...)); __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...)); __code get(Impl* stack, __code next(Type* data, ...)); __code get2(Impl* stack, __code next(Type* data, Type* data1, ...)); __code next(...); } Stack; ``` --- # 定義し直したInterface構文 - APIのみを記述すれば良くなった ```c typedef struct Stack<>{ __code whenEmpty(...); __code clear(Impl* stack,__code next(...)); __code push(Impl* stack,Type* data, __code next(...)); __code pop(Impl* stack, __code next(Type* data, ...)); __code pop2(Impl* stack, __code next(Type* data, Type* data1, ...)); __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...)); __code get(Impl* stack, __code next(Type* data, ...)); __code get2(Impl* stack, __code next(Type* data, Type* data1, ...)); __code next(...); } Stack; ``` --- # Implementの型定義ファイルの導入 - Interfaceは型定義ファイルがあったが、実装側はなかった - context.h上にメタな構造体に直した実装の型を手で書いていた - これはメタ情報なので手で書きたくない - 型定義の一貫性がない - 実装側にも型定義ファイルを導入して一貫性を持たせたい - Perlトランスパイラフレームワークで利用可能 --- # Implementの型定義 - 基本はInterfaceと同じシンタックス - どのInterfaceを実装しているかを`Impl`の後ろに書く - Implの場合はフィールド変数を定義できる - `実装名.h`の命名規則 (`PhilsImp.h` ) ```c typedef struct PhilsImpl <> impl Phils { int self; struct AtomicT_int* Leftfork; struct AtomicT_int* Rightfork; __code next(...); } PhilsImpl; ``` --- # Interfaceの実装 - 定義したInterfaceは実装する必要がある - Stack Interfaceの場合はSingleLinkedStackなど - cbcファイルにCodeGearやコンストラクタを定義し、 型はcontext.hに直接書く ```c __code popSingleLinkedStack(struct SingleLinkedStack* stack, __code next(union Data* data, ...)) { if (stack->top) { data = stack->top->data; stack->top = stack->top->next; } else { data = NULL; } goto next(data, ...); } ``` ```c struct SingleLinkedStack { struct Element* top; } SingleLinkedStack; ``` --- # Context定義ファイルの自動生成 - ContextはすべてのDataGearの型情報をunion Dataとして持つ必要がある - すべてのDataGearの定義をunion Dataの定義内に書く - これは今まで手書きで作製していた - Interfaceの型定義ファイルを導入したので、自動生成が可能になった - ビルド時に使用しているDataGearを回収し、 context.hを作製する ```c union Data { struct Stack { ... } Stack; struct SingleLinkedStack { ... } SingleLinkedStack; } ``` --- # Interfaceのパーサーの導入 - PerlでのInterfaceの情報の取得は、CbC自体のファイルの解析処理と共通だった - Interfaceならではの情報が取れない - スクリプトに直接書かれているので他のツールが使えない - モジュール化したInterfaceのパーサーを導入した - Perlフレームワークを使う一連のツールの作製が可能になった - InterfaceとImplを見た実装の雛形ファイルの作製ツール - コード変換時にInterfaceのAPIに関連するチェック機能 --- # メタ計算の切り替え機能 - CodeGearが継続するMetaCodeGearを自由に選択できるPerlモジュールを導入した - 従来はデフォルトで設定されるMetaCodeGearにしか継続しなかった - Perlモジュールを書くことで特定のCodeGearの継続先を変更可能にした - 様々な処理をMetaCodeGearですることが可能になった - すでにモデル検査用のメタ計算を入れることが出来た(東恩納さんの修論) ![w:932 h:10cm](./metapm.svg) --- # まとめ - Perlトランスパイラのフレームワークの機能を充実させた - 型定義ファイルの導入、呼び出しシンタックスの導入を行った - DataGearの定義方法に一貫性が出た - 従来手書きしていたメタな定義をビルド時に自動的に生成するようにした - 煩雑な処理や手で実装することによるバグの混入を回避 - MetaCodeGearの制御をユーザー側で行えるようにした - モデル検査をメタ計算として自在に組み込むことが可能となった - Interfaceシステムを改良し、Perlトランスパイラで警告を発生させるようになった - 他言語のInterfaceと同様に使うことができた --- ```perl sub replaceMeta { return ( [qr/PhilsImpl/ => \&generateMcMeta], ); } sub generateMcMeta { my ($context, $next) = @_; return "goto mcMeta($context, $next);"; } ```