---
marp: true
title: GearsOSのメタ計算
paginate: true
---


#  GearsOSのメタ計算

- 清水 隆博
    - 琉球大学理工学研究科
    - 198584B
    - 河野研

---
# 研究発表の構成
- 研究目的
- CbC、GearsOSの基礎概念
- 従来のGearsOSの課題
- 本研究での新たなGearsOSのシステムの解説
    - GearsOSのInterfaceシステムの改善
    - Perlトランパイラの改善


---

# 研究目的

- アプリケーションの信頼性を保証したい
    - この為には土台のOSの信頼性を高く保証する必要がある
- OSそのものも巨大なプログラム
    - プログラムの信頼性の保証にはテストが一般的に使われる
- 並列並行処理など起因するバグや、そもそもOSを構成する処理が巨大
    - テストコードで信頼性を保証しきれない
- 形式手法を用いてテストに頼らず信頼性を保証したい
    - 定理証明
    - モデル検査

---

# ノーマルレベルとメタレベルを用いた信頼性の向上

- プログラムの実行部分は以下の2つからなる
    - 入力と出力の関係を決める計算(ノーマルレベル)
    - プログラムを実行したり、 信頼性を保証するために必要な計算(メタレベル)
- メタレベルの例
    - メモリやCPUの資源管理
    - システムコールの動作(副作用)
    - 並行実行(他のプロセスとの干渉)
    - モデル検査(可能な実行を列挙する方式の実行)
    - 証明(入力時と出力時の論理的な条件)、(invariant)
- メタレベルの計算として信頼性を保証する

---
# メタレベルの計算とGearsOS
- ノーマルレベル、メタレベルを一貫して記述できる言語CbCを用いてGearsOSを開発している
- GearsOSのメタレベルの処理は従来のものは手動で行うものが多かった
    - 計算で使うすべてのデータ構造の管理
    - 別のInterfaceの出力を受けるメタレベルの処理
- Perlでメタレベルに変換された後で気づくエラーも多い
    - ノーマルレベルで検知したい

---

# モデル検査
- プログラムの可能な実行を数え上げて仕様を満たしているかどうかの確認
- 実際に想定されるパターンを全て動かして検証する
- デッドロック発生の検知
  - JavaPathFinderなど
- 状態爆発が問題になる
- Spinを用いる方法では、 promelaという言語で実装し直す必要がある
- 実装を変更せず、カジュアルにモデル検査を行いたい

---

# 定理証明支援系
- 論理学的なモデルに変更して証明する
  - Agda
  - Coq
- HoareLogicを用いる
    - PreCondition -> Statement -> PostCondition
- 従来の方法ではStatementには限られたコマンドしか使えない
    - ループは不変条件を使うが、 条件を見つけることが一般的には困難
    - 実装言語と同じ記述で証明をすることはできない

---
# GearsOSでの信頼性の保証
- メタレベルのみで信頼性の保証を行う
    - ノーマルレベルでの記述は変更しない
- Continuation Based C(CbC)をつかって、ノーマルレベルとメタレベルの分離を行う
- C言語の下位言語であり、 いくつかのCコンパイラ上で実装している
- C言語の構文は使用可能だが、 関数呼び出しの他に軽量継続を持つ
    - 関数呼び出し時のスタックの操作を行わず`jmp`命令で次の処理に移動する
    - schemaなどと違い環境を持たず継続するために軽量継続と呼ぶ

---
# GearsOSでの信頼性の保証

- デフォルトのメタレベルの計算は自動生成される
- 資源管理あるいは検証用のメタ計算は必要に応じて挿入する
- これにより大きなコード変更が無くモデル検査や定理証明を行うことができる
- モデル検査や定理証明の困難さはメタレベルのプログラミングとして吸収する
    - 例えばOSで使用するデータ構造に合わせたモデル検査用の状態圧縮
    - OSの検証に利用できるinvariantの提供
- CbCを用いたOSであるGearsOSを開発している



---
# 研究発表の構成
- 研究目的
- **CbC、GearsOSの基礎概念**
- 従来のGearsOSの課題
- 本研究での新たなGearsOSのシステムの解説
    - GearsOSのInterfaceシステムの改善
    - Perlトランパイラの改善

---
# 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の型クラスに相当する
- GearsOSではこの他にもgoto時の値の保管に利用される

---
# Interfaceの定義
- GearsOSで拡張したtypedef構文で宣言する
    - 入出力の引数と、CodeGearを列挙する

```c
typedef struct Stack<Type, Impl>{
        union Data* stack;
        union Data* data;
        union Data* data1;
        /* Type* stack; */
        /* Type* data; */
        /* Type* 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の実装
- 定義した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;
```

---
# メタレベルからみたInterface
- Cの構造体になる
- CodeGearはCodeGearの番号で持ち歩く
- 定義はcontext.h内のunion Dataの定義に書く
    - union DataはすべてのDataGearの型をもつ

