---
marp: true
title:  Gears OSでモデル検査を実現する手法について
paginate: true
---

# <!--fit--> Gears OSでモデル検査を実現する手法について
- 東恩納 琢偉
  - 琉球大学理工学研究科 情報工学専攻
---

# 研究目的

- OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こる。
- 本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性の保証をOSの機能として行うことを目指しており、本研究ではモデル検査をもちいた手法について発表する。
- また GearsOS そのものを GearsOS 上でモデル検査する手法についても考察する。
---

# Gears OS

- Continuation based C によって記述されている。
- 信頼性を保証する手法として、モデル検査による検証や、定理証明によるアプローチも行っている。

----

# Continution based C (CbC)

- Gear という単位で分割され、goto 文によって遷移する。
- codeGear は プログラムにおける処理記述になっている。
- また 変数や構造体といったデータは dataGear に保管される。
- 下の例題は CbC によって記述された codeGear である。
```
__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);

}

```

---

# goto
- CbC での遷移は軽量継続といいgoto 文を用いる。
- これは関数呼び出しと異なり、stackや環境を隠して持つことがありません。
- CbC において、処理を行うのは codeGear であるため、プログラムの状態の変化は codeGear によって決まる。
- よって CbC での遷移記述をそのまま状態記述とすることが出来る。



<center><img src="./pic/goto.svg" alt="" width="80%" height="80%" ></center>

----

# メタ計算
- 軽量継続である CbC は遷移する際に別の処理を挟む事が可能で、この処理をメタ計算という。
- メタ計算は meta codeGear で行われ、ここに検証用の処理を入れる事が出来る。
<center><img src="./pic/meta_gear2.svg" alt="" width="90%" height="90%" ></center>

----

# data Gear と meta dataGear

- CbC における入力は dataGear と呼ばれる構造体になっており、ノーマルレベル
とメタレベルがある。
- メタレベルには計算を行うCPUやメモリ、計算に関するノーマルレベルのdataGearもcontext に格納されている。

---

# stub CodeGear (メタレベルからノーマルレベルへの橋渡し)

- メタレベルから見ると、code Gearの入力はcontext ただ1つである。
- ノーマルレベルからメタレベルの context を直接参照してしまうことはできない。
- context から必要なノーマルレベルのdata Gearを取り出して、ノーマルレベルのcodeGearを呼び出し渡す処理を行う仲介役として、メタレベルの stub codeGearを用意する。

```
__code clearSingleLinkedStack(struct Context *context,struct SingleLinkedStack* stack,enum Code next) {
    stack->top = NULL;
    goto meta(context, next);
}

__code clearSingleLinkedStack_stub(struct Context* context) {
    SingleLinkedStack* stack = (SingleLinkedStack*)GearImpl(context, Stack, stack);
    enum Code next = Gearef(context, Stack)->next;
    goto clearSingleLinkedStack(context, stack, next);
} 
```

---

# プロセスであるcontext の並べ替えによる並列実行

- プログラムの非決定的な実行は、入力あるいは並列実行の非決定性から生じる。
- 並列実行の非決定性は、実行される codeGear の並び替えを生成し、contextの状態を数え上げる。
- これがモデル検査になる。
- 並び替えの数(プログラム全体の可能な状態)はとても巨大になる場合がある。
- 状態はデータベースに格納する。

---

# codeGearのatomicity

- codeGear は処理の基本単位であり、並列処理などにより割り込まれることなく記述された通りに実行される必要がある。
- 一般的には、他の codeGear が共有されたdataGearに競合的に書き込んだり、割り込みにより処理が中断したりする。
- GearsOS においては codeGear が正しくatomicに実行されるように実装する。

---

# モデル検査する仕様の記述法

- 検証したい内容を時様相論理式 p をつくり、対象のシステムの初期状態 s のモデル M があるとき、M,s |= p(M,s が p を満たすか)をモデル検査器を用いて調べることによって信頼性を保証する手法である。

- 時相論理式にはCTL(Computation Tree Logic) や LTTL(Linear Time Temporal Logic)といったものがあり、それぞれ計算木と線形時相論理式と言われるものである。


----

# 他のモデル検査実装例
- SPIN
 Promela (Process Meta Language)で仕様と実装を記述する。

