---
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のメタ計算フレームワーク
- GearsOSはPerlを中心としたメタコード生成のフレームワークが構築されている
    - 計算に必要なデータの入出力のメタ計算を主に生成していた
- メタレベルの処理は従来のものは手動で作る方が多かった
    - 計算で使うすべてのデータ構造の管理
    - 別のInterfaceの出力を受けるメタレベルのデータ管理など
- Perlでメタレベルに変換された後で気づくエラーも多い
    - 変換する前の時点でコード自体は間違えている
    - 変換されてしまった後なのでコードを見比べないと原因が不明

---
# GearsOSのメタ計算フレームワークとInterface
- CbCには無いモジュール化の仕組みとしてInterfaceがある
    - Perlフレームワーク上に構築
    - コンパイル時に等価な純粋なCbCに変換する
- Interfaceの機能が他の言語のInterfaceの機能とギャップがあった
    - 実装していないAPIがあっても、変換前の時点でエラーが出ないなど
- Interfaceの定義ファイルもあるものと無いものがあった
    - トランスパイラで統一な処理が出来ない

---
# Perlを中心としたフレームワークによるメタ計算の生成
- GearsOSの例題を作製する場合も、コピペや手書きが多発していた
    - フレームワークに実装したAPIを使って自動生成に変更したい
- Interfaceの機能充実も、 メタ計算の生成もCbCで行うのは難しい
    - Perlを中心としたフレームワークを活用したい
- コード変換(トランスパイル)を行うために必要な環境の整備もする必要がある
- Perlを中心としたトランスパイルシステムの整備、拡張を行った
    - GearsOSのメタ計算の生成がより柔軟かつ高い信頼性で可能となった

---
# GearsOSの基礎概念
- CodeGear、DataGear
- Interface
- GearsOSのビルドシステム
    - cmake
    - Perlトランスパイラ

---
# CbCとCodeGear(ノーマルレベル)
- 軽量継続で表現する単位をCodeGearと呼ぶ
- CodeGearはCの関数とアセンブラの中間の様に使える
- CodeGearは返り値の型の代わりに`__code`で宣言する

```c
__code insertTest2(struct StackTestImpl3* stackTest, struct Stack* stack, __code next(...)) {
    String* str = &ALLOCATE(context, String)->String;
    str->size = 100;
    goto stack->push((union Data*)str, pop2Test);
}
```


---
# 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)


---
# Interface
- GearsOSのモジュール化の仕組み
- Interface はある Data Gear と、それに対する操作(API)を行う Code Gear とその操作に用いる Data Gear の集合を表現する。
- JavaのInteface、Haskellの型クラスに相当する
- ContextにInterfaceの引数の保存場所がある
    - goto時にStubCodeGearでデータをとってくる
- `goto interfaceName->method()`のようにAPIを呼び出す
    - Perlトランスパイラが`goto meta()`に書き直す
    - `goto meta`はcontextから引数を取り出すMetaCodeGearに継続させるもの

---
# GearsOSのビルドシステム
- CMakeとPerlを使ってビルドする
    - CMakeはMakefileやbuild.ninjaを生成する
    - Perlは2種類のスクリプトが自動的に呼ばれる
- Perlでエラーを出すとCMakeがビルドを止める
    - 従来はエラーを出していなかったので怪しいコードを生成しても止まらない
![w:632 h:10cm](./geasflow1.svg)

---
# GearsOSのビルドシステム
- generate_stub.pl
    - GearsOSで拡張したCbCを1行ずつ読む
    - 純粋なCbCに変形したものを生成する
    - CbCコンパイラがコンパイルする前にコードを変換する
        - ユーザーが書いたGearsOSのソースコードにメタ情報をつける
        - コードからコードを生成する、トランスパイラ
- generate\_context.pl
    - Contextに関係するファイルを生成する
        - Contextの初期化ルーチン
        - CodeGear/DataGearの番号(enum)
    - 変換したプロジェクトで使うすべてのCbCファイルを入力で受け取る
    - すべてのCbCファイルを読み込み、使用しているCodeGearなどの情報を取得



---
# 主なGearsOSに導入された新機能
- Interfaceシステムの強化
- 手書きからの解放
- MetaCodeGearの入れ替え機能の追加

---
# Interfaceシステムの強化
- Interface構文の簡素化
    - より簡潔に明確に記述できるように定義した。
- Interfaceの実装の型の導入
    - GearsOSでの型定義の方法に一貫性が生まれた
- Interfaceの引数の確認
- Interfaceで未定義のAPIの検知
- InterfaceにないAPIの呼び出しの検知
    - コード変換前にPerlレベルでエラーを発生させた