```c
    struct Stack {
        union Data* stack;
        union Data* data;
        union Data* data1;
        enum Code clear;
        enum Code push;
        enum Code pop;
        enum Code pop2;
        enum Code isEmpty;
        enum Code get;
        enum Code get2;
        enum Code next;
        enum Code whenEmpty;
    } Stack;
```

---
# メタレベルからみたInterface
- 構造体にコンストラクタを使って値を書き込み、Interfaceを表現
    - 実装のオブジェクト(構造体)そのものへのポインタ
    - 定義したAPIに対応するenum Code(CodeGearの番号の連番)
        - APIの名前ごとに、実装のCodeGearの番号を代入する
```c
Stack* createSingleLinkedStack(struct Context* context) {
    struct Stack* stack = new Stack();
    struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack();
    stack->stack = (union Data*)singleLinkedStack;
    singleLinkedStack->top = NULL;
    ...
    stack->get2  = C_get2SingleLinkedStack;
    stack->isEmpty = C_isEmptySingleLinkedStack;
    stack->clear = C_clearSingleLinkedStack;
    return stack;
}
```

---
# GearsOSのビルドシステム
- CMakeを使ってビルドする
    - CMakeはMakefileやbuild.ninjaを生成する
- CbCコンパイラがコンパイルする前にPerlでコードを変換する
    - ユーザーが書いたGearsOSのソースコードにメタ情報をつける
    - generate_stub.plが行う
- 入力をもとにCodeGear/DataGearの番号も、コンパイル前に自動で生成する
    - generate\_context.plがおこなう

---
# GearsOSのビルドシステム
- Perlが最低2回よばれる
    - generate_stub.plはCbCファイル毎に実行される
    - generate_stub.plはトランスパイラする
        - ソースコードからソースコードに変換する処理系
![w:632 h:10cm](./geasflow1.svg)



---
# 研究発表の構成
- 研究目的
- CbC、GearsOSの基礎概念
- **従来のGearsOSの課題**
- 本研究での新たなGearsOSのシステムの解説
    - GearsOSのInterfaceシステムの改善
    - Perlトランパイラの改善



---
# GearsOSの課題(1)
- Interfaceシステムが不十分
    - 定義する際の構文が混乱を仕様とずれた記述を誘発させていた
    - 未実装のAPIがあっても警告が発生しない
    - メソッド呼び出し時の引数の数が足りなくても警告が発生しない
    - 定義していないAPIを呼び出してもエラーが出ない
    - 並行呼び出しに対応していなかった
- Interfaceの実装の型には型定義ファイルが存在しなかった
    - 型定義の方法の一貫性がなかった
    - メタ情報を手動で実装する必要性があった

---
# GearsOSの課題(2)
- Interface間の連携が上手くいっていなかった
    - 入出力の受け取りするメタ部分を手動で実装する必要があった
- メタレベルの計算、データの定義を従来は手動で行っていた
    - 自動的にコンパイル時に決定するはずの情報をすべて手書き
- メタレベルのCodeGearの定義やユーザーからの制御が困難であった
    - モデル検査などをメタ計算として定義できない
- 書いたGearsOSのプログラムを、メタを含むコードに変換し、コンパイルしないとバグに気づかない状態があった
    - メタを含むコードに変換する前に気づきたい
- 例題を作製する際にコピペを行う回数が多く、バグを発生させがちであった

---
# GearsOSの課題(1)
- **Interfaceシステムが不十分**
    - 定義する際の構文が混乱を仕様とずれた記述を誘発させていた
    - 未実装のAPIがあっても警告が発生しない
    - メソッド呼び出し時の引数の数が足りなくても警告が発生しない
    - 定義していないAPIを呼び出してもエラーが出ない
    - 並行呼び出しに対応していなかった
- Interfaceの実装の型には型定義ファイルが存在しなかった
    - 型定義の方法の一貫性がなかった
    - メタ情報を手動で実装する必要性があった

---
# Interfaceの定義構文の改良
- 従来は引数とCodeGearの定義を別けて記述していた
    - Interfaceの宣言なので、書ける変数は引数/出力のもののみ
- Javaのクラス変数やインスタンス変数のようなものだと思われてしまった
    - GearsOSに慣れてない
    - シンタックスが問題
- シンタックスをgolangやJavaのInterfaceを参考に簡潔なものにした

---
# 従来のInterface

# 定義し直したInterface構文

---
# Implementの型定義ファイルの導入
- Interfaceは型定義ファイルがあったが、Implはなかった
    - generate_stub.plでImplの型は別ファイルからとってなかった為
- 自分でcontext.h上にimplの型を書いていた
    - これはメタ情報なので手で書きたくない
    - 型定義の一貫性がない
- Implementにも型定義ファイルを導入して一貫性を持たせたい

---
# 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;
```

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