Mercurial > hg > Papers > 2020 > ikkun-sigos
changeset 32:003a8f96e16e default tip
merge
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Feb 2021 15:21:35 +0900 |
| parents | 8f9caa063e54 (current diff) 1048f5e71d91 (diff) |
| children | |
| files | paper/ikkun-sigos.pdf paper/ikkun-sigos.tex |
| diffstat | 17 files changed, 643 insertions(+), 132 deletions(-) [+] |
line wrap: on
line diff
--- 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}
--- 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
--- /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
--- /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
--- /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 +
--- /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 @@ +<!DOCTYPE html><html lang="ja-JP"><head><title>Gears OSでモデル検査を実現する手法について</title><meta property="og:title" content="Gears OSでモデル検査を実現する手法について"><meta charset="UTF-8"><meta name="viewport" content="width=device-width,height=device-height,initial-scale=1.0"><meta name="apple-mobile-web-app-capable" content="yes"><meta http-equiv="X-UA-Compatible" content="ie=edge"><meta property="og:type" content="website"><meta name="twitter:card" content="summary"><style>.bespoke-marp-note,.bespoke-marp-osc,.bespoke-progress-parent{display:none;transition:none}@media screen{body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button{-webkit-appearance:none;-moz-appearance:none;appearance:none;background-color:transparent;border:0;color:inherit;cursor:pointer;font-size:inherit;opacity:.8;outline:none;padding:0;transition:opacity .2s linear;-webkit-tap-highlight-color:transparent}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:disabled,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:disabled,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:disabled{cursor:not-allowed;opacity:.15!important}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover{opacity:1}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:active,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:active,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover:active{opacity:.6}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:not(:disabled),body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button:hover:not(:disabled),body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button:hover:not(:disabled){transition:none}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button.bespoke-marp-presenter-info-page-prev{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48cGF0aCBmaWxsPSJub25lIiBzdHJva2U9IiNmZmYiIHN0cm9rZS1saW5lY2FwPSJyb3VuZCIgc3Ryb2tlLWxpbmVqb2luPSJyb3VuZCIgc3Ryb2tlLXdpZHRoPSI1IiBkPSJNNjggOTBMMjggNTBsNDAtNDAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button.bespoke-marp-presenter-info-page-next{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48cGF0aCBmaWxsPSJub25lIiBzdHJva2U9IiNmZmYiIHN0cm9rZS1saW5lY2FwPSJyb3VuZCIgc3Ryb2tlLWxpbmVqb2luPSJyb3VuZCIgc3Ryb2tlLXdpZHRoPSI1IiBkPSJNMzIgOTBsNDAtNDAtNDAtNDAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen]{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48ZGVmcz48c3R5bGU+LmF7ZmlsbDpub25lO3N0cm9rZTojZmZmO3N0cm9rZS1saW5lY2FwOnJvdW5kO3N0cm9rZS1saW5lam9pbjpyb3VuZDtzdHJva2Utd2lkdGg6NXB4fTwvc3R5bGU+PC9kZWZzPjxyZWN0IGNsYXNzPSJhIiB4PSIxMCIgeT0iMjAiIHdpZHRoPSI4MCIgaGVpZ2h0PSI2MCIgcng9IjUuNjciLz48cGF0aCBjbGFzcz0iYSIgZD0iTTQwIDcwSDIwVjUwbTIwIDBMMjAgNzBtNDAtNDBoMjB2MjBtLTIwIDBsMjAtMjAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button.exit[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button.exit[data-bespoke-marp-osc=fullscreen]{background-image:url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48ZGVmcz48c3R5bGU+LmF7ZmlsbDpub25lO3N0cm9rZTojZmZmO3N0cm9rZS1saW5lY2FwOnJvdW5kO3N0cm9rZS1saW5lam9pbjpyb3VuZDtzdHJva2Utd2lkdGg6NXB4fTwvc3R5bGU+PC9kZWZzPjxyZWN0IGNsYXNzPSJhIiB4PSIxMCIgeT0iMjAiIHdpZHRoPSI4MCIgaGVpZ2h0PSI2MCIgcng9IjUuNjciLz48cGF0aCBjbGFzcz0iYSIgZD0iTTIwIDUwaDIwdjIwbS0yMCAwbDIwLTIwbTQwIDBINjBWMzBtMjAgMEw2MCA1MCIvPjwvc3ZnPg==")}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter]{background:transparent url("data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAxMDAgMTAwIj48ZGVmcz48c3R5bGU+LmF7ZmlsbDpub25lO3N0cm9rZTojZmZmO3N0cm9rZS1saW5lY2FwOnJvdW5kO3N0cm9rZS13aWR0aDo1cHh9PC9zdHlsZT48L2RlZnM+PHBhdGggY2xhc3M9ImEiIGQ9Ik0yMCA2MGgtNWE1IDUgMCAwMS01LTVWMjBhNSA1IDAgMDE1LTVoNjBhNSA1IDAgMDE1IDV2NU0zMCA4NWg2MCIvPjxyZWN0IHg9IjMwIiB5PSIzNSIgd2lkdGg9IjYwIiBoZWlnaHQ9IjQwIiByeD0iNSIgZmlsbD0ibm9uZSIgc3Ryb2tlPSIjZmZmIi8+PHJlY3QgY2xhc3M9ImEiIHg9IjMwIiB5PSIzNSIgd2lkdGg9IjYwIiBoZWlnaHQ9IjQwIiByeD0iNSIvPjxwYXRoIGNsYXNzPSJhIiBkPSJNNDAgNTBoNDBNNDAgNjBoMzAiLz48L3N2Zz4=") no-repeat 50%;background-size:contain;overflow:hidden;text-indent:100%;white-space:nowrap}body,html{height:100%;margin:0}body{background:#000;overflow:hidden}svg.bespoke-marp-slide{opacity:0;pointer-events:none;z-index:-1}svg.bespoke-marp-slide.bespoke-marp-active{opacity:1;pointer-events:auto;z-index:0}svg.bespoke-marp-slide[data-bespoke-marp-load=hideable]{display:none}svg.bespoke-marp-slide[data-bespoke-marp-load=hideable].bespoke-marp-active{display:block}[data-bespoke-marp-fragment=inactive]{visibility:hidden}body[data-bespoke-view=""] .bespoke-marp-parent,body[data-bespoke-view=next] .bespoke-marp-parent{bottom:0;left:0;position:absolute;right:0;top:0}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc{background:rgba(0,0,0,.65);border-radius:7px;bottom:50px;color:#fff;display:block;font-family:Helvetica,Arial,sans-serif;font-size:16px;left:50%;line-height:0;opacity:1;padding:12px;position:absolute;touch-action:manipulation;transform:translateX(-50%);transition:opacity .2s linear;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;white-space:nowrap;z-index:1;will-change:transform}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>*,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>*{margin-left:6px}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>:first-child,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>:first-child{margin-left:0}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>span,body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>span{opacity:.8}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>span[data-bespoke-marp-osc=page],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>span[data-bespoke-marp-osc=page]{display:inline-block;min-width:140px;text-align:center}body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=""] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=fullscreen],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=next],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=presenter],body[data-bespoke-view=next] .bespoke-marp-parent>.bespoke-marp-osc>button[data-bespoke-marp-osc=prev]{height:32px;line-height:32px;width:32px}body[data-bespoke-view=""] .bespoke-marp-parent.bespoke-marp-inactive,body[data-bespoke-view=next] .bespoke-marp-parent.bespoke-marp-inactive{cursor:none}body[data-bespoke-view=""] .bespoke-marp-parent.bespoke-marp-inactive>.bespoke-marp-osc,body[data-bespoke-view=next] .bespoke-marp-parent.bespoke-marp-inactive>.bespoke-marp-osc{opacity:0;pointer-events:none}body[data-bespoke-view=""] svg.bespoke-marp-slide,body[data-bespoke-view=next] svg.bespoke-marp-slide{height:100%;left:0;position:absolute;top:0;width:100%}body[data-bespoke-view=""] .bespoke-progress-parent{background:#222;display:flex;height:5px;width:100%}body[data-bespoke-view=""] .bespoke-progress-parent+.bespoke-marp-parent{top:5px}body[data-bespoke-view=""] .bespoke-progress-parent .bespoke-progress-bar{flex:0 0 0;background:#0288d1;transition:flex-basis .2s cubic-bezier(0,1,1,1)}body[data-bespoke-view=next]{background:transparent}body[data-bespoke-view=presenter]{background:#161616}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container{height:100%;left:0;position:absolute;top:0;width:100%;display:grid;grid-template-columns:2fr 1fr;grid-template-rows:minmax(140px,1fr) 2fr 3em;grid-template-areas:"current next" "current note" "info note"}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent{grid-area:current;position:relative;overflow:hidden}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent svg.bespoke-marp-slide{height:calc(100% - 40px);left:20px;position:absolute;pointer-events:none;top:20px;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;width:calc(100% - 40px)}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-parent svg.bespoke-marp-slide.bespoke-marp-active{-webkit-filter:drop-shadow(0 3px 10px rgba(0,0,0,.5));filter:drop-shadow(0 3px 10px rgba(0,0,0,.5))}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container{background:#222;cursor:pointer;display:none;grid-area:next;overflow:hidden;position:relative}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container.active{display:block}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-next-container iframe.bespoke-marp-presenter-next{background:transparent;border:0;display:block;-webkit-filter:drop-shadow(0 3px 10px rgba(0,0,0,.5));filter:drop-shadow(0 3px 10px rgba(0,0,0,.5));height:calc(100% - 40px);left:20px;position:absolute;pointer-events:none;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none;top:20px;width:calc(100% - 40px)}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container{background:#222;color:#ddd;grid-area:note}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note{margin:20px;width:calc(100% - 40px);height:calc(100% - 40px);box-sizing:border-box;overflow:auto;padding-right:3px;white-space:pre-wrap;word-wrap:break-word;scrollbar-width:thin;scrollbar-color:hsla(0,0%,86.7%,.5) transparent}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar{width:6px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar-track{background:transparent}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note::-webkit-scrollbar-thumb{background:hsla(0,0%,86.7%,.5);border-radius:6px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note:empty{pointer-events:none}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note.active{display:block}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note p:first-child{margin-top:0}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-note-container .bespoke-marp-note p:last-child{margin-bottom:0}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container{align-items:center;box-sizing:border-box;color:#ddd;display:flex;flex-wrap:nowrap;grid-area:info;justify-content:center;padding:0 10px}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-time,body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-timer{display:block;box-sizing:border-box;padding:0 10px;white-space:nowrap;width:100%}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container button{height:1.5em;line-height:1.5em;width:1.5em}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page{order:2;text-align:center}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-page .bespoke-marp-presenter-info-page-text{display:inline-block;min-width:120px;text-align:center}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-time{color:#999;order:1;text-align:left}body[data-bespoke-view=presenter] .bespoke-marp-presenter-container .bespoke-marp-presenter-info-container .bespoke-marp-presenter-info-timer{color:#999;order:3;text-align:right}}@media print{.bespoke-marp-presenter-info-container,.bespoke-marp-presenter-next-container,.bespoke-marp-presenter-note-container{display:none}}</style><style>div#p>svg>foreignObject>section{width:1280px;height:720px;box-sizing:border-box;overflow:hidden;position:relative;scroll-snap-align:center center}div#p>svg>foreignObject>section:after{bottom:0;content:attr(data-marpit-pagination);padding:inherit;pointer-events:none;position:absolute;right:0}div#p>svg>foreignObject>section:not([data-marpit-pagination]):after{display:none}/* Normalization */div#p>svg>foreignObject>section h1{font-size:2em;margin:0.67em 0}div#p>svg>foreignObject>section video::-webkit-media-controls{will-change:transform}@page{size:1280px 720px;margin:0}@media print{body,html{background-color:#fff;margin:0;page-break-inside:avoid;break-inside:avoid-page}div#p>svg>foreignObject>section{page-break-before:always;break-before:page}div#p>svg>foreignObject>section,div#p>svg>foreignObject>section *{-webkit-print-color-adjust:exact!important;color-adjust:exact!important}div#p>svg[data-marpit-svg]{display:block;height:100vh;width:100vw}} +/*! + * Marp default theme. + * + * @theme default + * @author Yuki Hattori + * + * @auto-scaling true + * @size 4:3 960px 720px + */div#p>svg>foreignObject>section .octicon{display:inline-block;fill:currentColor;vertical-align:text-bottom}div#p>svg>foreignObject>section .anchor{float:left;line-height:1;margin-left:-20px;padding-right:4px}div#p>svg>foreignObject>section .anchor:focus{outline:none}div#p>svg>foreignObject>section h1 .octicon-link,div#p>svg>foreignObject>section h2 .octicon-link,div#p>svg>foreignObject>section h3 .octicon-link,div#p>svg>foreignObject>section h4 .octicon-link,div#p>svg>foreignObject>section h5 .octicon-link,div#p>svg>foreignObject>section h6 .octicon-link{color:#1b1f23;vertical-align:middle;visibility:hidden}div#p>svg>foreignObject>section h1:hover .anchor,div#p>svg>foreignObject>section h2:hover .anchor,div#p>svg>foreignObject>section h3:hover .anchor,div#p>svg>foreignObject>section h4:hover .anchor,div#p>svg>foreignObject>section h5:hover .anchor,div#p>svg>foreignObject>section h6:hover .anchor{text-decoration:none}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link{visibility:visible}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link:before{width:16px;height:16px;content:" ";display:inline-block;background-image:url("data:image/svg+xml;charset=utf-8,%3Csvg xmlns='http://www.w3.org/2000/svg' width='16' height='16' aria-hidden='true'%3E%3Cpath fill-rule='evenodd' d='M4 9h1v1H4c-1.5 0-3-1.69-3-3.5S2.55 3 4 3h4c1.45 0 3 1.69 3 3.5 0 1.41-.91 2.72-2 3.25V8.59c.58-.45 1-1.27 1-2.09C10 5.22 8.98 4 8 4H4c-.98 0-2 1.22-2 2.5S3 9 4 9zm9-3h-1v1h1c1 0 2 1.22 2 2.5S13.98 12 13 12H9c-.98 0-2-1.22-2-2.5 0-.83.42-1.64 1-2.09V6.25c-1.09.53-2 1.84-2 3.25C6 11.31 7.55 13 9 13h4c1.45 0 3-1.69 3-3.5S14.5 6 13 6z'/%3E%3C/svg%3E")}div#p>svg>foreignObject>section{-ms-text-size-adjust:100%;-webkit-text-size-adjust:100%;color:#24292e;font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica,Arial,sans-serif,Apple Color Emoji,Segoe UI Emoji;font-size:16px;line-height:1.5;word-wrap:break-word}div#p>svg>foreignObject>section details{display:block}div#p>svg>foreignObject>section summary{display:list-item}div#p>svg>foreignObject>section a{background-color:initial}div#p>svg>foreignObject>section a:active,div#p>svg>foreignObject>section a:hover{outline-width:0}div#p>svg>foreignObject>section strong{font-weight:inherit;font-weight:bolder}div#p>svg>foreignObject>section h1{margin:.67em 0}div#p>svg>foreignObject>section img{border-style:none}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section kbd,div#p>svg>foreignObject>section pre{font-family:monospace,monospace;font-size:1em}div#p>svg>foreignObject>section hr{box-sizing:initial;overflow:visible}div#p>svg>foreignObject>section input{font:inherit;margin:0;overflow:visible}div#p>svg>foreignObject>section [type=checkbox]{padding:0}div#p>svg>foreignObject>section *,div#p>svg>foreignObject>section [type=checkbox]{box-sizing:border-box}div#p>svg>foreignObject>section input{font-family:inherit;font-size:inherit;line-height:inherit}div#p>svg>foreignObject>section a{color:#0366d6;text-decoration:none}div#p>svg>foreignObject>section a:hover{text-decoration:underline}div#p>svg>foreignObject>section strong{font-weight:600}div#p>svg>foreignObject>section hr{height:0;margin:15px 0;overflow:hidden;background:transparent;border-bottom:1px solid #dfe2e5}div#p>svg>foreignObject>section hr:after,div#p>svg>foreignObject>section hr:before{display:table;content:""}div#p>svg>foreignObject>section hr:after{clear:both}div#p>svg>foreignObject>section table{border-spacing:0;border-collapse:collapse}div#p>svg>foreignObject>section td,div#p>svg>foreignObject>section th{padding:0}div#p>svg>foreignObject>section details summary{cursor:pointer}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2,div#p>svg>foreignObject>section h3,div#p>svg>foreignObject>section h4,div#p>svg>foreignObject>section h5,div#p>svg>foreignObject>section h6{margin-top:0;margin-bottom:0}div#p>svg>foreignObject>section h1{font-size:32px}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2{font-weight:600}div#p>svg>foreignObject>section h2{font-size:24px}div#p>svg>foreignObject>section h3{font-size:20px}div#p>svg>foreignObject>section h3,div#p>svg>foreignObject>section h4{font-weight:600}div#p>svg>foreignObject>section h4{font-size:16px}div#p>svg>foreignObject>section h5{font-size:14px}div#p>svg>foreignObject>section h5,div#p>svg>foreignObject>section h6{font-weight:600}div#p>svg>foreignObject>section h6{font-size:12px}div#p>svg>foreignObject>section p{margin-top:0;margin-bottom:10px}div#p>svg>foreignObject>section blockquote{margin:0}div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section ul{padding-left:0;margin-top:0;margin-bottom:0}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ul ol{list-style-type:lower-roman}div#p>svg>foreignObject>section ol ol ol,div#p>svg>foreignObject>section ol ul ol,div#p>svg>foreignObject>section ul ol ol,div#p>svg>foreignObject>section ul ul ol{list-style-type:lower-alpha}div#p>svg>foreignObject>section dd{margin-left:0}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section pre{font-family:SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;font-size:12px}div#p>svg>foreignObject>section pre{margin-top:0;margin-bottom:0}div#p>svg>foreignObject>section input::-webkit-inner-spin-button,div#p>svg>foreignObject>section input::-webkit-outer-spin-button{margin:0;-webkit-appearance:none;appearance:none}div#p>svg>foreignObject>section :checked+.radio-label{position:relative;z-index:1;border-color:#0366d6}div#p>svg>foreignObject>section .border{border:1px solid #e1e4e8!important}div#p>svg>foreignObject>section .border-0{border:0!important}div#p>svg>foreignObject>section .border-bottom{border-bottom:1px solid #e1e4e8!important}div#p>svg>foreignObject>section .rounded-1{border-radius:3px!important}div#p>svg>foreignObject>section .bg-white{background-color:#fff!important}div#p>svg>foreignObject>section .bg-gray-light{background-color:#fafbfc!important}div#p>svg>foreignObject>section .text-gray-light{color:#6a737d!important}div#p>svg>foreignObject>section .pl-3,div#p>svg>foreignObject>section .px-3{padding-left:16px!important}div#p>svg>foreignObject>section .px-3{padding-right:16px!important}div#p>svg>foreignObject>section .f6{font-size:12px!important}div#p>svg>foreignObject>section .lh-condensed{line-height:1.25!important}div#p>svg>foreignObject>section .text-bold{font-weight:600!important}div#p>svg>foreignObject>section .pl-c{color:#6a737d}div#p>svg>foreignObject>section .pl-c1,div#p>svg>foreignObject>section .pl-s .pl-v{color:#005cc5}div#p>svg>foreignObject>section .pl-e,div#p>svg>foreignObject>section .pl-en{color:#6f42c1}div#p>svg>foreignObject>section .pl-s .pl-s1,div#p>svg>foreignObject>section .pl-smi{color:#24292e}div#p>svg>foreignObject>section .pl-ent{color:#22863a}div#p>svg>foreignObject>section .pl-k{color:#d73a49}div#p>svg>foreignObject>section .pl-pds,div#p>svg>foreignObject>section .pl-s,div#p>svg>foreignObject>section .pl-s .pl-pse .pl-s1,div#p>svg>foreignObject>section .pl-sr,div#p>svg>foreignObject>section .pl-sr .pl-cce,div#p>svg>foreignObject>section .pl-sr .pl-sra,div#p>svg>foreignObject>section .pl-sr .pl-sre{color:#032f62}div#p>svg>foreignObject>section .pl-smw,div#p>svg>foreignObject>section .pl-v{color:#e36209}div#p>svg>foreignObject>section .pl-bu{color:#b31d28}div#p>svg>foreignObject>section .pl-ii{color:#fafbfc;background-color:#b31d28}div#p>svg>foreignObject>section .pl-c2{color:#fafbfc;background-color:#d73a49}div#p>svg>foreignObject>section .pl-c2:before{content:"^M"}div#p>svg>foreignObject>section .pl-sr .pl-cce{font-weight:700;color:#22863a}div#p>svg>foreignObject>section .pl-ml{color:#735c0f}div#p>svg>foreignObject>section .pl-mh,div#p>svg>foreignObject>section .pl-mh .pl-en,div#p>svg>foreignObject>section .pl-ms{font-weight:700;color:#005cc5}div#p>svg>foreignObject>section .pl-mi{font-style:italic;color:#24292e}div#p>svg>foreignObject>section .pl-mb{font-weight:700;color:#24292e}div#p>svg>foreignObject>section .pl-md{color:#b31d28;background-color:#ffeef0}div#p>svg>foreignObject>section .pl-mi1{color:#22863a;background-color:#f0fff4}div#p>svg>foreignObject>section .pl-mc{color:#e36209;background-color:#ffebda}div#p>svg>foreignObject>section .pl-mi2{color:#f6f8fa;background-color:#005cc5}div#p>svg>foreignObject>section .pl-mdr{font-weight:700;color:#6f42c1}div#p>svg>foreignObject>section .pl-ba{color:#586069}div#p>svg>foreignObject>section .pl-sg{color:#959da5}div#p>svg>foreignObject>section .pl-corl{text-decoration:underline;color:#032f62}div#p>svg>foreignObject>section .mb-0{margin-bottom:0!important}div#p>svg>foreignObject>section .my-2{margin-bottom:8px!important;margin-top:8px!important}div#p>svg>foreignObject>section .pl-0{padding-left:0!important}div#p>svg>foreignObject>section .py-0{padding-top:0!important;padding-bottom:0!important}div#p>svg>foreignObject>section .pl-1{padding-left:4px!important}div#p>svg>foreignObject>section .pl-2{padding-left:8px!important}div#p>svg>foreignObject>section .py-2{padding-top:8px!important;padding-bottom:8px!important}div#p>svg>foreignObject>section .pl-3{padding-left:16px!important}div#p>svg>foreignObject>section .pl-4{padding-left:24px!important}div#p>svg>foreignObject>section .pl-5{padding-left:32px!important}div#p>svg>foreignObject>section .pl-6{padding-left:40px!important}div#p>svg>foreignObject>section .pl-7{padding-left:48px!important}div#p>svg>foreignObject>section .pl-8{padding-left:64px!important}div#p>svg>foreignObject>section .pl-9{padding-left:80px!important}div#p>svg>foreignObject>section .pl-10{padding-left:96px!important}div#p>svg>foreignObject>section .pl-11{padding-left:112px!important}div#p>svg>foreignObject>section .pl-12{padding-left:128px!important}div#p>svg>foreignObject>section hr{border-bottom-color:#eee}div#p>svg>foreignObject>section kbd{display:inline-block;padding:3px 5px;font:11px SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;line-height:10px;color:#444d56;vertical-align:middle;background-color:#fafbfc;border:1px solid #d1d5da;border-radius:3px;box-shadow:inset 0 -1px 0 #d1d5da}div#p>svg>foreignObject>section:after,div#p>svg>foreignObject>section:before{display:table + /* content:""; */}div#p>svg>foreignObject>section:after{clear:both}div#p>svg>foreignObject>section>:first-child{margin-top:0!important}div#p>svg>foreignObject>section>:last-child{margin-bottom:0!important}div#p>svg>foreignObject>section a:not([href]){color:inherit;text-decoration:none}div#p>svg>foreignObject>section blockquote,div#p>svg>foreignObject>section details,div#p>svg>foreignObject>section dl,div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section p,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section table,div#p>svg>foreignObject>section ul{margin-top:0;margin-bottom:16px}div#p>svg>foreignObject>section hr{height:.25em;padding:0;margin:24px 0;background-color:#e1e4e8;border:0}div#p>svg>foreignObject>section blockquote{padding:0 1em;color:#6a737d;border-left:.25em solid #dfe2e5}div#p>svg>foreignObject>section blockquote>:first-child{margin-top:0}div#p>svg>foreignObject>section blockquote>:last-child{margin-bottom:0}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2,div#p>svg>foreignObject>section h3,div#p>svg>foreignObject>section h4,div#p>svg>foreignObject>section h5,div#p>svg>foreignObject>section h6{margin-top:24px;margin-bottom:16px;font-weight:600;line-height:1.25}div#p>svg>foreignObject>section h1{font-size:2em}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2{padding-bottom:.3em;border-bottom:1px solid #eaecef}div#p>svg>foreignObject>section h2{font-size:1.5em}div#p>svg>foreignObject>section h3{font-size:1.25em}div#p>svg>foreignObject>section h4{font-size:1em}div#p>svg>foreignObject>section h5{font-size:.875em}div#p>svg>foreignObject>section h6{font-size:.85em;color:#6a737d}div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section ul{padding-left:2em}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ol ul,div#p>svg>foreignObject>section ul ol,div#p>svg>foreignObject>section ul ul{margin-top:0;margin-bottom:0}div#p>svg>foreignObject>section li{word-wrap:break-all}div#p>svg>foreignObject>section li>p{margin-top:16px}div#p>svg>foreignObject>section li+li{margin-top:.25em}div#p>svg>foreignObject>section dl{padding:0}div#p>svg>foreignObject>section dl dt{padding:0;margin-top:16px;font-size:1em;font-style:italic;font-weight:600}div#p>svg>foreignObject>section dl dd{padding:0 16px;margin-bottom:16px}div#p>svg>foreignObject>section table{display:block;width:100%;overflow:auto}div#p>svg>foreignObject>section table th{font-weight:600}div#p>svg>foreignObject>section table td,div#p>svg>foreignObject>section table th{padding:6px 13px;border:1px solid #dfe2e5}div#p>svg>foreignObject>section table tr{background-color:#fff;border-top:1px solid #c6cbd1}div#p>svg>foreignObject>section table tr:nth-child(2n){background-color:#f6f8fa}div#p>svg>foreignObject>section img{max-width:100%;box-sizing:initial;background-color:#fff}div#p>svg>foreignObject>section img[align=right]{padding-left:20px}div#p>svg>foreignObject>section img[align=left]{padding-right:20px}div#p>svg>foreignObject>section code{padding:.2em .4em;margin:0;font-size:85%;background-color:rgba(27,31,35,.05);border-radius:3px}div#p>svg>foreignObject>section pre{word-wrap:normal}div#p>svg>foreignObject>section pre>code{padding:0;margin:0;font-size:100%;word-break:normal;white-space:pre;background:transparent;border:0}div#p>svg>foreignObject>section .highlight{margin-bottom:16px}div#p>svg>foreignObject>section .highlight pre{margin-bottom:0;word-break:normal}div#p>svg>foreignObject>section pre{padding:16px;overflow:auto;font-size:85%;line-height:1.45;background-color:#f6f8fa;border-radius:3px}div#p>svg>foreignObject>section pre code{display:inline;max-width:auto;padding:0;margin:0;overflow:visible;line-height:inherit;word-wrap:normal;background-color:initial;border:0}div#p>svg>foreignObject>section .commit-tease-sha{display:inline-block;font-family:SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;font-size:90%;color:#444d56}div#p>svg>foreignObject>section .full-commit .btn-outline:not(:disabled):hover{color:#005cc5;border-color:#005cc5}div#p>svg>foreignObject>section .blob-wrapper{overflow-x:auto;overflow-y:hidden}div#p>svg>foreignObject>section .blob-wrapper-embedded{max-height:240px;overflow-y:auto}div#p>svg>foreignObject>section .blob-num{width:1%;min-width:50px;padding-right:10px;padding-left:10px;font-family:SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;font-size:12px;line-height:20px;color:rgba(27,31,35,.3);text-align:right;white-space:nowrap;vertical-align:top;cursor:pointer;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none}div#p>svg>foreignObject>section .blob-num:hover{color:rgba(27,31,35,.6)}div#p>svg>foreignObject>section .blob-num:before{content:attr(data-line-number)}div#p>svg>foreignObject>section .blob-code{position:relative;padding-right:10px;padding-left:10px;line-height:20px;vertical-align:top}div#p>svg>foreignObject>section .blob-code-inner{overflow:visible;font-family:SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;font-size:12px;color:#24292e;word-wrap:normal;white-space:pre}div#p>svg>foreignObject>section .pl-token.active,div#p>svg>foreignObject>section .pl-token:hover{cursor:pointer;background:#ffea7f}div#p>svg>foreignObject>section .tab-size[data-tab-size="1"]{-moz-tab-size:1;-o-tab-size:1;tab-size:1}div#p>svg>foreignObject>section .tab-size[data-tab-size="2"]{-moz-tab-size:2;-o-tab-size:2;tab-size:2}div#p>svg>foreignObject>section .tab-size[data-tab-size="3"]{-moz-tab-size:3;-o-tab-size:3;tab-size:3}div#p>svg>foreignObject>section .tab-size[data-tab-size="4"]{-moz-tab-size:4;-o-tab-size:4;tab-size:4}div#p>svg>foreignObject>section .tab-size[data-tab-size="5"]{-moz-tab-size:5;-o-tab-size:5;tab-size:5}div#p>svg>foreignObject>section .tab-size[data-tab-size="6"]{-moz-tab-size:6;-o-tab-size:6;tab-size:6}div#p>svg>foreignObject>section .tab-size[data-tab-size="7"]{-moz-tab-size:7;-o-tab-size:7;tab-size:7}div#p>svg>foreignObject>section .tab-size[data-tab-size="8"]{-moz-tab-size:8;-o-tab-size:8;tab-size:8}div#p>svg>foreignObject>section .tab-size[data-tab-size="9"]{-moz-tab-size:9;-o-tab-size:9;tab-size:9}div#p>svg>foreignObject>section .tab-size[data-tab-size="10"]{-moz-tab-size:10;-o-tab-size:10;tab-size:10}div#p>svg>foreignObject>section .tab-size[data-tab-size="11"]{-moz-tab-size:11;-o-tab-size:11;tab-size:11}div#p>svg>foreignObject>section .tab-size[data-tab-size="12"]{-moz-tab-size:12;-o-tab-size:12;tab-size:12}div#p>svg>foreignObject>section .task-list-item{list-style-type:none}div#p>svg>foreignObject>section .task-list-item+.task-list-item{margin-top:3px}div#p>svg>foreignObject>section .task-list-item input{margin:0 .2em .25em -1.6em;vertical-align:middle}div#p>svg>foreignObject>section .hljs{display:block;background:#fff;padding:.5em;color:#333;overflow-x:auto}div#p>svg>foreignObject>section .hljs-comment,div#p>svg>foreignObject>section .hljs-meta{color:#969896}div#p>svg>foreignObject>section .hljs-emphasis,div#p>svg>foreignObject>section .hljs-quote,div#p>svg>foreignObject>section .hljs-strong,div#p>svg>foreignObject>section .hljs-template-variable,div#p>svg>foreignObject>section .hljs-variable{color:#df5000}div#p>svg>foreignObject>section .hljs-keyword,div#p>svg>foreignObject>section .hljs-selector-tag,div#p>svg>foreignObject>section .hljs-type{color:#d73a49}div#p>svg>foreignObject>section .hljs-attribute,div#p>svg>foreignObject>section .hljs-bullet,div#p>svg>foreignObject>section .hljs-literal,div#p>svg>foreignObject>section .hljs-symbol{color:#0086b3}div#p>svg>foreignObject>section .hljs-name,div#p>svg>foreignObject>section .hljs-section{color:#63a35c}div#p>svg>foreignObject>section .hljs-tag{color:#333}div#p>svg>foreignObject>section .hljs-attr,div#p>svg>foreignObject>section .hljs-selector-attr,div#p>svg>foreignObject>section .hljs-selector-class,div#p>svg>foreignObject>section .hljs-selector-id,div#p>svg>foreignObject>section .hljs-selector-pseudo,div#p>svg>foreignObject>section .hljs-title{color:#6f42c1}div#p>svg>foreignObject>section .hljs-addition{color:#55a532;background-color:#eaffea}div#p>svg>foreignObject>section .hljs-deletion{color:#bd2c00;background-color:#ffecec}div#p>svg>foreignObject>section .hljs-link{text-decoration:underline}div#p>svg>foreignObject>section .hljs-number{color:#005cc5}div#p>svg>foreignObject>section .hljs-string{color:#032f62}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{max-height:563px}div#p>svg>foreignObject>section h1{color:#246;font-size:1.6em}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2{border-bottom:none}div#p>svg>foreignObject>section h2{font-size:1.3em}div#p>svg>foreignObject>section h3{font-size:1.1em}div#p>svg>foreignObject>section h4{font-size:1.05em}div#p>svg>foreignObject>section h5{font-size:1em}div#p>svg>foreignObject>section h6{font-size:.9em}div#p>svg>foreignObject>section h1 strong,div#p>svg>foreignObject>section h2 strong,div#p>svg>foreignObject>section h3 strong,div#p>svg>foreignObject>section h4 strong,div#p>svg>foreignObject>section h5 strong,div#p>svg>foreignObject>section h6 strong{font-weight:inherit;color:#48c}div#p>svg>foreignObject>section hr{height:0;padding-top:.25em}div#p>svg>foreignObject>section pre{border:1px solid #999;line-height:1.15;overflow:visible}div#p>svg>foreignObject>section pre code svg[data-marp-fitting=svg]{max-height:529px}div#p>svg>foreignObject>section footer,div#p>svg>foreignObject>section header{margin:0;position:absolute;left:30px;color:hsla(0,0%,40%,.75);font-size:18px}div#p>svg>foreignObject>section header{top:21px}div#p>svg>foreignObject>section footer{bottom:21px}div#p>svg>foreignObject>section{align-items:stretch;background:#fff;display:flex;flex-direction:column;flex-wrap:nowrap;font-size:29px;height:720px;justify-content:center;padding:78.5px;width:1280px}div#p>svg>foreignObject>section>:last-child,div#p>svg>foreignObject>section[data-footer]>:nth-last-child(2){margin-bottom:0}div#p>svg>foreignObject>section>:first-child,div#p>svg>foreignObject>section>header:first-child+*{margin-top:0}div#p>svg>foreignObject>section:after{position:absolute;padding:0;right:30px;bottom:21px;font-size:24px;color:#777}div#p>svg>foreignObject>section.invert{background-color:#222;color:#e6eaf0}div#p>svg>foreignObject>section.invert:after{color:#999}div#p>svg>foreignObject>section.invert img{background-color:transparent}div#p>svg>foreignObject>section.invert a{color:#50b3ff}div#p>svg>foreignObject>section.invert h1{color:#a3c5e7}div#p>svg>foreignObject>section.invert h2,div#p>svg>foreignObject>section.invert h3,div#p>svg>foreignObject>section.invert h4,div#p>svg>foreignObject>section.invert h5{color:#ebeff5}div#p>svg>foreignObject>section.invert blockquote,div#p>svg>foreignObject>section.invert h6{border-color:#3d3f43;color:#939699}div#p>svg>foreignObject>section.invert h1 strong,div#p>svg>foreignObject>section.invert h2 strong,div#p>svg>foreignObject>section.invert h3 strong,div#p>svg>foreignObject>section.invert h4 strong,div#p>svg>foreignObject>section.invert h5 strong,div#p>svg>foreignObject>section.invert h6 strong{color:#7bf}div#p>svg>foreignObject>section.invert hr{background-color:#3d3f43}div#p>svg>foreignObject>section.invert footer,div#p>svg>foreignObject>section.invert header{color:hsla(0,0%,60%,.75)}div#p>svg>foreignObject>section.invert code,div#p>svg>foreignObject>section.invert kbd{background-color:#111}div#p>svg>foreignObject>section.invert kbd{border-color:#666;box-shadow:inset 0 -1px 0 #555;color:#e6eaf0}div#p>svg>foreignObject>section.invert table tr{background-color:#12181d;border-color:#60657b}div#p>svg>foreignObject>section.invert table tr:nth-child(2n){background-color:#1b2024}div#p>svg>foreignObject>section.invert table td,div#p>svg>foreignObject>section.invert table th{border-color:#5b5e61}div#p>svg>foreignObject>section.invert pre{background-color:#0a0e12;border-color:#777}div#p>svg>foreignObject>section.invert pre code{background-color:transparent}div#p>svg>foreignObject>section[data-color] h1,div#p>svg>foreignObject>section[data-color] h2,div#p>svg>foreignObject>section[data-color] h3,div#p>svg>foreignObject>section[data-color] h4,div#p>svg>foreignObject>section[data-color] h5,div#p>svg>foreignObject>section[data-color] h6{color:currentColor}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{display:block;height:auto;width:100%}@supports (-ms-ime-align:auto){div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{position:static}}div#p>svg>foreignObject>section svg[data-marp-fitting=svg].__reflow__{content:""}@supports (-ms-ime-align:auto){div#p>svg>foreignObject>section svg[data-marp-fitting=svg].__reflow__{position:relative}}div#p>svg>foreignObject>section [data-marp-fitting-svg-content]{display:table;white-space:nowrap}div#p>svg>foreignObject>section [data-marp-fitting-svg-content-wrap]{white-space:pre}div#p>svg>foreignObject>section img[data-marp-twemoji]{background:transparent;height:1em;margin:0 .05em 0 .1em;vertical-align:-.1em;width:1em} + +/* @theme example */div#p>svg>foreignObject>section{background-image:url("assets/logo.svg");background-position:right 3% bottom 2%;background-repeat:no-repeat;background-attachment:5%;background-size:20% auto} + +/* @theme mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd */div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="1" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1><svg data-marp-fitting="svg"><foreignObject><span data-marp-fitting-svg-content> Gears OSでモデル検査を実現する手法について</span></foreignObject></svg></h1> +<ul> +<li>東恩納 琢偉 +<ul> +<li>琉球大学理工学研究科 情報工学専攻</li> +</ul> +</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="2" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="2" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>研究目的</h1> +<ul> +<li>OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こり得る。</li> +<li>本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、今回はモデル検査による信頼性の保証について考察する。</li> +<li>またGearsOS そのものをGearsOS上でモデル検査する手法について考察する。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="3" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>Gears OS</h1> +<ul> +<li>軽量継続を基本とする言語 Contnution based C を用いて記述されている。</li> +<li>アプリケーションやサービスの信頼性をOSの機能として保証することを目指しています。</li> +<li>信頼性を保証する方法としてモデル検査による検証や、定理証明を用いる事で、信頼性へのアプローチを行っています。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="4" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>Continution based C</h1> +<ul> +<li>CbC とは C言語をベースとして、開発された言語でC言語との違いはプログラムにおける goto 文を用いて CodeGear という単位で遷移する。</li> +<li>goto 文による遷移は関数呼び出しとは異なり、stackや環境を隠して持つことがない。</li> +<li>以下は CbC によって記述された codeGear です。</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>code pickup_lfork(PhilsPtr <span class="hljs-keyword">self</span>, TaskPtr current_task) +{ + <span class="hljs-keyword">if</span> (<span class="hljs-keyword">self</span>->left_fork->owner == <span class="hljs-keyword">NULL</span>) { + <span class="hljs-keyword">self</span>->left_fork->owner = <span class="hljs-keyword">self</span>; + <span class="hljs-keyword">self</span>->next = pickup_rfork; + <span class="hljs-keyword">goto</span> scheduler(<span class="hljs-keyword">self</span>, current_task); + } <span class="hljs-keyword">else</span> { + <span class="hljs-keyword">self</span>->next = hungry1; + <span class="hljs-keyword">goto</span> scheduler(<span class="hljs-keyword">self</span>, current_task); +} +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="5" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>goto</h1> +<ul> +<li>goto 文はCbC における状態遷移に使われ、 goto の直後に遷移先を記述することで接続される。</li> +<li>goto による遷移は軽量継続と言い、関数呼び出しのような環境変数を持たず、遷移元の処理に囚われず、遷移先を自由に変更する事が可能である。これにより処理の間にメタレベルの計算を挿入する事が可能である。</li> +<li>CbC における遷移記述はそのまま状態遷移記述にすることができる。</li> +</ul> +<center><img src="./pic/input-outputDataSegment.svg" alt="" width="100%" height="100%" /></center> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="6" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>dataGear と meta dataGear</h1> +<ul> +<li>CbC における入力は dataGear と呼ばれる構造体になっており、ノーマルレベル<br /> +とメタレベルがある。</li> +<li>メタレベルには計算を行うCPUやメモリ、計算に関するノーマルレベルのdataGearを格納するcontext などがある。context は一般的なOSのプロセスに相当する。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="7" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>stub CodeGear</h1> +<ul> +<li>メタレベルから見ると、code Gearの入力はcontext ただ1つである。</li> +<li>ノーマルレベルからMeta dataGear であるcontext を直接参照してしまう事は、ユーザーがメタレベルに対して自由に記述できてしまう事になる。</li> +<li>この問題を防ぐため context から必要なノーマルレベルのdata Gearを取り出して、ノーマルレベルのcodeGearを呼び出し渡す処理を行う仲介役として、メタレベルの stub CodeGearがある。</li> +</ul> +<pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>__code clear<span class="hljs-constructor">SingleLinkedStack(<span class="hljs-params">struct</span> Context <span class="hljs-operator">*</span><span class="hljs-params">context</span>,<span class="hljs-params">struct</span> SingleLinkedStack<span class="hljs-operator">*</span> <span class="hljs-params">stack</span>,<span class="hljs-params">enum</span> Code <span class="hljs-params">next</span>)</span> { + stack->top = NULL; + goto meta(context, next); +} + +__code clear<span class="hljs-constructor">SingleLinkedStack_stub(<span class="hljs-params">struct</span> Context<span class="hljs-operator">*</span> <span class="hljs-params">context</span>)</span> { + SingleLinkedStack* stack = (SingleLinkedStack*)<span class="hljs-constructor">GearImpl(<span class="hljs-params">context</span>, Stack, <span class="hljs-params">stack</span>)</span>; + enum Code next = <span class="hljs-constructor">Gearef(<span class="hljs-params">context</span>, Stack)</span>->next; + goto clear<span class="hljs-constructor">SingleLinkedStack(<span class="hljs-params">context</span>, <span class="hljs-params">stack</span>, <span class="hljs-params">next</span>)</span>; +} +</span></span></foreignObject></svg></code></pre> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="8" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>contextと状態数</h1> +<ul> +<li>プログラムの非決定的な実行は、入力あるいは並列実行の非決定性から生じる。</li> +<li>並列実行の非決定性は、同時に実行される codeGear の順列並び替えになるので、それらの並び替えを生成し、その際に生じるcontextの状態を数え上げる事で、モデル検査を実装できる。</li> +<li>しかし、このcontextの状態はとても巨大になる事がある、そのためそれらを抽象化する必要性がある。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="9" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>GearsOSの実装</h1> +<ul> +<li>codeGear は処理の基本単位であり、並列処理などにより割り込まれることなく記述された通りに実行される必要がある。</li> +<li>しかし一般的には、他のcodeGearが共有されたdataGearに競合的に書き込んだり、割り込みにより処理が中断したりする。</li> +<li>しかし、GearsOSにおいては正しく実行される事を保証されるように実装されているとする。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="10" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>モデル検査</h1> +<ul> +<li>モデルとは検証したいアプリケーションやサービスの振る舞いや性質を抽象化して表現したものであり、抽象化の手法には以下のようなものがある。</li> +</ul> +<p>状態遷移モデル<br /> +論理モデル<br /> +組み合わせモデル<br /> +フローモデル ..etc</p> +<ul> +<li>このモデルが仕様を満たしているかどうかを検査するのがモデル検査である。</li> +<li>検査の要点によってモデルを使い分ける必要性がある。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="11" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>状態遷移モデル</h1> +<ul> +<li>今回行うモデル検査は状態遷移からプログラムの振る舞いを検証する。</li> +<li>状態遷移モデルとは、処理前と処理後の状態をつなぎ合わせる手法である。</li> +</ul> +<table> +<thead> +<tr> +<th>構成要素</th> +<th></th> +</tr> +</thead> +<tbody> +<tr> +<td>状態</td> +<td>プログラムの状態</td> +</tr> +<tr> +<td>初期状態</td> +<td>何らかの処理、計算が行われる前の状態</td> +</tr> +<tr> +<td>終了状態</td> +<td>処理、または計算が行われた状態</td> +</tr> +<tr> +<td>処理(計算)</td> +<td>状態を変化させる</td> +</tr> +<tr> +<td>遷移条件</td> +<td>状態が分岐する際の条件</td> +</tr> +</tbody> +</table> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="12" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>既存のモデル検査手法(SPIN)</h1> +<ul> +<li>一般的に扱われるモデル検査ツールとしてSPINがある。</li> +<li>SPIN はPromela (Process Meta Language)で記述される。</li> +<li>C言語と似た文法を持ち、元は通信プロトコルの検証として開発された言語であり、検証機を生成し、コンパイルと実行を行うことで検証される。</li> +<li>チャネルを使って通信や並列動作を記述する。</li> +<li>有限オートマトンに変換してモデル検査を行う。</li> +<li>Promelaへの書き換えが必要</li> +<li>SPIN での検査可能な性質<br /> +アサーション<br /> +デッドロック<br /> +到達性<br /> +進行性<br /> +線形時相論理で記述された仕様</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="13" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>既存のモデル検査手法(Java path Finder)</h1> +<ul> +<li>Java Path Finder はjavaプログラムの検査ツール</li> +<li>java バーチャルマシン(JVM) を直接シュミレーション実行している、これによりjavaのバイトコードを直接実行可能である。</li> +<li>バイトコードを状態遷移モデルとして扱い、実行時に遷移し得る状態を網羅的に検査している。</li> +<li>実行パターンを網羅的に調べるため、複数のプロセスの取り扱いができず、また状態空間が巨大な場合は、一部を抜き出して検査する必要がある。</li> +<li>JPF で検査可能な性質<br /> +スレッドの可能な実行すべてを調べる<br /> +デッドロックの検出<br /> +アサーション<br /> +Partial Order Reduction</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="14" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>モデル検査手法について</h1> +<ul> +<li>GearsOS におけるモデル検査はcode gear 単位の順列組み合わせによって行われる。</li> +<li>codegear 実行後の状態を、データベースに格納する。</li> +<li>新しい状態が生成されなくなった時モデル検査が終了する。</li> +<li>哲学者５人が次の状態に進めなくなった時をデッドロックとして検出する。</li> +<li>必要な状態はフォークの状態だけになるので、それ以外の状態は無視することができる。</li> +<li>これにより状態数を下げることができる。</li> +<li>つまり、問題に合わせたメタ計算により、モデル検査の状態数を下げることができる。</li> +<li>GearsOS による検証用プログラムとして Dining Philosohers Ploblem (DPP）を用いる。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="15" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>DPP(dining philosohers ploblem)</h1> +<ul> +<li>5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。</li> +<li>フォークは皿の間に１本ずつの計5本しかないため、すべての哲学者が同時に食事することはできず、また全員がフォークを1本ずつ持ってしまった場合、誰も食事することは出来ない。この状態をデッドロックとする。</li> +</ul> +<center><img src="./pic/dpp_image.svg" alt="" width="48%" height="48%" /></center> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="16" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>DPP</h1> +<ul> +<li>状態の構成要素は次の6つからなる。<br /> +<code>Pickup Right fork</code> <code> Pickup Left fork</code> <code>eating</code> <code> Put Right fork</code> <code>Put Left fork</code> <code>Thinking</code></li> +</ul> +<p><right><img src="./pic/dpp_image.svg" alt="" width="55%" height="55%" /></right></p> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="17" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>GeasOS におけるDPP実装(1/3)</h1> +<ul> +<li>5つのスレッドで並列処理を行う事で、哲学者の行動を再現する。</li> +<li>gearsOSには並列機構の par goto があり、これを使用するスケジューラーによって並列にスレッドを起動する。</li> +<li>par goto は引数として dataGear と実行後に継続する _exit をわたす。</li> +<li>par goto は複数スレッドでの実行であるので、各スレッドで実行後に__exitに継続する事で終了する。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="18" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>GearsOS におけるDPP実装(2/3)</h1> +<ul> +<li>マルチスレッドでのデータの一貫性を保証する手法としてCheck and Set (CAS) がある。</li> +<li>CAS を用いて値の比較、更新をアトミックに行う。</li> +<li>CAS は書き込みの際に、書き込む MetaCodeGear に更新前と更新後の値を渡し、更新前の値が保存されているメモリ番地の値と比較し同じデータがであれば書き込みを行う。異なる場合はほかからの書き込みがあったとみなし、値の更新に失敗し、もう一度CASを行う。</li> +<li>DPPの例題ではフォークがスレッドで共有されるデータにあたるので、CAS を用いることによってスレッド間での同期を行う。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="19" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>GearsOS におけるDPP実装(3/3)</h1> +<p>v- 5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表す。</p> +<ul> +<li>この状態遷移は goto next によって遷移し、metaCodeGear を 挟みメタレベルで各スレッドの状態を 各スレッドごとに用意した Memory Tree に保存する。</li> +<li>Memory Tree はstateDBによってまとめられ、同じ状態は共有される。</li> +<li>またDPPにおける状態遷移は無限ループであるため、stateDBを用いて同じ状態を検索することで、終了判定を行う。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="20" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>GearsOS でのモデル検査を実現する方法について</h1> +<ul> +<li>DPP をGearsOS 上のアプリケーションとして実装する。</li> +<li>DPP を codeGear のシャッフルの１つとして実行する。</li> +<li>可能な実行を生成する iterator を作成する</li> +<li>状態を記録する memory Tree と stateDB を作成する。</li> +</ul> +</section> +</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-theme="mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd" data-marpit-pagination="21" data-marpit-pagination-total="21" style="--paginate:true;--theme:mnjt2hxjszcthvc5m3hy4oi69bqkh2zeb6nunhwmdntd;"> +<h1>GearsOS の GearsOS によるモデル検査</h1> +<ul> +<li>GerasOS そのものも codeGear で記述されている。</li> +<li>CPU毎の C.context、共有するkernel のK.context、ユーザープログラムのU.context と考えることができ、これらはmeta dataGear であるK.context に含まれている。</li> +<li>U.context がDPPのような単純なものならば、OS全体のcontext も複雑にはならないため、これらをGearsOSで実行することが可能である。</li> +<li>GearsOS を含む codeGear のシャッフル実行を行う事ができれば、DPPと同じようにモデル検査を行う事ができる。</li> +<li>検査する codeGear と検査される codeGear は同じものであるが、実行する meta codeGear を異なっている。</li> +<li>異なるmeta codeGear を指定してコンパイルすることで実現できる。</li> +</ul> +</section> +<script>!function(){"use strict";function t(t){Array.from(document.getElementsByTagName("svg"),e=>{if(e.hasAttribute("data-marpit-svg")){const{clientHeight:r,clientWidth:a}=e;e.style.transform||(e.style.transform="translateZ(0)");const o=t||e.currentScale||1,i=e.viewBox.baseVal.width/o,n=e.viewBox.baseVal.height/o,s=Math.min(r/n,a/i);Array.from(e.querySelectorAll(":scope > foreignObject"),t=>{const e=t.x.baseVal.value,o=t.y.baseVal.value;Array.from(t.querySelectorAll(":scope > section"),t=>{t.style.transformOrigin||(t.style.transformOrigin="0 0");const l=(a-s*i)/2-e,c=(r-s*n)/2-o;t.style.transform=`translate3d(${l}px,${c}px,0) scale(${s}) translate(${e}px,${o}px)`})})}})}const e=(t,e,r)=>{if(t.getAttribute(e)!==r)return t.setAttribute(e,r),!0};function r(a=!0){for(const e of"Apple Computer, Inc."===navigator.vendor?[t]:[])e();Array.from(document.querySelectorAll('svg[data-marp-fitting="svg"]'),t=>{const r=t.firstChild,a=r.firstChild,{scrollWidth:o,scrollHeight:i}=a;let n,s=1;if(t.hasAttribute("data-marp-fitting-code")&&(n=t.parentElement.parentElement),t.hasAttribute("data-marp-fitting-math")&&(n=t.parentElement),n){const t=getComputedStyle(n),e=Math.ceil(n.clientWidth-parseFloat(t.paddingLeft)-parseFloat(t.paddingRight));e&&(s=e)}const l=Math.max(o,s),c=Math.max(i,1),p=`0 0 ${l} ${c}`;e(r,"width",""+l),e(r,"height",""+c),e(t,"preserveAspectRatio",getComputedStyle(t).getPropertyValue("--preserve-aspect-ratio")||"xMinYMin meet"),e(t,"viewBox",p)&&t.classList.toggle("__reflow__")}),a&&window.requestAnimationFrame(()=>r(a))}!function(){if("undefined"==typeof window)throw new Error("Marp Core's browser script is valid only in browser context.");window.marpCoreBrowserScript?console.warn("Marp Core's browser script has already executed."):(Object.defineProperty(window,"marpCoreBrowserScript",{value:!0}),r())}()}(); +</script></foreignObject></svg></div><script>!function(){"use strict";var e=function(e,t){var n,r=1===(e.parent||e).nodeType?e.parent||e:document.querySelector(e.parent||e),s=[].filter.call("string"==typeof e.slides?r.querySelectorAll(e.slides):e.slides||r.children,(function(e){return"SCRIPT"!==e.nodeName})),a={},o=function(e,t){return(t=t||{}).index=s.indexOf(e),t.slide=e,t},i=function(e,t){a[e]=(a[e]||[]).filter((function(e){return e!==t}))},l=function(e,t){return(a[e]||[]).reduce((function(e,n){return e&&!1!==n(t)}),!0)},c=function(e,t){s[e]&&(n&&l("deactivate",o(n,t)),n=s[e],l("activate",o(n,t)))},d=function(e,t){var r=s.indexOf(n)+e;l(e>0?"next":"prev",o(n,t))&&c(r,t)},u={off:i,on:function(e,t){return(a[e]||(a[e]=[])).push(t),i.bind(null,e,t)},fire:l,slide:function(e,t){if(!arguments.length)return s.indexOf(n);l("slide",o(s[e],t))&&c(e,t)},next:d.bind(null,1),prev:d.bind(null,-1),parent:r,slides:s,destroy:function(e){l("destroy",o(n,e)),a={}}};return(t||[]).forEach((function(e){e(u)})),n||c(0),u};function t(e){e.parent.classList.add("bespoke-marp-parent"),e.slides.map(e=>e.classList.add("bespoke-marp-slide")),e.on("activate",t=>{e.slides.map(e=>e.classList.remove("bespoke-marp-active")),t.slide.classList.add("bespoke-marp-active")})}function n(e=2e3){return t=>{let n;function r(){n&&clearTimeout(n),n=setTimeout(()=>{t.parent.classList.add("bespoke-marp-inactive")},e),t.parent.classList.remove("bespoke-marp-inactive")}document.addEventListener("mousedown",r),document.addEventListener("mousemove",r),document.addEventListener("touchend",r),setTimeout(r,0)}}const r=["AUDIO","BUTTON","INPUT","SELECT","TEXTAREA","VIDEO"];function s(e){e.parent.addEventListener("keydown",e=>{if(!e.target)return;const t=e.target;(r.includes(t.nodeName)||"true"===t.contentEditable)&&e.stopPropagation()})}function a(e){window.addEventListener("load",()=>{for(const t of e.slides){const e=t.querySelector("[data-marp-fitting]")?"":"hideable";t.setAttribute("data-bespoke-marp-load",e)}})}function o(e){let t=0,n=0;Object.defineProperty(e,"fragments",{enumerable:!0,value:e.slides.map(e=>[null,...e.querySelectorAll("[data-marpit-fragment]")])});const r=r=>void 0!==e.fragments[t][n+r],s=(r,s)=>{t=r,n=s,e.fragments.forEach((e,t)=>{e.forEach((e,n)=>{if(null==e)return;const a=t<r||t===r&&n<=s;e.setAttribute("data-bespoke-marp-fragment",a?"active":"inactive"),t===r&&n===s?e.setAttribute("data-bespoke-marp-current-fragment","current"):e.removeAttribute("data-bespoke-marp-current-fragment")})}),e.fragmentIndex=s;const a={slide:e.slides[r],index:r,fragments:e.fragments[r],fragmentIndex:s};e.fire("fragment",a)};e.on("next",()=>{if(r(1))return s(t,n+1),!1;const a=t+1;e.fragments[a]&&s(a,0)}),e.on("prev",()=>{if(r(-1))return s(t,n-1),!1;const a=t-1;e.fragments[a]&&s(a,e.fragments[a].length-1)}),e.on("slide",({index:t,fragment:n})=>{let r=0;if(void 0!==n){const s=e.fragments[t];if(s){const{length:e}=s;r=-1===n?e-1:Math.min(Math.max(n,0),e-1)}}s(t,r)}),s(0,0)}var i,l=function(e,t){return e(t={exports:{}},t.exports),t.exports}((function(e){ +/*! + * screenfull + * v5.0.2 - 2020-02-13 + * (c) Sindre Sorhus; MIT License + */ +!function(){var t="undefined"!=typeof window&&void 0!==window.document?window.document:{},n=e.exports,r=function(){for(var e,n=[["requestFullscreen","exitFullscreen","fullscreenElement","fullscreenEnabled","fullscreenchange","fullscreenerror"],["webkitRequestFullscreen","webkitExitFullscreen","webkitFullscreenElement","webkitFullscreenEnabled","webkitfullscreenchange","webkitfullscreenerror"],["webkitRequestFullScreen","webkitCancelFullScreen","webkitCurrentFullScreenElement","webkitCancelFullScreen","webkitfullscreenchange","webkitfullscreenerror"],["mozRequestFullScreen","mozCancelFullScreen","mozFullScreenElement","mozFullScreenEnabled","mozfullscreenchange","mozfullscreenerror"],["msRequestFullscreen","msExitFullscreen","msFullscreenElement","msFullscreenEnabled","MSFullscreenChange","MSFullscreenError"]],r=0,s=n.length,a={};r<s;r++)if((e=n[r])&&e[1]in t){for(r=0;r<e.length;r++)a[n[0][r]]=e[r];return a}return!1}(),s={change:r.fullscreenchange,error:r.fullscreenerror},a={request:function(e){return new Promise(function(n,s){var a=function(){this.off("change",a),n()}.bind(this);this.on("change",a);var o=(e=e||t.documentElement)[r.requestFullscreen]();o instanceof Promise&&o.then(a).catch(s)}.bind(this))},exit:function(){return new Promise(function(e,n){if(this.isFullscreen){var s=function(){this.off("change",s),e()}.bind(this);this.on("change",s);var a=t[r.exitFullscreen]();a instanceof Promise&&a.then(s).catch(n)}else e()}.bind(this))},toggle:function(e){return this.isFullscreen?this.exit():this.request(e)},onchange:function(e){this.on("change",e)},onerror:function(e){this.on("error",e)},on:function(e,n){var r=s[e];r&&t.addEventListener(r,n,!1)},off:function(e,n){var r=s[e];r&&t.removeEventListener(r,n,!1)},raw:r};r?(Object.defineProperties(a,{isFullscreen:{get:function(){return Boolean(t[r.fullscreenElement])}},element:{enumerable:!0,get:function(){return t[r.fullscreenElement]}},isEnabled:{enumerable:!0,get:function(){return Boolean(t[r.fullscreenEnabled])}}}),n?e.exports=a:window.screenfull=a):n?e.exports={isEnabled:!1}:window.screenfull={isEnabled:!1}}()}));l.isEnabled;function c(e){e.fullscreen=()=>{l.isEnabled&&l.toggle(document.body)},document.addEventListener("keydown",t=>{70!==t.which&&122!==t.which||t.altKey||t.ctrlKey||t.metaKey||!l.isEnabled||(e.fullscreen(),t.preventDefault())})}function d(e={}){const t=Object.assign({interval:200},e);return e=>{document.addEventListener("keydown",t=>{(32===t.which&&t.shiftKey||33===t.which||37===t.which||38===t.which)&&e.prev(),(32===t.which&&!t.shiftKey||34===t.which||39===t.which||40===t.which)&&e.next(),35===t.which&&e.slide(e.slides.length-1,{fragment:-1}),36===t.which&&e.slide(0)});let n,r,s=0;e.parent.addEventListener("wheel",a=>{let o=!1;const l=(e,t)=>{e&&(o=o||function(e,t){return function(e,t){const n=t===i.X?"Width":"Height";return e["client"+n]<e["scroll"+n]}(e,t)&&function(e,t){const{overflow:n}=e,r=e["overflow"+t];return"auto"===n||"scroll"===n||"auto"===r||"scroll"===r}(getComputedStyle(e),t)}(e,t)),(null==e?void 0:e.parentElement)&&l(e.parentElement,t)};if(0!==a.deltaX&&l(a.target,i.X),0!==a.deltaY&&l(a.target,i.Y),o)return;a.preventDefault(),r&&clearTimeout(r),r=setTimeout(()=>{n=0},t.interval);const c=Date.now()-s<t.interval,d=Math.sqrt(Math.pow(a.deltaX,2)+Math.pow(a.deltaY,2)),u=d<=n;if(n=d,c||u)return;let f;(a.deltaX>0||a.deltaY>0)&&(f="next"),(a.deltaX<0||a.deltaY<0)&&(f="prev"),f&&(e[f](),s=Date.now())})}}!function(e){e.X="X",e.Y="Y"}(i||(i={}));const u=(...e)=>history.replaceState(...e);var f;!function(e){e.Normal="",e.Presenter="presenter",e.Next="next"}(f||(f={}));const p=(e,{protocol:t,host:n,pathname:r,hash:s}=location)=>{const a=e.toString();return`${t}//${n}${r}${a?"?":""}${a}${s}`},m=()=>{switch(document.body.getAttribute("data-bespoke-view")){case f.Normal:return f.Normal;case f.Presenter:return f.Presenter;case f.Next:return f.Next;default:throw new Error("View mode is not assigned.")}},h=e=>new URLSearchParams(location.search).get(e),g=(e,t={})=>{const n=Object.assign({location:location,setter:u},t),r=new URLSearchParams(n.location.search);for(const t of Object.keys(e)){const n=e[t];"string"==typeof n?r.set(t,n):r.delete(t)}try{n.setter(null,document.title,p(r,n.location))}catch(e){console.error(e)}},b={available:(()=>{try{return localStorage.setItem("bespoke-marp","bespoke-marp"),localStorage.removeItem("bespoke-marp"),!0}catch(e){return console.warn("Warning: Using localStorage is restricted in the current host so some features may not work."),!1}})(),get:e=>{try{return localStorage.getItem(e)}catch(e){return null}},set:(e,t)=>{try{return localStorage.setItem(e,t),!0}catch(e){return!1}},remove:e=>{try{return localStorage.removeItem(e),!0}catch(e){return!1}}};function v(e=".bespoke-marp-osc"){const t=document.querySelector(e);if(!t)return()=>{};const n=(e,n)=>{t.querySelectorAll(`[data-bespoke-marp-osc=${JSON.stringify(e)}]`).forEach(n)};return l.isEnabled||n("fullscreen",e=>e.style.display="none"),b.available||n("presenter",e=>{e.disabled=!0,e.title="Presenter view is disabled due to restricted localStorage."}),e=>{t.addEventListener("click",t=>{if(t.target instanceof HTMLElement){const{bespokeMarpOsc:n}=t.target.dataset;switch(n&&t.target.blur(),n){case"next":e.next();break;case"prev":e.prev();break;case"fullscreen":"function"==typeof e.fullscreen&&l.isEnabled&&e.fullscreen();break;case"presenter":e.openPresenterView()}}}),e.parent.appendChild(t),e.on("activate",({index:t})=>{n("page",n=>n.textContent=`Page ${t+1} of ${e.slides.length}`)}),e.on("fragment",({index:t,fragments:r,fragmentIndex:s})=>{n("prev",e=>e.disabled=0===t&&0===s),n("next",n=>n.disabled=t===e.slides.length-1&&s===r.length-1)}),l.isEnabled&&l.onchange(()=>n("fullscreen",e=>e.classList.toggle("exit",l.isEnabled&&l.isFullscreen)))}}function w(){const e=Math.max(Math.floor(.85*window.innerWidth),640),t=Math.max(Math.floor(.85*window.innerHeight),360);return window.open(this.presenterUrl,"bespoke-marp-presenter-"+this.syncKey,`width=${e},height=${t},menubar=no,toolbar=no`)}function y(){const e=new URLSearchParams(location.search);return e.set("view","presenter"),e.set("sync",this.syncKey),p(e)}var x=["area","base","br","col","command","embed","hr","img","input","keygen","link","meta","param","source","track","wbr"];let E=e=>String(e).replace(/[&<>"']/g,e=>`&${k[e]};`),k={"&":"amp","<":"lt",">":"gt",'"':"quot","'":"apos"},S="dangerouslySetInnerHTML",L={className:"class",htmlFor:"for"},I={};function P(e,t){let n=[],r="";t=t||{};for(let e=arguments.length;e-- >2;)n.push(arguments[e]);if("function"==typeof e)return t.children=n.reverse(),e(t);if(e){if(r+="<"+e,t)for(let e in t)!1!==t[e]&&null!=t[e]&&e!==S&&(r+=` ${L[e]?L[e]:E(e)}="${E(t[e])}"`);r+=">"}if(-1===x.indexOf(e)){if(t[S])r+=t[S].__html;else for(;n.length;){let e=n.pop();if(e)if(e.pop)for(let t=e.length;t--;)n.push(e[t]);else r+=!0===I[e]?e:E(e)}r+=e?`</${e}>`:""}return I[r]=!0,r}const M=({children:e})=>P(null,null,...e),N="bespoke-marp-presenter-container",F="bespoke-marp-presenter-next",O="bespoke-marp-presenter-next-container",T="bespoke-marp-presenter-note-container",q="bespoke-marp-presenter-info-container",C="bespoke-marp-presenter-info-page",$="bespoke-marp-presenter-info-page-text",j="bespoke-marp-presenter-info-page-prev",A="bespoke-marp-presenter-info-page-next",K="bespoke-marp-presenter-info-time",R="bespoke-marp-presenter-info-timer";function U(e){const{title:t}=document;document.title="[Presenter view]"+(t?" - "+t:"");const n={},r=e=>(n[e]=n[e]||document.querySelector("."+e),n[e]);document.body.appendChild((e=>{const t=document.createElement("div");return t.className=N,t.appendChild(e),t.insertAdjacentHTML("beforeend",P(M,null,P("div",{class:O},P("iframe",{class:F,src:"?view=next"})),P("div",{class:T}),P("div",{class:q},P("div",{class:C},P("button",{class:j,tabindex:"-1",title:"Previous"},"Previous"),P("span",{class:$}),P("button",{class:A,tabindex:"-1",title:"Next"},"Next")),P("time",{class:K,title:"Current time"}),P("div",{class:R})))),t})(e.parent)),(e=>{r(O).addEventListener("click",()=>e.next());const t=r(F),n=(s=t,(e,t)=>s.contentWindow.postMessage(`navigate:${e},${t}`,"null"===window.origin?"*":window.origin));var s;t.addEventListener("load",()=>{r(O).classList.add("active"),n(e.slide(),e.fragmentIndex),e.on("fragment",({index:e,fragmentIndex:t})=>n(e,t))});const a=document.querySelectorAll(".bespoke-marp-note");a.forEach(e=>{e.addEventListener("keydown",e=>e.stopPropagation()),r(T).appendChild(e)}),e.on("activate",()=>a.forEach(t=>t.classList.toggle("active",t.dataset.index==e.slide()))),e.on("activate",({index:t})=>{r($).textContent=`${t+1} / ${e.slides.length}`});const o=r(j),i=r(A);o.addEventListener("click",()=>{o.blur(),e.prev()}),i.addEventListener("click",()=>{i.blur(),e.next()}),e.on("fragment",({index:t,fragments:n,fragmentIndex:r})=>{o.disabled=0===t&&0===r,i.disabled=t===e.slides.length-1&&r===n.length-1});const l=()=>r(K).textContent=(new Date).toLocaleTimeString();l(),setInterval(l,250)})(e)}function V(e){const t=m();return t===f.Next&&e.appendChild(document.createElement("span")),e=>{t===f.Normal&&function(e){if(!(e=>e.syncKey&&"string"==typeof e.syncKey)(e))throw new Error("The current instance of Bespoke.js is invalid for Marp bespoke presenter plugin.");Object.defineProperties(e,{openPresenterView:{enumerable:!0,value:w},presenterUrl:{enumerable:!0,get:y}}),b.available&&document.addEventListener("keydown",t=>{80!==t.which||t.altKey||t.ctrlKey||t.metaKey||(t.preventDefault(),e.openPresenterView())})}(e),t===f.Presenter&&U(e),t===f.Next&&function(e){const t=t=>{if(t.origin!==window.origin)return;const[n,r]=t.data.split(":");if("navigate"===n){const[t,n]=r.split(",");e.slide(Number.parseInt(t,10),{fragment:Number.parseInt(n,10)}),e.next()}};window.addEventListener("message",t),e.on("destroy",()=>window.removeEventListener("message",t))}(e)}}function X(e){e.on("activate",t=>{document.querySelectorAll(".bespoke-progress-bar").forEach(n=>{n.style.flexBasis=100*t.index/(e.slides.length-1)+"%"})})}const D=e=>{const t=Number.parseInt(e,10);return Number.isNaN(t)?null:t};function Y(e={}){const t=Object.assign({history:!0},e);return e=>{let n=!0;const r=e=>{const t=n;try{return n=!0,e()}finally{n=t}},s=(t={fragment:!0})=>{((t,n)=>{const{fragments:r,slides:s}=e,a=Math.max(0,Math.min(t,s.length-1)),o=Math.max(0,Math.min(n||0,r[a].length-1));a===e.slide()&&o===e.fragmentIndex||e.slide(a,{fragment:o})})((D(location.hash.slice(1))||1)-1,t.fragment?D(h("f")||""):null)};e.on("fragment",({index:e,fragmentIndex:r})=>{n||g({f:0===r||r.toString()},{location:Object.assign(Object.assign({},location),{hash:"#"+(e+1)}),setter:(...e)=>t.history?history.pushState(...e):history.replaceState(...e)})}),setTimeout(()=>{s(),window.addEventListener("hashchange",()=>r(()=>{s({fragment:!1}),g({f:void 0})})),window.addEventListener("popstate",()=>{n||r(()=>s())}),n=!1},0)}}function B(e={}){const t=e.key||((e=21)=>{let t="",n=crypto.getRandomValues(new Uint8Array(e));for(;e--;){let r=63&n[e];t+=r<36?r.toString(36):r<62?(r-26).toString(36).toUpperCase():r<63?"_":"-"}return t})(),n="bespoke-marp-sync-"+t,r=()=>{const e=b.get(n);return e?JSON.parse(e):Object.create(null)},s=e=>{const t=r(),s=Object.assign(Object.assign({},t),e(t));return b.set(n,JSON.stringify(s)),s};return s(e=>({reference:(e.reference||0)+1})),e=>{Object.defineProperty(e,"syncKey",{value:t,enumerable:!0});let a=!0;setTimeout(()=>{e.on("fragment",e=>{a&&s(()=>({index:e.index,fragmentIndex:e.fragmentIndex}))})},0),window.addEventListener("storage",t=>{if(t.key===n&&t.oldValue&&t.newValue){const n=JSON.parse(t.oldValue),r=JSON.parse(t.newValue);if(n.index!==r.index||n.fragmentIndex!==r.fragmentIndex)try{a=!1,e.slide(r.index,{fragment:r.fragmentIndex})}finally{a=!0}}}),e.on("destroy",()=>{const{reference:e}=r();void 0===e||e<=1?b.remove(n):s(()=>({reference:e-1}))})}}function z(e={}){const t=Object.assign({slope:Math.tan(-35*Math.PI/180),swipeThreshold:30},e);return e=>{let n;const r=e.parent,s=e=>{const t=r.getBoundingClientRect();return{x:e.pageX-(t.left+t.right)/2,y:e.pageY-(t.top+t.bottom)/2}};r.addEventListener("touchstart",e=>{n=1===e.touches.length?s(e.touches[0]):void 0},{passive:!0}),r.addEventListener("touchmove",e=>{if(n)if(1===e.touches.length){e.preventDefault();const t=s(e.touches[0]),r=t.x-n.x,a=t.y-n.y;n.delta=Math.sqrt(Math.pow(Math.abs(r),2)+Math.pow(Math.abs(a),2)),n.radian=Math.atan2(r,a)}else n=void 0}),r.addEventListener("touchend",r=>{if(n){if(n.delta&&n.delta>=t.swipeThreshold){let s=n.radian-t.slope;s=(s+Math.PI)%(2*Math.PI)-Math.PI,e[s<0?"next":"prev"](),r.stopPropagation()}n=void 0}},{passive:!0})}}const H=[f.Normal,f.Presenter,f.Next];!function(r=document.getElementById("p")){document.body.setAttribute("data-bespoke-view",(()=>{switch(h("view")){case"next":return f.Next;case"presenter":return f.Presenter;default:return f.Normal}})());const i=(e=>{const t=h(e);return g({[e]:void 0}),t})("sync")||void 0,l=!1,u=!0,p=e(r,((...e)=>{const t=H.findIndex(e=>m()===e);if(t<0)throw new Error("Invalid view");return e.map(([e,n])=>e[t]&&n).filter(e=>e)})([[u,u,l],B({key:i})],[[u,u,u],V(r)],[[u,u,l],s],[[u,u,u],t],[[u,l,l],n()],[[u,u,u],a],[[u,u,u],Y({history:!1})],[[u,u,l],d()],[[u,u,l],c],[[u,l,l],X],[[u,u,l],z()],[[u,l,l],v()],[[u,u,u],o]));window.addEventListener("beforeunload",()=>g({sync:p.syncKey})),window.addEventListener("unload",()=>p.destroy())}()}(); +</script></body></html> \ No newline at end of file
--- /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 +--- + +# <!--fit--> 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 における遷移記述はそのまま状態遷移記述にすることができる。 + + +<center><img src="./pic/input-outputDataSegment.svg" alt="" width="100%" height="100%" ></center> + +--- + +# 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本ずつ持ってしまった場合、誰も食事することは出来ない。この状態をデッドロックとする。 +<center><img src="./pic/dpp_image.svg" alt="" width="48%" height="48%" ></center> + +--- + +# DPP + +- 状態の構成要素は次の6つからなる。 +`Pickup Right fork` ` Pickup Left fork` `eating` ` Put Right fork` `Put Left fork` ` Thinking ` + +<right><img src="./pic/dpp_image.svg" alt="" width="55%" height="55%" ></right> + +--- + + +# 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 を指定してコンパイルすることで実現できる。 + + + + +