Mercurial > hg > Papers > 2020 > ikkun-sigos

comparison paper/ikkun-sigos.tex @ 11:452f0f1e582c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add model checking
author ikkun <ikkun@cr.ie.u-ryukyu.ac.jp>
date Thu, 07 May 2020 16:28:01 +0900
parents 7cbb0c656be3
children 2c17d3dc56f0
comparison
equal deleted inserted replaced
10:7cbb0c656be3 11:452f0f1e582c
90 \newpage　 90 \newpage　
91 \section{Continuation based C} 91 \section{Continuation based C}
92 　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 となる。 92 　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 となる。
93 \begin{figure}[tb] 93 \begin{figure}[tb]
94 \begin{center} 94 \begin{center}
95 \includegraphics[width=70mm]{./pic/input-outputDataSegment.pdf} 95 \includegraphics[width=80mm]{./pic/input-outputDataSegment.pdf}
96 \end{center} 96 \end{center}
97 \caption{CodeSegment と DataSegment} 97 \caption{CodeSegment と DataSegment}
98 \label{code-datasegment} 98 \label{code-datasegment}
99 \end{figure} 99 \end{figure}
100 100
101 CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずプログラムの検証を行なう。\\ 101 CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずプログラムの検証を行なう。\\
102 　CbC における接続は goto を用いて行われる。got は関数呼び出しのような環境変数を持たず goto の直後に遷移先を記述することで、遷移先に接続される。これを軽量継続と言い、遷移元の処理に囚われず、遷移先を自由に変更する事が可能でり 遷移元の code gear の goto 先以外に変更する事なく、goto 先を変更するだけで遷移元の code gear の変 102 　CbC における接続は goto を用いて行われる。got は関数呼び出しのような環境変数を持たず goto の直後に遷移先を記述することで、遷移先に接続される。これを軽量継続と言い、遷移元の処理に囚われず、遷移先を自由に変更する事が可能でり 遷移元の code gear の goto 先以外に変更する事なく、処理の間にメタレベルの計算を挿入する事が可能である。CbC における遷移記述はそのまま状態遷移記述にすることができる。\ref{fig:meta_Gear}\\
103 処理の間にメタレベルの計算を挿入する事が可能である。CbC における遷移記述はそのまま状態遷移記述にすることができる。\\
104 103
105 \begin{figure}[tb] 104 \begin{figure}[tb]
106 \begin{center} 105 \begin{center}
107 \includegraphics[width=70mm]{./pic/meta_gear.pdf} 106 \includegraphics[width=90mm]{./pic/meta_gear.pdf}
108 \end{center} 107 \end{center}
109 \caption{Gears OS のメタ計算} 108 \caption{Gears OS のメタ計算}
110 \label{meta_Gear} 109 \label{meta_Gear}
111 \end{figure} 110 \end{figure}
112 111
113 　GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。マルチコアCPU環境では CodeGaer と CodeSegment は同一だが、、GPU環境では CodeGear にはOpenCL/CUDA における kernel も含まれる。kernelとはGPUで実行される関数のことである。\\ 112 　GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。マルチコアCPU環境では CodeGaer と CodeSegment は同一だが、、GPU環境では CodeGear にはOpenCL/CUDA における kernel も含まれる。kernelとはGPUで実行される関数のことである。\\
114 113
115 114
116 \section{DPP} 115 \section{DPP}
117 　検証用のサンプルプログラムとしてDining Philosohers Ploblem を用いる。これは資源共有問題の１つで、次のような内容である。\\ 116 　検証用のサンプルプログラムとしてDining Philosohers Ploblem (以下DPP)を用いる。これは資源共有問題の１つで、次のような内容である。\\
118 　5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{fig}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが開くのを待つ。\\ 117 　5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{fig}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが置かれるのを待つ。\\
119 　各哲学者を１つのプロセスとすると、この問題では5個のプロセスが並列に動くことになり、全員が1本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。\\ 118 　各哲学者を１つのプロセスとすると、この問題では5個のプロセスが並列に動くことになり、全員が1本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。\\
120 \begin{figure}[tb] 119 \begin{figure}[tb]
121 \begin{center} 120 \begin{center}
122 \includegraphics[width=70mm]{./pic/dpp_image.pdf} 121 \includegraphics[width=70mm]{./pic/dpp_image.pdf}
123 \end{center} 122 \end{center}
124 \caption{Dining Philosohers Ploblem} 123 \caption{Dining Philosohers Ploblem}
125 \label{DPP_imag} 124 \label{DPP_imag}
126 \end{figure} 125 \end{figure}
127
128
129 126
127 \section{タブロー展開と状態数の抽象化}
128 　GearsOS におけるモデル検査はタブロー展開を用いることでデッドロックを調べる。タブロー法は生成可能な状態の全てを生成する手法である。反例を探す場合は反例が見つかった時点で状態の生成を停止してもよいが、証明を行う場合は全ての状態を生成する必要がある。状態の生成は初期状態から非決定的に生成される全ての次の状態を生成することにより行われ、これを状態の展開という。証明はプログラムの状態の数に比例し、またプログラムが含む変数の数の指数状の計算量がかかる。この展開の際に仕様うも同時に展開することでプログラムに対する仕様の検証を行う事が可能である。\\
129 　タブロー法は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。
130 130
131 \section{GearsOSを用いたモデル検査} 131 \section{GearsOSを用いたモデル検査}
132 サンプル問題であるDining Phirosoher ploblem は5つのスレッドが同時に処理を行う問題である。そこで Gears OS の並列構文の par goto が用いることでマルチスレッド処理の実装を行う。 par goto は引数として、data gaer と実行後に継続する\|__exit|を渡す。par goto で生成された Task は\|__exit| に継続する事で終了する。これによりGears OS は複数スレッドでの実行を行う事が可能であり、また Gears OS には　Synchronized Queue というマルチスレッドでのデータの一貫性を保証する事ができる Queue がある。 132 　DPP は哲学者5人が同時に行動するので、5つのスレッドで同時に処理することで状態を生成する事ができる。まず Gears OS の並列構文の par goto が用いることでマルチスレッド処理の実装を行う。 par goto は引数として、data gaer と実行後に継続する\|__exit|を渡す。par goto で生成された Task は\|__exit| に継続する事で終了する。これによりGears OS は複数スレッドでの実行を行う事が可能である。
133 Syncrhonized Queueは CAS(Check and Set,Compare and Swap)を用いて実装されている。\\ 133 　また Gears OS には　Synchronized Queue というマルチスレッドでのデータの一貫性を保証する事ができる Queue があり、これを使い5つのフォークの状態を管理する。
134 CAS は値の比較、更新をアトミックに行う命令である。CASを使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じデータ今日がないため、データの更新に成功する。異なる場合は他の書き込みがあったとみなされ、値の更新に失敗する。 134 　Syncrhonized Queueは CAS(Check and Set)を用いて実装されており、値の比較、更新をアトミックに行う命令である。CASを使う際は更新前の値と更新後の値を渡し、渡された更新前の値を実際に保存されているメモリ番地の値と比較し、同じデータ今日がないため、データの更新に成功する。異なる場合は他の書き込みがあったとみなされ、値の更新に失敗し、もう一度 CAS を行う。
135 　5スレッドで行われる処理の状態は以下の6通りで、think のあとPickup Right fork に戻ってくる。
136 \begin{itemize}
137 \item Pickup Right fork
138 \item Pickup Left fork
139 \item eating
140 \item Put Right fork
141 \item Put Left fork
142 \item Thinking
143 \end{itemize}
144 この状態は goto next によって遷移する。またタブロー法を用いてデッドロックを左g酢ため、にこの状態遷移を Memory Tree として保管する。
135 145
136 \section{GearsOSによるタブロー展開。} 146 　
137 　GearsOS におけるモデル検査はタブロー法という手法が用いる。タブロー法は様相論理式の恒真性を検証する定理証明アルゴリズムで、プログラムの大域的な状態の全てを生成する手法である。反例を探す場合は反例が見つかった時点で状態の生成を停止してもよいが、証明を行う場合は全ての大域的な状態を生成する必要がある。大域的な状態の生成は初期状態から非決定的に生成される全ての次の状態を生成することにより行われ、これを状態の展開という。証明はプログラムの状態の数に比例し、またプログラムが含む変数の数の指数状の計算量がかかる。この展開の際に仕様うも同時に展開することでプログラムに対する仕様の検証を行う事が可能である。\\
138 　タブロー法は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。タブロー法に沿って状態を展開する事をタブロー展開といい
139
140 \section{モデル検査における状態数爆発について}
141 147
142 148
143 149
150 \begin{figure}[tb]
151 \begin{center}
152 \includegraphics[width=70mm]{./pic/model_checking.pdf}
153 \end{center}
154 \caption{DPP chacking}
155 \label{DPP_chacking}
156 \end{figure}
144 157
145 158
146 159
147 160
148 \nocite{*} 161 \nocite{*}