# HG changeset patch # User Shinji KONO # Date 1612160495 -32400 # Node ID 003a8f96e16ec4100963242c69c5e94162b00133 # Parent 8f9caa063e541373e6015d2668fb49d156c8e9d5# Parent 1048f5e71d915d0ee0082cfc1055dd0ee0808a4c merge diff -r 8f9caa063e54 -r 003a8f96e16e .DS_Store Binary file .DS_Store has changed diff -r 8f9caa063e54 -r 003a8f96e16e paper/GearsOS-modelchecking.pdf Binary file paper/GearsOS-modelchecking.pdf has changed diff -r 8f9caa063e54 -r 003a8f96e16e paper/ikkun-sigos.pdf Binary file paper/ikkun-sigos.pdf has changed diff -r 8f9caa063e54 -r 003a8f96e16e paper/ikkun-sigos.tex --- a/paper/ikkun-sigos.tex Thu May 07 22:42:40 2020 +0900 +++ b/paper/ikkun-sigos.tex Mon Feb 01 15:21:35 2021 +0900 @@ -14,6 +14,28 @@ \usepackage[dvips,dvipdfmx]{graphicx} \usepackage{latexsym} \usepackage{listings} +\lstset{ + language=C, + tabsize=2, + frame=single, + basicstyle={\tt\footnotesize}, % + identifierstyle={\footnotesize}, % + commentstyle={\footnotesize\itshape}, % + keywordstyle={\footnotesize\ttfamily}, % + ndkeywordstyle={\footnotesize\ttfamily}, % + stringstyle={\footnotesize\ttfamily}, + breaklines=true, + captionpos=b, + columns=[l]{fullflexible}, % + xrightmargin=0zw, % + xleftmargin=1zw, % + aboveskip=1zw, + numberstyle={\scriptsize}, % + stepnumber=1, + numbersep=0.5zw, % + lineskip=-0.5ex, +} + \usepackage{caption} \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline} \def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\} \def\|{\verb|} @@ -22,7 +44,7 @@ %\setcounter{巻数}{59}%vol59=2018 %\setcounter{号数}{10} %\setcounter{page}{1} - +\renewcommand{\lstlistingname}{Code} \begin{document} @@ -105,8 +127,14 @@ メタレベルから見ると、codeGearの入力は context ただ一つであり、そこから必要なノーマルレベルのdataGearを取り出して、ノーマルレベルのcodeGaerを 呼び出す。この取り出しは stub と呼ばれる meta codeGear によって行われる。 +<<<<<<< working copy これは通常の関数呼び出しのABI(引数とレジスタやスタック上の関係を決めたバイナリインターフェース)に相当する。 +======= +Codeは codeGear では codeGear における goto の遷移と引数を渡す例題である。 +Codeは stub codeGear は codeGear の接続の間に挟まれる Meta Code Gear である。ノーマルレベルのcodeGear から MetadataGear である Context を直接参照してしまうと、ユーザーがメタ計算をノーマルレベルで自由に記述できてしまい、メタ計算を分離した意味がなくなってしまう。stub Code Gear はこの問題を防ぐため、Context から必要なdataGaerのみをノーマルレベルに和刺す処理を行なっている。 +>>>>>>> merge rev +<<<<<<< working copy 遷移は次のcodeGearに移動するだけだが、その前に出力するdataGearをcontextに書き出す必要がある。 これは通常の関数呼び出しのreturnの処理に相当する。 以下はメタレベルから見た codeGear である。 @@ -137,12 +165,8 @@ \end{verbatim} } -ここでcodeGearの実行はOSの中での基本単位である必要がある。つまり、codeGearは並行処理などにより割り込まれることなく、codeGearで記述された -通りに実行される必要がある。これは一般的には保証されない。他のcodeGearが共有された dataGearに競合的に書き込んだり、割り込みにより処理が -中断したりする。しかし、Gears OS が codeGear が正しく実行さることを保証する。つまり、Gears OS はそのように実装されているとする。 - -プログラムの非決定的な実行は入力あるいは並列実行の非決定性から生じる。後者は並列実行される codeGear の順列並び替えになる。従って、 -これらの並び替えを生成し、その時に生じる context の状態をすべて数え上げれればモデル検査を実装できることになる。 +ここでcodeGearの実行はOSの中での基本単位である必要がある。つまり、codeGearは並行処理などにより割り込まれることなく、codeGearで記述された通りに実行される必要がある。これは一般的には保証されない。他のcodeGearが共有された dataGearに競合的に書き込んだり、割り込みにより処理が中断したりする。しかし、Gears OS が codeGear が正しく実行さることを保証する。つまり、Gears OS はそのように実装されているとする。 +プログラムの非決定的な実行は入力あるいは並列実行の非決定性から生じる。後者は並列実行される codeGear の順列並び替えになる。従って、これらの並び替えを生成し、その時に生じる context の状態をすべて数え上げれればモデル検査を実装できることになる。 ただし、context の状態は有限状態になるとは限らないし、有限になるとしても巨大になることがある。しかし、OSやアプリケーションのテストだと 考えると、それらの動作の振る舞いを調べるのに十分な状態があれば良い。一つの方法は context の状態をなんらかの方法で抽象化することである。 @@ -229,10 +253,31 @@ GearsOS では codeGear と DataGear はそれぞれ codeGear と DataGear と呼ばれている。マルチコアCPU環境では codeGaer と codeGear は同一だが、、GPU環境では codeGear にはOpenCL/CUDA における kernel も含まれる。kernelとはGPUで実行される関数のことである。 \section{DPP} -検証用のサンプルプログラムとしてDining Philosohers Ploblem (以下DPP)を用いる。これは資源共有問題の１つで、次のような内容である。 -5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{DPP_imag}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが置かれるのを待つ。 -各哲学者を1つのプロセスとすると、この問題では5個のプロセスが並列に動くことになり、全員が1本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。 + +検証用のサンプルプログラムとしてDining Philosohers Ploblem (以下DPP)を用いる。これは資源共有問題の１つで、次のような内容である。\ref{varargnext3} + +5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{fig}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが置かれるのを待つ。 + +各哲学者を１つのプロセスとすると、この問題では5個のプロセスが並列に動くことになり、全員が1本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。 + +以下はDPPにおける左側のフォークを取るプログラムである。 +最初に左のフォークを持たれているかどうかを確認し、いなければ自分を持ち主に登録する。 +その後 next に次に遷移する自分の状態を入れ scheduler に遷移することによって scheduler を通して次の状態に遷移する。このときscheduler からメタ計算を挟むことによって状態をMemoryTree に入れる事ができる。 +左のフォークの持ち主がいた場合は飢餓状態を登録し scheduler に遷移する事で待機状態を維持する。 +\begin{lstlisting}[label=varargnext3,frame=lrbt,label=src:cbc_example,caption={DPP}] + 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); +} +\end{lstlisting} \begin{figure}[tb] \begin{center} @@ -262,9 +307,9 @@ \item Put Left fork \item Thinking \end{itemize} -この状態は goto next によって遷移する。この時に次に動作するのは5人のうちのどれでも良い。 -この状態遷移を深さ優先探索すると無限ループするが、同じ状態かどうかを Memort Tree と State DB により判定する。 -同じ状態であれば、深さ優先探索の一つ前の iterator に戻る。 + +この状態は goto next によって遷移する。状態を遷移する際、MemoryTreeによって状態を保存する。またこの状態遷移は無限ループするのでMemoryTree に保管される。またこのMemoryTreeはスレッドの数だけあり、sutats DB によってまとめられている。 +DPPの状態遷移は6つの状態を繰り返すため、同じ状態が出た場合には終了させなければならない。そこでstate DBを用いて同じ状態を検索することで終了判定をだす。 \begin{figure}[tb] \begin{center} @@ -314,9 +359,7 @@ \nocite{*} \bibliographystyle{ipsjunsrt} -\bibliography{ikkun-bib} - - +\bibliography{ikkun.bib} \end{document} diff -r 8f9caa063e54 -r 003a8f96e16e paper/ikkun.bib --- a/paper/ikkun.bib Thu May 07 22:42:40 2020 +0900 +++ b/paper/ikkun.bib Mon Feb 01 15:21:35 2021 +0900 @@ -1,117 +1,46 @@ -@inbook{inbook1, - author = "Knuth, D. E.", - title = "Fundamental Algorithms", - series = "Art of Computer Programming", - volume = 1, - chapter = 2, - pages = "371--381", - publisher = "Addison-Wesley", - address = "Reading, Massachusetts", - edition = "2nd", - year = 1973} - -@incollection{incollection1, - author = "Schwartz, Aaaa Jjjj", - title = "Subdividing B{\'e}zier Curves and Surfaces", - booktitle = "Geometric Modeling: Algorithms and New Trends", - editor = "Farin, G. E.", - publisher = "SIAM", - address = "Philadelphia", - pages = "55--66", - year = 1987} - -@inproceedings{inproceedings1, - author = "Baraff, D", - title = "Curved Surfaces and Coherence for Non-penetrating - Rigid Body Simulation", - booktitle = "SIGGRAPH '90 Proceedings", - pages = "19--28", - editor = "Beach, R. J.", - address = "Dallas, Texas", - organization = "ACM", - publisher = "Addison-Wesley", - year = 1990} - -@inproceedings{inproceedings2, - author = "Hiroshi Nakashima and others", - title = "OhHelp: A Scalable Domain-Decomposing Dynamic - Load Balancing for Particle-in-Cell Simulations", - booktitle = "Proc.\ Intl.\ Conf. Supercomputing", - year = 2009, - pages = "90-99", - doi = "http://doi.acm.org/10.1145/1542275.1542293"} - -@manual{manual1, - organization = "Adobe Systems Inc.", - title = "PostScript Language Reference Manual", - publisher = "Addison-Wesley", - address = "Reading, Massachusetts", - year = 1985} - -@mastersthesis{mastersthesis1, - author = "山下 義行", - yomi = "Yamashita, Y", - title = "文脈自由文法への否定の導入", - school = "筑波大学大学院工学研究科", - year = 1989} - +@article{ + pargoto, + author = "河野 真治 and 伊波 立樹 and 東恩納 琢偉", + title = {Code Gear、Data Gear に基づく OS のプロトタイプ}, + journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)}, + month = "May", + year = 2016 +} -@phdthesis{phdthesis1, - author = "Weihl, W.", - title = "Specification and Implementation of - Atomic Data Types", - school = "MIT", - address = "Boston", - year = 1984} - -@proceedings{proceedings1, - title = "Proc. Intl. Conf. on Fifth Generation Computer - Systems", - organization = "Institute for New Generation Computer Technology", - volume = 1, - year = 1992} - -@techreport{techreport1, - author = "Ihsakat Aredon", - title = "{\TeX} 独稽古", - type = "Seminar on Mathematical Sciences", - number = 13, - institution = "Department of Mathematics, Keio University", - address = "Yokohama", - year = 1989} - - -@webpage{webpage1, - author = "情報処理学会", - title = "コンピュータ博物館設立の提言", - organization = "情報処理学会", - url = "http://www.ipsj.or.jp/03somu/teigen/museum200702.html", - refdate = "2007-02-05"} - -@webpage{webpage2, - author = "情報処理学会論文誌編集委員会", - title = "「情報処理学会論文誌（IPSJ Journal）」原稿執筆案内", - organization = "情報処理学会", - url="http://www.ipsj.or.jp/08editt/journal/shippitsu/ronbunJ-prms.pdf", - refdate = "2010-10-28"} - -@webpage{webpage3, - author = "Alan Kay", - title = "Welcome to Squeakland", - organization = "Squeakland", - url = "http://www.squeakland.org/community/biography/alanbio.html", - refdate = "2007-04-05"} - -@webpage{webpage4, - author = "Hiroshi Nakashima", - title = "A {WEB} Page", - organization = "Kyoto University", - url = "http://www.para.media.kyoto-u.ac.jp/~nakashima/a.web.page.of.long.url/", - refdate = "2010-10-30"} - -@webpage{webpage5, - author = "Hiroshi Nakashima", - title = "Another {WEB} Page", - organization = "Kyoto University", - url = "http://www.para.media.kyoto-u.ac.jp/~nakashima/a.web.page.of.much.longer.url/", - refdate = "2010-10-30"} +@article{ + gearsOS2, + author = "宮城　光希 and 桃原　優 and 河野真治", + title = {Code Gear と Data Gear を持つ Gears OS の設計}, + journal = {第59回プログラミング・シンポジウム}, + month = "Jan", + year = 2018 + } +@article{ + GearsOS, + author = "小久保翔平 and 伊波立樹 and 河野真治", + title = {Monad に基づくメタ計算を基本とする Gears OS の設計}, + journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)}, + month = "May", + year = 2015 + } +@article{ + tauble, + author = "下地篤樹 and 河野真治", + title = {タブロー法を用いたContinuation based C プログラムの検証}, + journal = {日本ソフトウェア科学会第23回大会}, + year = 2006 + } +@article{ + CbC, + author = "河野真治", + title = {継続を持つCの下位言語によるシステム記述}, + journal = {日本ソフトウェア科学会第17回大会}, + year = 2000 + } +@article{ + tauble2, + author = "比嘉 薫 and 河野真治", + title = {タブロー法の負荷分散について}, + journal = {日本ソフトウェア科学会第18回論文集}, + year = 2001 + } \ No newline at end of file diff -r 8f9caa063e54 -r 003a8f96e16e paper/pic/model_checking.odg Binary file paper/pic/model_checking.odg has changed diff -r 8f9caa063e54 -r 003a8f96e16e paper/pic/model_checking.pdf Binary file paper/pic/model_checking.pdf has changed diff -r 8f9caa063e54 -r 003a8f96e16e paper/src/codegear-goto --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/codegear-goto Mon Feb 01 15:21:35 2021 +0900 @@ -0,0 +1,7 @@ + __code cg0(int a, int b) { + goto cg1(a+b); + } + + __code cg1(int c) { + goto cg2(c); + } \ No newline at end of file diff -r 8f9caa063e54 -r 003a8f96e16e paper/src/pickupL.cbc --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/src/pickupL.cbc Mon Feb 01 15:21:35 2021 +0900 @@ -0,0 +1,10 @@ +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); +} \ No newline at end of file diff -r 8f9caa063e54 -r 003a8f96e16e presen/pic/dpp_image.bb --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presen/pic/dpp_image.bb Mon Feb 01 15:21:35 2021 +0900 @@ -0,0 +1,5 @@ +%%Title: ./dpp_image.pdf +%%Creator: ebb Version 0.5.2 +%%BoundingBox: 0 0 626 475 +%%CreationDate: Tue Feb 12 04:12:11 2008 + diff -r 8f9caa063e54 -r 003a8f96e16e presen/pic/dpp_image.pdf Binary file presen/pic/dpp_image.pdf has changed diff -r 8f9caa063e54 -r 003a8f96e16e presen/pic/input-outputDataSegment.pdf Binary file presen/pic/input-outputDataSegment.pdf has changed diff -r 8f9caa063e54 -r 003a8f96e16e presen/pic/meta_gear.pdf Binary file presen/pic/meta_gear.pdf has changed diff -r 8f9caa063e54 -r 003a8f96e16e presen/pic/model_checking.odg Binary file presen/pic/model_checking.odg has changed diff -r 8f9caa063e54 -r 003a8f96e16e presen/pic/model_checking.pdf Binary file presen/pic/model_checking.pdf has changed diff -r 8f9caa063e54 -r 003a8f96e16e presen/sigos.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presen/sigos.html Mon Feb 01 15:21:35 2021 +0900 @@ -0,0 +1,278 @@ +Gears OSでモデル検査を実現する手法について
+

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

