# HG changeset patch # User ikkun # Date 1588836481 -32400 # Node ID 452f0f1e582c12575d4482c76280583ee90f7f5e # Parent 7cbb0c656be3eda7b9b8950639e65c90c3cb8b76 add model checking diff -r 7cbb0c656be3 -r 452f0f1e582c paper/ikkun-sigos.pdf Binary file paper/ikkun-sigos.pdf has changed diff -r 7cbb0c656be3 -r 452f0f1e582c paper/ikkun-sigos.tex --- a/paper/ikkun-sigos.tex Wed May 06 17:03:24 2020 +0900 +++ b/paper/ikkun-sigos.tex Thu May 07 16:28:01 2020 +0900 @@ -92,19 +92,18 @@ 　GearsOS は Continuation based C (以下CbC) という言語を用いて拡張性と信頼性を両立させることを目的として本研究室で開発されている。CbC はC言語と似た構文を持つ言語であるが、CodeSegment と DataSegment を用いるプログラミングスタイルを提案している。CodeSegmentは処理の単位である。CodeSegument は値を入力として受け取り処理を行ったあと出力を行う、また他の CodeSegment を接続していくことによりプログラムを構築していく。DataSegment は CodeSegment が扱うデータの単位であり、処理に必要なデータが全て入っている。DataSegmen は Input DataSegment と呼ばれ、出力はOutput DataSegment と呼ばれる。CodeSegment A と CodeSegment B を接続したとき、A の Output DataSegment は B の入力 Input DataSegment となる。 \begin{figure}[tb] \begin{center} - \includegraphics[width=70mm]{./pic/input-outputDataSegment.pdf} + \includegraphics[width=80mm]{./pic/input-outputDataSegment.pdf} \end{center} \caption{CodeSegment と DataSegment} \label{code-datasegment} \end{figure} CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずプログラムの検証を行なう。\\ -　CbC における接続は goto を用いて行われる。got は関数呼び出しのような環境変数を持たず goto の直後に遷移先を記述することで、遷移先に接続される。これを軽量継続と言い、遷移元の処理に囚われず、遷移先を自由に変更する事が可能でり 遷移元の code gear の goto 先以外に変更する事なく、goto 先を変更するだけで遷移元の code gear の変 -処理の間にメタレベルの計算を挿入する事が可能である。CbC における遷移記述はそのまま状態遷移記述にすることができる。\\ +　CbC における接続は goto を用いて行われる。got は関数呼び出しのような環境変数を持たず goto の直後に遷移先を記述することで、遷移先に接続される。これを軽量継続と言い、遷移元の処理に囚われず、遷移先を自由に変更する事が可能でり 遷移元の code gear の goto 先以外に変更する事なく、処理の間にメタレベルの計算を挿入する事が可能である。CbC における遷移記述はそのまま状態遷移記述にすることができる。\ref{fig:meta_Gear}\\ \begin{figure}[tb] \begin{center} - \includegraphics[width=70mm]{./pic/meta_gear.pdf} + \includegraphics[width=90mm]{./pic/meta_gear.pdf} \end{center} \caption{Gears OS のメタ計算} \label{meta_Gear} @@ -114,8 +113,8 @@ \section{DPP} -　検証用のサンプルプログラムとしてDining Philosohers Ploblem を用いる。これは資源共有問題の１つで、次のような内容である。\\ -　5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{fig}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが開くのを待つ。\\ +　検証用のサンプルプログラムとしてDining Philosohers Ploblem (以下DPP)を用いる。これは資源共有問題の１つで、次のような内容である。\\ +　5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{fig}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが置かれるのを待つ。\\ 　各哲学者を１つのプロセスとすると、この問題では5個のプロセスが並列に動くことになり、全員が1本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。\\ \begin{figure}[tb] \begin{center} @@ -124,23 +123,37 @@ \caption{Dining Philosohers Ploblem} \label{DPP_imag} \end{figure} - - + \section{タブロー展開と状態数の抽象化} + 　GearsOS におけるモデル検査はタブロー展開を用いることでデッドロックを調べる。タブロー法は生成可能な状態の全てを生成する手法である。反例を探す場合は反例が見つかった時点で状態の生成を停止してもよいが、証明を行う場合は全ての状態を生成する必要がある。状態の生成は初期状態から非決定的に生成される全ての次の状態を生成することにより行われ、これを状態の展開という。証明はプログラムの状態の数に比例し、またプログラムが含む変数の数の指数状の計算量がかかる。この展開の際に仕様うも同時に展開することでプログラムに対する仕様の検証を行う事が可能である。\\ +　タブロー法は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。 \section{GearsOSを用いたモデル検査} - サンプル問題であるDining Phirosoher ploblem は5つのスレッドが同時に処理を行う問題である。そこで Gears OS の並列構文の par goto が用いることでマルチスレッド処理の実装を行う。 par goto は引数として、data gaer と実行後に継続する\|__exit|を渡す。par goto で生成された Task は\|__exit| に継続する事で終了する。これによりGears OS は複数スレッドでの実行を行う事が可能であり、また Gears OS には　Synchronized Queue というマルチスレッドでのデータの一貫性を保証する事ができる Queue がある。 - Syncrhonized Queueは CAS(Check and Set,Compare and Swap)を用いて実装されている。\\ - CAS は値の比較、更新をアトミックに行う命令である。CASを使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じデータ今日がないため、データの更新に成功する。異なる場合は他の書き込みがあったとみなされ、値の更新に失敗する。 +　DPP は哲学者5人が同時に行動するので、5つのスレッドで同時に処理することで状態を生成する事ができる。まず Gears OS の並列構文の par goto が用いることでマルチスレッド処理の実装を行う。 par goto は引数として、data gaer と実行後に継続する\|__exit|を渡す。par goto で生成された Task は\|__exit| に継続する事で終了する。これによりGears OS は複数スレッドでの実行を行う事が可能である。 +　また Gears OS には　Synchronized Queue というマルチスレッドでのデータの一貫性を保証する事ができる Queue があり、これを使い5つのフォークの状態を管理する。 +　Syncrhonized Queueは CAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う命令である。CASを使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じデータ今日がないため、データの更新に成功する。異なる場合は他の書き込みがあったとみなされ、値の更新に失敗し、もう一度 CAS を行う。 +　5スレッドで行われる処理の状態は以下の6通りで、think のあとPickup Right fork に戻ってくる。 +\begin{itemize} +\item Pickup Right fork +\item Pickup Left fork +\item eating +\item Put Right fork +\item Put Left fork +\item Thinking +\end{itemize} +この状態は goto next によって遷移する。またタブロー法を用いてデッドロックを左g酢ため、にこの状態遷移を Memory Tree として保管する。 - \section{GearsOSによるタブロー展開。} - 　GearsOS におけるモデル検査はタブロー法という手法が用いる。タブロー法は様相論理式の恒真性を検証する定理証明アルゴリズムで、プログラムの大域的な状態の全てを生成する手法である。反例を探す場合は反例が見つかった時点で状態の生成を停止してもよいが、証明を行う場合は全ての大域的な状態を生成する必要がある。大域的な状態の生成は初期状態から非決定的に生成される全ての次の状態を生成することにより行われ、これを状態の展開という。証明はプログラムの状態の数に比例し、またプログラムが含む変数の数の指数状の計算量がかかる。この展開の際に仕様うも同時に展開することでプログラムに対する仕様の検証を行う事が可能である。\\ -　タブロー法は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。タブロー法に沿って状態を展開する事をタブロー展開といい - - \section{モデル検査における状態数爆発について} +　 +\begin{figure}[tb] + \begin{center} + \includegraphics[width=70mm]{./pic/model_checking.pdf} + \end{center} + \caption{DPP chacking} + \label{DPP_chacking} +\end{figure}