---
# 手書きからの解放
- 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<Type, Impl>{
        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の実装時の型名の省略
- 従来は型名を必ず書かなければならなかった
    - これはメタ情報なので変換時に書き換える
### 従来

```c
__code pickup_lforkPhilsImpl(struct PhilsImpl* phils, __code next(...)) {
    struct AtomicT_int* left_fork = phils->Leftfork;
    goto left_fork->checkAndSet(-1, phils->self, pickup_rforkPhilsImpl, eatingPhilsImpl);

}
```
### 現在

```c
__code pickup_lfork(struct PhilsImpl* phils, __code next(...)) {
    struct AtomicT_int* left_fork = phils->Leftfork;
    goto left_fork->checkAndSet(-1, phils->self, pickup_rfork, eating);

}
```

---
### トランスパイル前
```c
__code pickup_lfork(struct PhilsImpl* phils, __code next(...)) {
    struct AtomicT_int* left_fork = phils->Leftfork;
    goto left_fork->checkAndSet(-1, phils->self, pickup_rfork, eating);

}
```
### トランスパイル後
```c
__code pickup_lforkPhilsImpl(struct Context *context,struct PhilsImpl* phils, enum Code next) {
    struct AtomicT_int* left_fork = phils->Leftfork;
    Gearef(context, AtomicT_int)->atomicT_int = (union Data*) left_fork;
    Gearef(context, AtomicT_int)->oldData = -1;
    Gearef(context, AtomicT_int)->newData = phils->self;
    Gearef(context, AtomicT_int)->next = C_pickup_rforkPhilsImpl;
    Gearef(context, AtomicT_int)->fail = C_eatingPhilsImpl;
    goto meta(context, left_fork->checkAndSet);

}
```
---
# Interfaceのパーサーの導入
- PerlでのInterfaceの情報の取得は、CbC自体のファイルの解析処理と共通だった
    - Interfaceならではの情報が取れない
    - スクリプトに直接書かれているので他のツールが使えない
- モジュール化したInterfaceのパーサーを導入した
    - Perlフレームワークを使う一連のツールの作製が可能になった
        - InterfaceとImplを見た実装の雛形ファイルの作製ツール
        - コード変換時にInterfaceのAPIに関連するチェック機能


---
# Interfaceの実装の雛形生成コマンドの実装
- Interfaceと実装する型が決まると、最低限書かないといけないCodeGearが決まる
- 従来は手作業でCbCファイルにCodeGearの定義を書いて実装していた
    - コンストラクタも手書き
- JavaはIDEで、golangはコマンドとして雛形を生成するものを用意している
    - GearsOSでも導入した
- 実装の型ファイルを引数で渡すと雛形を生成する
```shell
$perl too/impl2cbc.pl SingleLinkedStack.h
```

---
# 生成された雛形cbcの一部
- 各CodeGearに実装したい内容をすぐに書き始めることが可能になった
    - 自動生成されるのでエラーの発生も抑えられる

```c
#include "../../../context.h"
#interface "Stack.h"

Stack* createSingleLinkedStack(struct Context* context) {
    struct Stack* stack  = new Stack();
    struct SingleLinkedStack* single_linked_stack = new SingleLinkedStack();
    stack->stack = (union Data*)single_linked_stack;
    ...
    stack->pop2 = C_pop2SingleLinkedStack;
    stack->get2 = C_get2SingleLinkedStack;
    return stack;
}
...

__code push(struct SingleLinkedStack* stack,union Data* data, __code next(...)) {

    goto next(...);
}
```

---
# PerlトランスパイラでのInterfaceのエラー生成
- Interfaceの実装時に様々なミスをする可能性がある
    - APIを完全に実装していない
    - 呼び出しの引数を間違えている
    - 無いAPIを呼び出している
- 従来は変換した後CbCコンパイラがコンパイルする際や、実行時にしかエラーが出なかった
    - どの記述でエラーが出たのかの特定が困難
    - CbCコンパイラがコンパイルする前にトランスパイラで検知したい

---
# 実装をし忘れているAPIがあった場合のエラー終了
- PerlトランスパイラでのInterfaceのエラー生成
    - CbCコンパイラが動く前にエラーを検知

```
[ 33%] Generating c/examples/DPP2/PhilsImpl.c
[ERROR] Not define eating at examples/DPP2/PhilsImpl.cbc
make[3]: *** [CMakeFiles/DPP2.dir/build.make:101: c/examples/DPP2/PhilsImpl.c] Error 25
make[2]: *** [CMakeFiles/Makefile2:442: CMakeFiles/DPP2.dir/all] Error 2
make[1]: *** [CMakeFiles/Makefile2:450: CMakeFiles/DPP2.dir/rule] Error 2
make: *** [Makefile:293: DPP2] Error 2
```

---
# Context定義ファイルの自動生成
- ContextはすべてのDataGearの型情報をunion Dataとして持つ必要がある
    - すべてのDataGearの定義をunion Dataの定義内に書く
- これは今まで手書きで作製していた
    - Interfaceの型定義ファイルを導入したので、自動生成が可能になった
- ビルド時に使用しているDataGearを回収し、 context.hを作製する
```c
union Data {
    struct Stack {
        ...
    } Stack;
    struct SingleLinkedStack {
        ...
    } SingleLinkedStack;
}
```
---
# StubCodeGear
- 実行したいCodeGearの直前に実行されるMetaCodeGear
- contextからDataGearを取り出す操作をする
- すべてのノーマルレベルのCodeGearに付随する
    - Perlトランスパイラでビルド時に自動生成
![w:632 h:10cm](./stubCodeGear.svg)

---
## 別のInterfaceの出力を受けるCodeGearのメタ計算部分の自動生成
- Stackから`data`と`data1`を受け取ろうとする例
    - 意図した通りに動かない

```c
__code pop2Test(struct StackTestImpl3* stackTest, struct Stack* stack, __code next(...)) {
    goto stack->pop2(pop2Test1);
}


__code pop2Test1(struct StackTestImpl3* stackTest, union Data* data, union Data* data1, struct Stack* stack, __code next(...)) {
    String* str = (String*)data;
    String* str2 = (String*)data1;

    printf("%d\n", str->size);
    printf("%d\n", str2->size);
    goto next(...);
}
```

---
## 別のInterfaceの出力を受けるCodeGearのメタ計算部分の自動生成
- Interfaceの継続に別のInterfaceを渡すと値の受け渡しが上手くいかない
    - StubCodeGearがおかしい

```c
__code pop2Test1StackTestImpl3_stub(struct Context* context) {
  StackTestImpl3* stackTest = (StackTestImpl3*)GearImpl(context, StackTest, stackTest);
  Data* data = Gearef(context, StackTest)->data;
  Data* data1 = Gearef(context, StackTest)->data1;
  Stack* stack = Gearef(context, StackTest)->stack;
  enum Code next = Gearef(context, StackTest)->next;
  goto pop2Test1StackTestImpl3(context, stackTest, data, data1, stack, next);
}
```


---
- メタ計算部分で取得するcontextの場所が異なっているのが問題
    - 取得する場所を手書きする必要があった

![w:732 h:13cm](./stackTest1.svg)

---
## 別のInterfaceの出力を受けるCodeGearのメタ計算部分の自動生成
- `goto interface->method()`している箇所を読み取る
    - `interface`がどのInterfaceなのかをPerlトランスパイラで特定させた
    - 特定したInterfaceをパーサーを呼び出して情報を取得
    - APIごとに出力があるかを調査
- 出力があったら、継続で渡しているCodeGearの入力を、呼び出しているInterfaceからとるように修正
    - データの取り出しはStubでしているので、新たなStubを作製した

---
# メタ計算の切り替えAPI
- CodeGearが継続するMetaCodeGearを自由に選択できるPerlモジュールを導入した
    - 従来はデフォルトで設定されるMetaCodeGearにしか継続しなかった
    - Perlモジュールを書くことで特定のCodeGearの継続先を変更可能にした
- 様々な処理をMetaCodeGearですることが可能になった
    - すでにモデル検査用のメタ計算を入れることが出来た

![w:932 h:10cm](./metapm.svg)


---
# まとめ
- Perlトランスパイラのフレームワークの機能を充実させた
- Interfaceシステムを改良した
    - 型定義ファイルの導入を行った
        - 定義方法に一貫性が出た
    - Perlトランスパイラで警告を発生させるようになった
- 従来手書きしていたメタな定義をビルド時に自動的に生成するようにした
    - 煩雑な処理や手で実装することによるバグの混入を回避
- MetaCodeGearの制御をユーザー側で行えるようにした
    - モデル検査をメタ計算として自在に組み込むことが可能となった

---

```perl
sub replaceMeta {
  return (
    [qr/PhilsImpl/ => \&generateMcMeta],
  );
}

sub generateMcMeta {
  my ($context, $next) = @_;
  return "goto mcMeta($context, $next);";
}
```