Gears OSでモデル検査を実現する手法について

  • 東恩納 琢偉
    • 琉球大学理工学研究科 情報工学専攻

研究目的

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

Gears OS

  • 軽量継続を基本とする言語 Contnution based C を用いて記述されている。
  • アプリケーションやサービスの信頼性をOSの機能として保証することを目指しています。
  • 信頼性を保証する方法としてモデル検査による検証や、定理証明を用いる事で、信頼性へのアプローチを行っています。

Continution based C

  • CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear という単位で遷移する。
  • goto 文による遷移は関数呼び出しとは異なり、stackや環境を隠して持つことがない。
  • 以下は CbC によって記述された codeGear です。
code pickup_lfork(PhilsPtr self, TaskPtr current_task)
{
    if (self->left_fork->owner == NULL) {
        self->left_fork->owner = self;
        self->next = pickup_rfork;
        goto scheduler(self, current_task);
    } else {
        self->next = hungry1;
        goto scheduler(self, current_task);
}

goto

  • goto 文はCbC における状態遷移に使われ、 goto の直後に遷移先を記述することで接続される。
  • goto による遷移は軽量継続と言い、関数呼び出しのような環境変数を持たず、遷移元の処理に囚われず、遷移先を自由に変更する事が可能である。これにより処理の間にメタレベルの計算を挿入する事が可能である。
  • CbC における遷移記述はそのまま状態遷移記述にすることができる。

dataGear と meta dataGear

  • CbC における入力は dataGear と呼ばれる構造体になっており、ノーマルレベル
    とメタレベルがある。
  • メタレベルには計算を行うCPUやメモリ、計算に関するノーマルレベルのdataGearを格納するcontext などがある。context は一般的なOSのプロセスに相当する。

stub CodeGear

  • メタレベルから見ると、code Gearの入力はcontext ただ1つである。
  • ノーマルレベルからMeta dataGear である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の状態を数え上げる事で、モデル検査を実装できる。
  • しかし、このcontextの状態はとても巨大になる事がある、そのためそれらを抽象化する必要性がある。

GearsOSの実装

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

モデル検査

  • モデルとは検証したいアプリケーションやサービスの振る舞いや性質を抽象化して表現したものであり、抽象化の手法には以下のようなものがある。

状態遷移モデル
論理モデル
組み合わせモデル
フローモデル ..etc

  • このモデルが仕様を満たしているかどうかを検査するのがモデル検査である。
  • 検査の要点によってモデルを使い分ける必要性がある。

状態遷移モデル

  • 今回行うモデル検査は状態遷移からプログラムの振る舞いを検証する。
  • 状態遷移モデルとは、処理前と処理後の状態をつなぎ合わせる手法である。
構成要素
状態 プログラムの状態
初期状態 何らかの処理、計算が行われる前の状態
終了状態 処理、または計算が行われた状態
処理(計算) 状態を変化させる
遷移条件 状態が分岐する際の条件

既存のモデル検査手法(SPIN)

  • 一般的に扱われるモデル検査ツールとしてSPINがある。
  • SPIN はPromela (Process Meta Language)で記述される。
  • C言語と似た文法を持ち、元は通信プロトコルの検証として開発された言語であり、検証機を生成し、コンパイルと実行を行うことで検証される。
  • チャネルを使って通信や並列動作を記述する。
  • 有限オートマトンに変換してモデル検査を行う。
  • Promelaへの書き換えが必要
  • SPIN での検査可能な性質
    アサーション
    デッドロック
    到達性
    進行性
    線形時相論理で記述された仕様

既存のモデル検査手法(Java path Finder)

  • Java Path Finder はjavaプログラムの検査ツール
  • java バーチャルマシン(JVM) を直接シュミレーション実行している、これによりjavaのバイトコードを直接実行可能である。
  • バイトコードを状態遷移モデルとして扱い、実行時に遷移し得る状態を網羅的に検査している。
  • 実行パターンを網羅的に調べるため、複数のプロセスの取り扱いができず、また状態空間が巨大な場合は、一部を抜き出して検査する必要がある。
  • JPF で検査可能な性質
    スレッドの可能な実行すべてを調べる
    デッドロックの検出
    アサーション
    Partial Order Reduction

モデル検査手法について

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

DPP(dining philosohers ploblem)

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

DPP

  • 状態は以下の構成要素からなる
    Pickup Right fork Pickup Left fork eating Put Right fork Put Left fork Thinking

GeasOS におけるDPP実装(1/3)

  • 5つのスレッドで並列処理を行う事で、哲学者の行動を再現する。
  • gearsOSには並列機構の par goto があり、これを使用するスケジューラーによって並列にスレッドを起動する。
  • par goto は引数として dataGear と実行後に継続する _exit をわたす。
  • par goto は複数スレッドでの実行であるので、各スレッドで実行後に__exitに継続する事で終了する。

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

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

GearsOS におけるDPP実装(3/3)

v- 5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表す。

  • この状態遷移は goto next によって遷移し、metaCodeGear を 挟みメタレベルで各スレッドの状態を 各スレッドごとに用意した Memory Tree に保存する。
  • Memory Tree はstateDBによってまとめられ、同じ状態は共有される。
  • またDPPにおける状態遷移は無限ループであるため、stateDBを用いて同じ状態を検索することで、終了判定を行う。

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

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