Mercurial > hg > Papers > 2021 > kono-sigos
changeset 1:5fc28fa1b01b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 27 Apr 2021 15:52:47 +0900 |
| parents | 67e6ca3c7e6c |
| children | 055c9c2a19d5 |
| files | main1.pdf model.ind |
| diffstat | 2 files changed, 127 insertions(+), 178 deletions(-) [+] |
line wrap: on
line diff
--- a/model.ind Tue Apr 27 14:25:56 2021 +0900 +++ b/model.ind Tue Apr 27 15:52:47 2021 +0900 @@ -6,50 +6,28 @@ -- OS の信頼性 - OS とは一般的にハードウェアへのアクセス、資源管理を行っているソフトウェアである。つまりコンピュータに接続されている全てのメモリやハードディスクといった記憶装置、また CPU や GPU といった計算処理装置には通常 OS の機能を利用する事でしかアクセスすることは出来なくなっている。 +OS とは一般的にハードウェアへのアクセス、資源管理を行っているソフトウェアである。つまりコンピュータに接続されている全てのメモリやハードディスクといった記憶装置、また CPU や GPU といった計算処理装置には通常 OS の機能を利用する事でしかアクセスすることは出来なくなっている。 -これはコンピュータ上で同時に複数のアプリケーションを利用することが可能なため、それぞれのアプリケーションの動作によって別々に資源要求をする場合がある事になる。この時アプリケーションから直接資源へのアクセスを許してしまうと、ハードウェアで競合が起きてしまい正常な処理が行えなくなってしまう可能性がある。 -このためハードウェアのアクセスを OS を通して行うことによって、ハードウェアでの競合が発生しないようになっている。 -複数のアプリケーションからのタスクを受け取るが、これらの実行する順番やアクセスする時間を管理することで CPU もしくは GPU の利用を複数スレッドに割当ることによって処理効率の向上を図っている。 - - またハードウェアへのアクセスや資源管理は複雑で容易ではなく、異なるハードウェアを扱う際にはそれぞれに対応したプログラミングが必要である。しかし OS がこれらのデバイスのアクセスや資源管理を行う機能を持つ事によって、アプリケーション側はハードウェアの違いを気にすることなく、プログラミングする事が出来る。 +OSはアプリケーションやサービスの信頼性を保証する基礎となる部分だが、同時に拡張性も必要となる。 +しかし、OS は非決定的な実行を持つため、その信頼性を保証するには従来のテストとデバックでは不十分と考えられている。 -このように OS はハードウェアのアクセス、資源管理を行う事によって、ハードウェア上での競合を防ぎ、アプリケーションの効率化と複雑な処理を受け持つ重要なソフトウェアである。 -そのため OS の不具合はコンピュータの全ての動作に影響するため、その信頼性はも重要なものであり、また時代とともにユーザーインターフェースや、ネットワークサービス、セキュリティといった進歩するハードウェア、サービスに対応して、OS 自体が拡張される必要がある。 -しかし、OS は非決定的な実行を持つため、その信頼性を保証するには従来のテストとデバックでは不十分と考えられる。 +テストとはソフトウェアやアプリケーションの検証は用いられる手法で、ソフトウェアあるいはアプリケーションに対して、決まったの入力を与えた場合に設計で予想された出力が返ってくる事を確かめる事によって信頼性を保証する手法である。 +このテストによる手法は、検証側が定めた範囲での入力による検証であるためテストしきれない部分が残ってしまう可能性がある。 - テストとはソフトウェアやアプリケーションの検証は用いられる手法で、ソフトウェアあるいはアプリケーションに対して、任意の入力を与えた場合に設計で予想された出力が返ってくる事を確かめる事によって信頼性を保証する手法である。 -このテストによる手法は、検証側が定めた範囲での入力による検証であるため全ての入力を抑えられてない場合があり、テストしきれない部分が残ってしまう可能性がある。 -このため、実装が必ずしも設計に沿っているとは保証しきれないという問題点がある。 - - テスト以外の信頼性を保証する検証としては形式検証があり、形式検証には定理証明とモデル検査\cite{EdmundM}の２つの手法がある。 - +テスト以外の信頼性を保証する検証としては形式検証があり、形式検証には定理証明とモデル検査\cite{EdmundM}の２つの手法がある。 定理証明は数学的な証明を用いて信頼性を保証する手法である。証明を用いるため、入力や、状態数に比較的影響をうけずに検証を行う事が出来るが、場合分けの複雑化や、場合分け自体が多くなる事がある。agda\cite{agda} といった定理証明支援器と言われるものがある。しかし証明には数学的な知識が不可欠となる - モデル検査は抽象化されたソフトウェアの実装である。プログラムの仕様である logic を満たすかどうかをモデル検査器を用いて調べる事で信頼性を保証する。 モデル検査の場合、自動で全ての状態を網羅的に出力し調べるため検証時間を工夫して短くすることが出来る。 - 本研究室で開発している Gears OS\cite{gears} は アプリケーションやソフトウェアの信頼性を OS の機能として保証することを目指しており、信頼性を保証する手法としてモデル検査やhoare logic を用いた定理証明\cite{agda-ryokka}を用いて信頼性へのアプローチを行っている。 - 本論文では、このGears OS におけるモデル検査を実現する手法について考察する。 +本研究室で開発している Gears OS\cite{gears} は アプリケーションやソフトウェアの信頼性を OS の機能として保証することを目指しており、信頼性を保証する手法としてモデル検査やhoare logic を用いた定理証明\cite{agda-ryokka}を用いて信頼性へのアプローチを行っている。 +本論文では、このGears OS におけるモデル検査を実現する手法について考察する。 --モデル検査とは モデル検査は、検証したい内容の時相論理式 p をつくり、対象のシステムの初期状態 s のモデル M があるとき、M,s が p を満たすか (M,s $\models$ p と表記される)モデル検査器を用いて調べることによって信頼性を保証する手法である。 -様相論理式にはCTL(Computational Tree Logic)やLTTL(Linear Time Temporal Logic)といったものがあり、それぞれ計算木論理、線形時相論理と言われるものである。またこの2つを合わせたCTL*というものがある。 - -今回の研究ではLTTLを用いて検証を行う。LTTLは時間を可能性や必然性として様相として持つ線形時相様相論理であるため、状態の遷移や時間の経過を基準に証明を行う場合に利用され、特にシステムのハードウェアやソフトウェアの仕様を記述する手法として用いられる。 - -モデル検査は様相演算子によって表され、状態が複雑なほど様相演算子で表す状態が増えるため論理式も複雑になってしまう。 -そのためモデルによってCTL、LTTL、CTL*の3つの論理式から適切なものを選び検証を行う事で、論理式の複雑度を抑える必要がある。 -CTLとLTTLの違いは、LTTLは枝の指定がなく、全ての枝でその状態が存在するか否かを見るので、経路ごとの表現ができない。しかしCTLは時相演算子の使い方に制約があるため、全てのLTTLをCTLで表現することはできない。 - - ---様相演算子 - -モデル検査を記述するのに使われる論理式の様相演算子は、枝を表すパス量化子と、いつ成り立つかを表す時相演算子がある。 -CTLとLTTLでは使われる様相演算子に違いはあるがCTL*ではどの様相演算子も使うことが出来る。 - +様相論理式にはCTL(Computational Tree Logic)を用いる。 +CTLの様相演算子は、枝を表すパス量化子と、いつ成り立つかを表す時相演算子がある。 パス量化子 \begin{itemize} @@ -69,48 +47,46 @@ この様相演算子を用いて表した CTL の導出木が図2.1 から 2.4のようになる。 \begin{figure}[htbp] - \begin{center} - \begin{tabular}{c} - - \begin{minipage}{0.50\hsize} +\begin{center} +\begin{tabular}{c} +\begin{minipage}{0.50\hsize} \begin{center} - \includegraphics[width=70mm]{images/graphEF.pdf} - \caption{ある枝でいつか真になる EF} - \label{fig:EF} +\includegraphics[width=70mm]{images/graphEF.pdf} +\caption{ある枝でいつか真になる EF} +\label{fig:EF} \end{center} \end{minipage} - \begin{minipage}{0.50\hsize} - \begin{center} - \includegraphics[width=70mm]{images/graphAF.pdf} +\begin{minipage}{0.50\hsize} +\begin{center} +\includegraphics[width=70mm]{images/graphAF.pdf} \caption{すべての枝でいつか真になる AF} - \label{fig:AF} +\label{fig:AF} \end{center} \end{minipage} - \end{tabular} +\end{tabular} \end{center} \end{figure} \begin{figure}[htbp] - \begin{center} - \begin{tabular}{c} - - \begin{minipage}{0.50\hsize} - \begin{center} - \includegraphics[width=70mm]{images/graphEG.pdf} - \caption{ある枝でいつも真になる EG} - \label{fig:EG} - \end{center} - \end{minipage} +\begin{center} +\begin{tabular}{c} +\begin{minipage}{0.50\hsize} +\begin{center} +\includegraphics[width=70mm]{images/graphEG.pdf} +\caption{ある枝でいつも真になる EG} +\label{fig:EG} +\end{center} +\end{minipage} - \begin{minipage}{0.50\hsize} - \begin{center} - \includegraphics[width=70mm]{images/graphAG.pdf} - \caption{すべての枝でいつも真になる AG} - \label{fig:AG} - \end{center} - \end{minipage} - \end{tabular} +\begin{minipage}{0.50\hsize} +\begin{center} +\includegraphics[width=70mm]{images/graphAG.pdf} +\caption{すべての枝でいつも真になる AG} +\label{fig:AG} +\end{center} +\end{minipage} +\end{tabular} \end{center} \end{figure} @@ -119,10 +95,8 @@ --モデル検査の実装例 -モデル検査の方法としてよく利用される物として、SPIN と java path finder(以下JVM)というツールがある。 - +モデル検査の方法としてSPIN と java path finder(以下JVM)というツールがある。 SPIN は Promela という仕様記述言語で記述する事でC言語の検証器を生成する事で、コンパイルまたは実行時に検証する事ができる。 - チャネルを使っての通信や並列動作する有限オートマトンのモデル検査が可能である。 SPINではオートマトンの並列実行処理の検証が可能であるが、これは厳密には実行するステートをランダムに選択し、実行することで実現している。 SPIN では以下の性質を検査する事ができる。 @@ -135,10 +109,11 @@ \end{itemize} Java Path Finder(JPF) は java プログラムに対するモデル検査ツールで、javaバーチャルマシン(JVM)を直接シミュレーションして実行している。そのため、javaのバイトコードを直接実行可能である。 +バイトコードを状態遷移モデルとして扱い、実行時に遷移し得る状態を網羅的に検査する。しかしバイトコードの実行パターンを網羅的に調べるために、膨大なCPU時間を必要とする。 +またJVMベースであるため、複数のプロセスの取り扱いが出来ず、状態空間が巨大になる場合は直接実行は出来ず、一部を抜き出してデバックをするのに使用される。 +JPFはJavaのreflectionの機能に依存しており、この部分はJava9 において大幅に変更されてしまったので、 +Java9以降では動作しない。 -バイトコードを状態遷移モデルとして扱い、実行時に遷移し得る状態を網羅的に検査する。しかしバイトコードの実行パターンを網羅的に調べるために、膨大なCPU時間を必要とする。 - -またJVMベースであるため、複数のプロセスの取り扱いが出来ず、状態空間が巨大になる場合は直接実行は出来ず、一部を抜き出してデバックをするのに使用される。 JPF では以下の事ができる。 \begin{itemize} \item スレッドの可能な実行全てを調べる @@ -146,26 +121,21 @@ \item アサーション \item Partial Order Reduction \end{itemize} -\chapter{Gears OS とCbC} -%信頼性を保証する一つの方法は、プログラムの可能な実行を数え上げて要求仕様を満たしているかどうかを調べるモデル検査である。 -%本論文では、Gears OS 上のアプリケーション、さらに Gears OS そのものをGears OS 上でモデル検査することに関して考察する。 --Continuation based C Gears OS は軽量継続を基本とする言語 Continuation based C (以下 CbC )\cite{CbC}を用いた OS の実装である。 - CbC は Code Gear という単位を用いて記述する C の機能を持つプログラミング言語である。コンパイルには llvmcbc\cite{llvmcbc} を用いて行う。Code Gear は一般的な処理記述にあたり関数に比べて細かく分割されている。Code Gear 間の遷移は軽量継続である goto 文によって行われる。 - 軽量継続である goto は継続前の Code Gear に戻ることはないため、プログラムの記述をそのまま状態遷移に落とし込むことが出来る。 Cの関数の型が\verb+__code+ であるような構文で定義することができる。 つまり、codeGearはdataGearを通して、次のcodeGearに goto で接続される(図\ref{fig:code-datagear})。 \begin{figure}[tb] - \begin{center} - \includegraphics[width=140mm]{fig/input-outputDataSegment.pdf} - \end{center} - \caption{codeGear と DataGear} - \label{fig:code-datagear} +\begin{center} +\includegraphics[width=140mm]{fig/input-outputDataSegment.pdf} +\end{center} +\caption{codeGear と DataGear} +\label{fig:code-datagear} \end{figure} @@ -191,11 +161,11 @@ \lstinputlisting[caption=pickuprfork, label=pickuprfork]{src/pickup_rfork.cbc} \begin{figure}[tb] - \begin{center} - \includegraphics[width=150mm]{fig/meta_gear.pdf} - \end{center} - \caption{Gears OS のメタ計算} - \label{fig:meta_Gear} +\begin{center} +\includegraphics[width=150mm]{fig/meta_gear.pdf} +\end{center} +\caption{Gears OS のメタ計算} +\label{fig:meta_Gear} \end{figure} メタレベルから見ると、codeGearの入力は context ただ一つであり、そこから必要なノーマルレベルのdataGearを取り出して、ノーマルレベルのcodeGaerを呼び出す。この取り出しは stub と呼ばれる meta codeGear によって行われる。(図\ref{fig:Context_ref}) @@ -207,27 +177,30 @@ 処理を行うことができるようになっている。ノーマルレベルとメタレベルは、必要ならばCPUのsystem mode と user mode の状態を変えても良い。 \begin{figure}[tb] - \begin{center} - \includegraphics[width=140mm]{fig/Context_ref.pdf} - \end{center} - \caption{Contexが持つDataGaerへのアクセス} - \label{fig:Context_ref} +\begin{center} +\includegraphics[width=140mm]{fig/Context_ref.pdf} +\end{center} +\caption{Contexが持つDataGaerへのアクセス} +\label{fig:Context_ref} \end{figure} \clearpage ---Gears OS における DPP の検証 +--Gears OS における平行実行の検証 -ここでcodeGearの実行はOSの中での基本単位である必要がある。つまり、codeGearは並行処理などにより割り込まれることなく、codeGearで記述された通りに実行される必要がある。しかしこれは一般的には保証されないものであるため、他のcodeGearによって共有されている dataGearに競合的に書き込んだり、割り込みにより処理が中断したりする可能性が存在する。 - -しかし、Gears OS は codeGear が正しく実行さることを保証される。つまり、Gears OS は CodeGear の処理によって競合が起きないように実装されているとする。 +codeGearの実行はOSの中での基本単位として実行される。つまり動作として +codeGearは並行処理などにより割り込まれることなく記述された通りに実行される。 +これはOSによって相対的に保証される。例えば機械故障のような場合まで保証するものとは異なる。 +他のcodeGearによって共有されている dataGearに競合的に書き込んだり、割り込みにより処理が中断したりする +しても、 Gears OS は codeGear が正しく実行さることを保証する。 プログラムの非決定的な実行は入力あるいは並列実行の非決定性から発生する。後者は並列実行される codeGear の順列並び替えとなる。よってこれらの並び替えを生成し、その時に生じる context の状態をすべて数え上げれれば\cite{tauble}モデル検査を実装できることになる。 - -ただし、context の状態は有限状態になるとは限らず、また有限になるとしても巨大になる場合が考えられる。この場合は OS やアプリケーションのテストとして動作する十分な状態にまで、 context の状態を抽象化することができればモデル検査を行えると考えられる。 +ただし、context の状態は有限状態になるとは限らず、また有限になるとしても巨大になる場合が考えられる。この場合は OS やアプリケーションのテストとして動作する十分な状態にまで、 context の状態を抽象化することができればモデル検査を行える。 +context はプロセス全体に相当するがモデル検査では変更された部分のみを考慮すれば良い。そこで、 +メモリ領域の集合から状態を作り格納するデータベースを用意する。 -メモリ領域の集合で一つの状態が定義され、この状態をさらに格納するデータベースを用意する。codeGearのシャッフルの深さ優先探索を行ない、新しく生成された状態をデータベースで参照し、既にあれば、深さを一つ戻り、別な探索枝に移ると言った動作を行うことで新しい状態が生成されてない、もしくは、バグを見つければモデル検査は終了と言うことになる。 +codeGearのシャッフルの深さ優先探索を行ない、新しく生成された状態をデータベースで参照し、既にあれば、深さを一つ戻り、別な探索枝に移る。新しい状態が生成されなくなる、もしくは、バグを見つければモデル検査は終了と言うことになる。 ここでは例題として Dining Phisopher 問題のdead lockの検出を行う。 @@ -239,36 +212,31 @@ (4) 状態を記録する memory 木と状態DBを作成する。 +(5) 状態DBがCTLの仕様を満たしているかをフラグを使って調べる。 + +(2)-(4)は Gears OS のメタ計算として実装される。 この段階でDPPのモデル検査が可能になるはずである。 +--OSそのもののモデル検査 + 一方で Gears OSそのものも codeGear で記述されている。CPU毎のC.context、そして、それが共有するKernelのK.context、それからユーザプログラムのU.context などの context からなると考えれ、これら全体は meta dataGear である K.context に含まれていると考える。 -また、U.context がDPPのように単純なものであれば OS 全体の context も複雑にはならないため、モデル検査を Gears OS 全体に対して実行可能であると考えられる。 +これらのうちのいくつかはハードウェアに関連した動作を持っているが、それをエミュレーションに置き換えることが常に可能である。Gears OSを構成している dataGear / codeGear は特殊なものではなく、普通にモデル検査の対象となる context に +登録して実行して良い。 +つまりモデル検査を Gears OS 全体に対して実行可能であると考えられる。この時、外側では普通の Gears OSが +動作し、モデル検査の対象となる context 内ではエミュレートされた dataGear / codeGear が実行される。 (5) Gears OSを含む codeGear のシャッフル実行を行ない、モデル検査を行う。 -これにより、Gears OSの自分自身によるモデル検査が可能になる。この時に、検査するcodeGearと検査されるcodeGearは同じ物であるが、 -実行する meta codeGarが異なっている。現状では、これは異なるmeta codeGearを指定してコンパイルしなおすことにより実現する。 Gears OSの実装は Unix 上のアプリケーションとしての実装と、x.v6\cite{xv6}の書き換えによる実装の二種類があるが、前者ではアプリケーションはOSに直接リンクされる。後者では x.v6 のexec機構により実行される。実際にOSのモデル検査を実行するためには、必要なmeta dataGear/meta codeGear の emulatorを書く必要がある。しかし、検査する必要がない部分は無視できるようにしたいと考えている。 Gears OSは並列実行機構を持っているので、 -(6) モデル検査を並行実行\cite{tauble2}することができる +(6) モデル検査そのものを並行実行\cite{tauble2}することができる と考えられる。 ---Gears OS におけるモデル検査 - -Gears OS 上で DPP を動かし、導出木を作成。これをLTTLに落とし込むことによってdead lock とlive lock の2つを探索することが可能である。 - -dead lock とは、スレッドが待機状態に入ったままになってしまう状態を指し、今回扱う DPP の例題だと、全てのスレッドが1つずつfork を持ってしまった場合に発生する。 - -またlive lock とは待機状態ではないが、同じ状態を繰り返してしまい処理が進まない状態をいい、今回の DPP の例題において「待機状態においてフォークを下ろす。」という処理を入れた場合で、さらに各スレッドが順番に動作するとした時、 dead lock の状態に入った場合において、各スレッドは fork を下ろす動作をするが、その後またfork を持ち上げる動作を行うので live lock 状態になる。 -このようにdead lock 状態ではないが、状態が膠着状態になるのがlive lock である。 - -LTTLで検証できる 常に p または 常に$\neg$p と、いつか p またはいつか$\neg$p であるから、dead lock を検証する事が可能である。 - --Dining Philosophers Problem の例題 モデル検査の検証用のサンプルプログラムとしてDining Philosohers Ploblem (以下DPP)を用いる。これは資源共有問題の１つで、次のような内容である。 @@ -285,11 +253,11 @@ \lstinputlisting[caption=pickuplfork, label=pickuplfork]{src/pickup_lfork.cbc} \begin{figure}[tb] - \begin{center} - \includegraphics[width=140mm]{fig/dpp_image.pdf} - \end{center} - \caption{Dining Philosohers Ploblem image} - \label{DPP_image} +\begin{center} +\includegraphics[width=140mm]{fig/dpp_image.pdf} +\end{center} +\caption{Dining Philosohers Ploblem image} +\label{DPP_image} \end{figure} @@ -328,11 +296,11 @@ \begin{figure}[tb] - \begin{center} - \includegraphics[width=140mm]{fig/model_checking.pdf} - \end{center} - \caption{DPP on Gears OS} - \label{DPP_chacking} +\begin{center} +\includegraphics[width=140mm]{fig/model_checking.pdf} +\end{center} +\caption{DPP on Gears OS} +\label{DPP_chacking} \end{figure} @@ -349,41 +317,18 @@ \item state\_db.c (状態の data base (2分木)) \end{itemize} ---Meta の入れ替え - -今回のモデル検査では全ての状態を走査する、またこれはランダムに行う必要がある。 -CbC で実装された DPP は ソースコード4.2 の Perl script meta.pm によって正規表現を用いて 遷移先の meta を機械的に置き換える事によってランダム実行を行っている。 +CbC で実装された DPP は ソースコード4.2 の Perl script meta.pm によって正規表現を用いて goto 時の +メタ計算実行を実現する。 mcMeta はモデル検査を行う場合で random は並行実行のシミュレーションを行う場合となっている。 - 7行目は多次元リストのPhilsImpls を regular expression に渡している。これはgoto の遷移先である。 - その後11行目で受け取った文字列を goto 先にランダムに、配置しており。 - 16行目では文字列を受け取った文字列に遷移する前に mcMeta を挟むようにしている。 +7行目は多次元リストのPhilsImpls を regular expression に渡している。これはgoto の遷移先である。 +その後11行目で受け取った文字列を goto 先にランダムに、配置しており。 +16行目では文字列を受け取った文字列に遷移する前に mcMeta を挟むようにしている。 + \lstinputlisting[caption=meta.pm, label=meta.pm]{src/meta.pm} ---モデル検査のフラグの管理 - - ソースコード4.3 の mcDPP.h はモデル検査で使われるフラグの宣言をしている。 - \lstinputlisting[caption=mcDPP.h, label=mcDPP.h]{src/mcDPP.h} - しかし今回の DPP の例題においては t\_eating と f\_F\_eating のフラグしか使用してしいない。 - - -DPPの例題は食事とそれ以外の状態を循環しているため t\_eating フラグの「食事中」と f\_F\_eating フラグの「いつか食事にする」という２つの状態で表すことが可能となる。また今回のモデル検査では DPP でのデッドロックの検出を行う。 - -デッドロックはプログラムの処理が止まってしまっている状態であるため、上の２つのフラグがついていない状態がデッドロックということになるため、２つのフラグによって表す事が出来る。 +--導出木の作り方 -フラグは now と next を見比べながら update する。すべての状態は 今のcontext にのっているが、過去は add\_memory\_rangeで記録されたものあるいはフラグしか見れないようになっている。 - -ソースコード4.4 のmcDPP.cbc ではフラグの比較によるモデル検査を行っている。 - \lstinputlisting[caption=mcDPP.cbc, label=mcDPP.cbc]{src/mcDPP.cbc} - - - -最初に今のフラグと次のフラグを取得し、次にphils-\>self が 1 である場合はreturn でぬける。 -12行目では 次と今のフラグがet\_ating または t\_F\_eatingであればt\_F\_eating; -15行目では直前のフラグと今のフラグ、または直前のフラグと次のフラグが違っているとchangeに1が入り、動き続け、そうでなければ18行目で今のフラグとt\_F\_eatingを比較し、あっている場合にはnot<>eating となり、終了する。 - - ---導出木の作り方 \lstinputlisting[caption=putdown\_lfork, label=putdownlfork]{src/putdown_lfork.cbc} ソースコード5.5 は DPP の例題のもので、Philospher の Leftfork を置く部分である。フォークは各 Philosher 間で共有されるデータのため、競合が起きないように CAS を行う必要がある。 このソースコードは以下のソースコード5.6に変換される。 @@ -397,6 +342,29 @@ \lstinputlisting[caption=mcMeta, label=mcMeta]{src/mcMeta.cbc} +--モデル検査のフラグの管理 + +ソースコード4.3 の mcDPP.h はモデル検査で使われるフラグの宣言をしている。 +\lstinputlisting[caption=mcDPP.h, label=mcDPP.h]{src/mcDPP.h} +しかし今回の DPP の例題においては t\_eating と f\_F\_eating のフラグしか使用してしいない。 +DPPの例題は食事とそれ以外の状態を循環しているため t\_eating フラグの「食事中」と f\_F\_eating フラグの「いつか食事にする」という２つの状態で表すことが可能となる。 + +現在 eating かどうかを調べて、t\_eating をまず設定する。導出木の生成を繰り返し行い、 +次の状態がt\_eatingまたはf\_F\_eating の時に f\_F\_eating を設定する。 +フラグが変化しなくなったら終了である。この方法だと導出木をFフラグの深さの分だけ繰り返すことになる。 + +f\_F\_eating のないノードがあれば、それはライブロックまたはデッドロックということになる。 +以下のノードで一部f\_F\_eating がないノードがあれば、それはライブロックということになる。 + +フラグは now と next を見比べながら update する。すべての状態は 今のcontext にのっているが、過去は add\_memory\_rangeで記録されたものあるいはフラグしか見れないようになっている。 + +ソースコード4.4 のmcDPP.cbc ではフラグの比較によるモデル検査を行っている。 +\lstinputlisting[caption=mcDPP.cbc, label=mcDPP.cbc]{src/mcDPP.cbc} + +最初に今のフラグと次のフラグを取得し、次にphils-\>self が 1 である場合はreturn でぬける。 +12行目では 次と今のフラグがet\_ating または t\_F\_eatingであればt\_F\_eating; +15行目では直前のフラグと今のフラグ、または直前のフラグと次のフラグが違っているとchangeに1が入り、動き続け、そうでなければ18行目で今のフラグとt\_F\_eatingを比較し、あっている場合にはnot<>eating となり、終了する。 + --実行結果 次にモデル検査を行った結果を一部抜き出して掲載する。 @@ -438,51 +406,32 @@ --評価 ---今後の展開 - - ----OS自体のモデル検査 - -Gears OS 自体も CodeGear と DataGear で書かれているので、CPU毎の C.context、共有するkernel のK.context、ユーザープログラムの U.context と考えることができ、これらはmeta dataGear であるK.context に含まれている。 - -U.context がDPPのような単純なものならば、OS全体のcontext も複雑にはならないため、DPP のモデル検査のようにシャッフル実行を行う事が出来れば、この枠組みの中で検証することが可能であると思われる。 +今回の実装はフラグの設定に繰り返し導出木を生成するアルゴリズムを用いてるのであまり +高速な実行になっていない。CTL検査ではなく、すべての場合を尽くすだけが目的であれば +繰り返し生成は必要ない。 +繰り返し実行自体は状態DBに次の状態を記録すれば避けられるがメモリ使用量は増える。 -しかし、OS のモデル検査にはいくつかの問題がある。 - -OS の場合はほとんどが meta level の記述なので、それを emulation する必要がある。メモリやCPUは問題ないが Translation Lookaside Buffer (以下TLB) を emulation する必要があるが、TLB は仮想アドレスから物理アドレスへの変換を高速化する際に使われるメモリ管理ユニットのキャッシュであり、またマイクロプロセッサによる物理空間と仮想空間の仮想記憶をサポートする際に利用しているため、emulation の仕方に工夫が必要となる。 +登録するメモリ領域、そして深さ探索する部分の指定は手動で行う必要がある。 +さらに、CTL用のフラグ管理もメタ計算として自分で書く必要がある。この部分を自動生成すること +自体は容易だと思われる。 -また CPUの状態、例えばキャッシュなども emulation する場合には、codeGear の大きさをメモリアクセスレベルまで小さくする必要がある。 -つまり、見つけたいバグを知っていれば検証は可能だが、起きる可能性のある未知のメタ計算が出てくる場合の検証方法と、その未知のメタ計算を探す手法が必要となってくる。 +現在はモデル検査の並列実行およびGears OS自体のモデル検査は行っていない。 -モデル検査は膨大な状態空間を探索する必要があり、OS 込みのモデル検査となると厳しいと予想される。 -しかし、OS 特定部分だけに絞り調べる場合には巨大なアプリケーションは必要ない思われ、普通のテストの代わりにモデル検査を使うように検証を行う事が出来ると考えられる。 +--今後の展開 この OS を含むモデル検査は OS の拡張性をデバイスドライバの開発などに向いていると考えられる。この場合は、デバイス自体の仕様が codeGear/dataGear で書かれている必要がある。 -Gears OS は Unix 上のApplicationとして実現されているものと、xv6 の書き換えとして実現するものとの二種類がある。 - -xv6 は linux を素体としたもので OS としては小さい構造となっている。そのためまずはこのxv6 に対してモデル検査を行えるようになることが OS 自体のモデル検査を行う上での次の目標となる。 - ----プログラムの展開と状態数の抽象化 - GearsOS におけるモデル検査はプログラムの実行を網羅的に行うことでプログラムの状態を展開しデッドロックを調べる。反例を探す場合はプログラムの状態を展開しつつ反例が見つかった時点で状態の生成を停止してもよいが、証明を行う場合は全ての状態を生成する必要がある。状態の生成は初期状態から非決定的に生成される全ての次の状態を生成することにより行われ、これを状態の展開という。証明はプログラムの状態の数に比例し、またプログラムが含む変数の数の指数乗の計算量がかかる。この展開の際に仕様も同時に展開することでプログラムに対する仕様の検証を行う事が可能である。 - 状態の展開は実行可能な状態の組み合わせを深さ優先探索で調べ、木構造で保存する方法である。この時、同じ状態の組み合わせがあれば共有することで状態を抽象化する事で、状態数が増えすぎる事を抑える。 ----dataGear - スレッド数がランダムで決まる、または途中でスレッドが増える例題がある場合について考える。 その例題を走査するためには、スレッド の状態を memoryTree として保管する iterator をスレッドの数だけ用意する必要がある。 しかし現在のData Gear は予め生成しておいたものであり、実行中に生成をする方法がない。 また生成される Data Gear は iterator であるためノーマルレベルからは呼び出せないようにしておく必要がある。このため Data Gear の自動生成 には工夫が必要となる。 ----Gears Debugger - モデル検査を行った際に、メモリの状態を iterator で保管している。 - このmemoryTree を実行履歴としてtrace し遡ることが出来れば、展開された状態から任意の実行状態を作る事が可能であると考えらる。さらに mcMeta に対して debugger を埋め込む事によって、状態の展開から bug の発生箇所を発見し、debug することが可能であると考えられる。 ----Red Black Tree への応用 Red Black Tree は平衡二分木の一種で複雑な構造ではあるが、探索、挿入、削除の最悪計算量O($\log${n})となるものである。この例題のモデル検査したいと考えている。 Red Black Tree をモデル検査するためにはノードを循環構造に事によって状態を有限で表す必要があり。またノードの値を iterator で整合性の検証の仕方について考察する必要がある。