+
    +
  • 状態の構成要素は次の6つからなる。
    +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)

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

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 を作成する。
    • +
+
+
+

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 を指定してコンパイルすることで実現できる。
    • +
+
+
\ No newline at end of file diff -r 8f9caa063e54 -r 003a8f96e16e presen/sigos.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presen/sigos.md Mon Feb 01 15:21:35 2021 +0900 @@ -0,0 +1,239 @@ +--- +marp: true +title: Gears OSでモデル検査を実現する手法について +paginate: true +--- + +# 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 + +- 状態の構成要素は次の6つからなる。 +`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) + +- マルチスレッドでのデータの一貫性を保証する手法としてCheck and Set (CAS) がある。 +- CAS を用いて値の比較、更新をアトミックに行う。 +- CAS は書き込みの際に、書き込む MetaCodeGear に更新前と更新後の値を渡し、更新前の値が保存されているメモリ番地の値と比較し同じデータがであれば書き込みを行う。異なる場合はほかからの書き込みがあったとみなし、値の更新に失敗し、もう一度CASを行う。 +- DPPの例題ではフォークがスレッドで共有されるデータにあたるので、CAS を用いることによってスレッド間での同期を行う。 + +--- + +# 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 を作成する。 + +--- + +# 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 を指定してコンパイルすることで実現できる。 + + + + +