- Java Path Finder
 JVM を直接シュミレーション実行する。
 様相論理ではなくassert 検証したい性質を記述する。

- XMV
 CMU で開発されたモデル検査器
 SAT solver 

----

# Geras OS のモデル検査

- CbC によって記述されており、CbC の記述そのものを状態遷移として落とし込む。
- par goto により複数スレッドの並行実行する。
- メタ計算によって並行実行のモデル検査を行う。


----

# Gears OS におけるモデル検査
1. GearsOS におけるモデル検査はcode gear 単位の順列組み合わせによって行われる。
2. codegear 実行後の状態を、データベースに格納する。
3. 新しい状態が生成されなくなった時モデル検査が終了する。
4. 哲学者５人が次の状態に進めなくなった時をデッドロックとして検出する。
5. 必要な状態はフォークの状態だけになるので、それ以外の状態は無視することができる。
6. これにより状態数を下げることができる。
7. 問題に合わせたメタ計算により、モデル検査の状態数を下げることができる。
8. GearsOS による検証用プログラムとして Dining Philosohers Ploblem (DPP）を用いる。

----
# DPP

<right><img src="./pic/dpp_image.svg" alt="" height="90%" ></right>

----
# DPP(dining philosohers ploblem)

- 5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。
- フォークは皿の間に１本ずつの計5本しかないため、すべての哲学者が同時に食事することはできず、また全員がフォークを1本ずつ持ってしまった場合、誰も食事することは出来ない。この状態をデッドロックとする。
-DPPは次の6つの状態からなる。 
`Pickup Right fork` ` Pickup Left fork` `eating` ` Put Right fork` `Put Left fork` ` Thinking `
----


# GearsOS におけるDPP実装(1/2)

- マルチスレッドでのデータの一貫性を保証する手法としてCheck and Set (CAS) を用いる。
- CAS を用いて値の比較、更新をアトミックに行う。
- CAS は書き込みの際に、書き込む MetaCodeGear に更新前と更新後の値を渡し、更新前の値が保存されているメモリ番地の値と比較し同じデータがであれば書き込みを行う。異なる場合はほかからの書き込みがあったとみなし、値の更新に失敗し、もう一度CASを行う。
- DPPの例題ではフォークがスレッドで共有されるデータにあたるので、CAS を用いることによってスレッド間での同期を行う。

----

# GearsOS におけるDPP実装(2/2)
- 5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表される。
- この状態遷移は goto next によって遷移し、metaCodeGear を 挟みメタレベルで各スレッドの状態を 各スレッドごとに用意した Memory Tree に保存する。
- Memory Tree はstateDBによってまとめられ、同じ状態は共有される。
- またDPPにおける状態遷移は無限ループであるため、stateDBを用いて同じ状態を検索することで、終了判定を行う。

----

<center><img src="./pic/model_checking.svg" width="50%" ></center>

----

# GearsOS でのモデル検査を実現する方法について

- DPP をGearsOS 上のアプリケーションとして実装する。
- DPP を codeGear のシャッフルの１つとして実行する。
- 可能な実行を生成する iterator
- 状態を記録する memory Tree と stateDB を作成する。

---

# モデル検査器の現状

- GearsOS 上での導出木の生成
- 生成した木のマーキングによる時相論理の検証

----

# Metaの入れ替え
- perl script を用いて、遷移先のmetaを置き換える事が可能となっている。
- 遷移先のmetaを切り替えることによって、ノーマルレベルで走るプログラムを書き換える事なく、mcMeta によるシングルスレッド実行と並列実行ようのランダム実行を行う事が出来る。

----

# モデル検査のフラグ管理
- モデル検査を行う際に全ての状態を網羅的に実行していく、この時実行した状態にフラグを立てていくことによって走った状態を記録しておく。
- フラグはeating のt_eating と、¬◇ eating　の f_F_eating フラグの2種類で、食事中といつか食事できないを表している。

----

# DPP　のメタ計算
- 導出木を作る時にはノーマルレベルの putdown_lfrok は　putdown_lforkPhilsImpl となり、context に代入を行うマクロである Gearef を使いCaS を行う。
その後 mcMeta に以降することで導出木の作成を行う

```
__code putdown_lfork(struct PhilsImpl* phils, __code next(...)) {
  struct AtomicT_int* left_fork = phils->Leftfor
  goto left_fork->set(-1, thinking);
 }

```
```
__code putdown_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)->newData = -1;
   Gearef(context, AtomicT_int)->next = C_thinkingPhilsImpl;
   goto mcMeta(context, left_fork->set);
}
```
----
# mcDPP
- フラグを確認しモデル検査を行っている。
```
void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcWorker, StateDB now,StateDB next, int check) {
  PhilsImpl* phils = (PhilsImpl*)GearImpl(mcWorker->mcContext, Phils, phils);
  int prev_now = now->flag;
  int prev_next = next->flag;
  enum Code nextc = mcWorker->mcContext->next;

  if (phils->self == 1 && nextc == C_putdown_rforkPhilsImpl ) {
    now->flag |= t_eating;
  }
  if ((next->flag & t_eating )||(next->flag & t_F_eating) ) {
    now->flag |= t_F_eating;
  }

  if ( prev_now != now->flag || prev_next != next->flag )
     mcWorker->change = 1;

  if (check) {
     if (!(now->flag & t_F_eating)) {
         printf("not <> eating\n");
     }
  }
}

```
----

# meta.pm

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

#my ($currentCodeGearName, $context, $next) = @_;

sub generateRandomMeta {
  my ($context, $next) = @_;
  return "goto random($context, $next);";
}

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

1;
```
----

# まとめ
- GearsOS上でDPPからの導出木を生成した。
- 生成した木にフラグを立て、これをmcDPP用いてモデル検査をおこなった。

- meta.pm を使うことでモデル検査を行う際のランダム生成を行う事が可能になった。

- GeearsOS で汎用モデル検査器を作ることができた。


----

# モデル検査における問題点

- 他のアプリケーションと違い、OS の記述はそれ自体が メタレベルのものであるため、それをemulationする方法を考える必要がある。
- TLB(Translation Lookaside Buffer ) という仮想記憶を物理アドレスに変換する際に使われるキャッシュ機能があり、これのemulation に工夫が必要となる。
- 検証内容によってこれらのemulation の方法をチューニングするため、未知のメタ計算、またはバグに対する検証方法が必要となる。
-ユーザーcontext が単純であっても OS は膨大な状態数を有するので、その全てを探索するのが厳しいと考えられる。

----


# 今後の展開
- 網羅的にプログラムを走破し、状態を展開して行くため同じ状態の組み合わせが出てくる。これらの組み合わせは抽象化し、状態数が増えすぎる事を抑える必要がある。
- 現在のData Gear は全て予め生成しておいたものでしかない。そのため生成が必要となる場合の方法を考える必要があり、またこの生成はノーマルレベルからは見えないようにしておく必要があるため工夫が必要となる。

- モデル検査でメモリの状態を保管していたiterator は実行履歴として、trace によって遡る事が可能であるため、これを利用することによってmcMeta にdebugger  を埋め込むことが可能であると考える。

----

# GearsOS の GearsOS によるモデル検査

- GerasOS そのものも codeGear で記述されている。
- CPU毎の C.context、共有するkernel のK.context、ユーザープログラムのU.context と考えることができ、これらはmeta dataGear であるK.context に含まれている。
- U.context がDPPのような単純なものならば、OS全体のcontext も複雑にはならないため、これらをGearsOSで実行することが可能になる。
- GearsOS を含む codeGear のシャッフル実行を行う事ができれば、DPPと同じようにモデル検査を行う事ができる。
- 検査する codeGear と検査される codeGear は同じものであるが、実行する meta codeGear を異なる。。
- 異なるmeta codeGear を指定してコンパイル出来る。

----
# OS 自体のモデル検査

- Gears OS は CbC で書かれている。そのため OS の動作であってもメタ計算を挟む事が可能である。
- CPU や kernel また ユーザープログラムのcontext として考える事によって、OS から独立しているものとして考える。

- またユーザーのcontext が単純なものであれば、OS 全体も複雑にはならないためDPPのようにシャッフル実行を行う事で、検証が可能であると考えられる。

----

# OS のモデル検査
- OS の全体を検証するのではなく、部分的な検証であればモデル検査出来ると考えられる。
- また小林らによって高次元プログラムの最悪時間計算量がｋ階の場合にｋ重指数完全であった高階モデル検査についての高速化手法が研究されている。

----