Mercurial > hg > Papers > 2020 > ikkun-sigos
changeset 9:9a18a3f1f7ed
fix
| author | ikkun <ikkun@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 05 May 2020 12:49:16 +0900 |
| parents | 465226b85d99 |
| children | 7cbb0c656be3 |
| files | etc/xv6model.mm paper/Makefile paper/ikkun-sigos.pdf paper/ikkun-sigos.tex |
| diffstat | 4 files changed, 24 insertions(+), 22 deletions(-) [+] |
line wrap: on
line diff
--- a/etc/xv6model.mm Mon May 04 03:36:56 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -<map version="1.0.1"> -<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> -<node CREATED="1587962519361" ID="ID_307407658" MODIFIED="1587966139651" TEXT="xv6の構成要素の継続の分析"> -<node CREATED="1587966142790" ID="ID_24786061" MODIFIED="1587966142790" POSITION="right" TEXT=""/> -<node CREATED="1587966144154" ID="ID_1416207432" MODIFIED="1587966148400" POSITION="left" TEXT="目次"> -<node CREATED="1587966149328" ID="ID_285261624" MODIFIED="1587966171170" TEXT="OSの信頼性"/> -<node CREATED="1587966171873" ID="ID_49224039" MODIFIED="1587966179381" TEXT="XV6 OSの概要"/> -<node CREATED="1587966179913" ID="ID_1735703718" MODIFIED="1587966190536" TEXT="XV6のファイルシステムの分析"/> -<node CREATED="1587966191026" ID="ID_710119512" MODIFIED="1587966196503" TEXT="CbCの導入"/> -<node CREATED="1587966196869" ID="ID_754369000" MODIFIED="1587966199587" TEXT="まとめ"/> -</node> -</node> -</map>
--- a/paper/Makefile Mon May 04 03:36:56 2020 +0900 +++ b/paper/Makefile Tue May 05 12:49:16 2020 +0900 @@ -1,4 +1,4 @@ -TARGET = anatofuz-sigos +TARGET = ikkun-sigos LATEX = platex BIBTEX = pbibtex
--- a/paper/ikkun-sigos.tex Mon May 04 03:36:56 2020 +0900 +++ b/paper/ikkun-sigos.tex Tue May 05 12:49:16 2020 +0900 @@ -11,7 +11,7 @@ -\usepackage[dvips]{graphicx} +\usepackage[dvips,dvipdfmx]{graphicx} \usepackage{latexsym} \def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline} @@ -93,14 +93,29 @@ \section{DPP} 検証用のサンプルプログラムとしてDining Philosohers Ploblem を用いる。これは資源共有問題の１つで、次のような内容である。 - 5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。食べるには2本のフォークを使わないと食べれないが、フォークは円卓に5本しかなく、また各々の間に一本ずつ置かれている。哲学者は思索と食事を交互に繰り返そうとし、食事するにはフォークを2本取る必要があるが取れなかった場合はフォークが空くのを待つ。 - 各哲学者を１つのプロセスとすると、この問題は後このプロセスが並列に動くことになる。 - + 5人の哲学者が円卓についており、各々スパゲッティーの皿が目の前に用意されている。スパゲッィーはとても絡まっているので食べるには2本のフォークを使わないと食べれない。しかしフォークはお皿の間に一本ずつおいてあるので、円卓にフォークが5本しか用意されていない。\figref{fig}哲学者は思索と食事を交互に繰り返している。空腹を覚えると、左右のオークを手に取ろうと試み、2本のフォークを取ることに成功するとしばし食事をし、しばらくするとフォークを置いて思索に戻る。隣の哲学者が食事中でフォークが手に取れない場合は、そのままフォークが開くのを待つ。 + 各哲学者を１つのプロセスとすると、この問題では5個のプロセスが並列に動くことになり、全員が1本ずつフォークを持って場合はデッドロックしていることになる。プロセスの並列実行はスケジューラによって制御することで実現する。 +\begin{figure}[tb] + \begin{center} + \includegraphics[width=70mm]{./pic/dpp_image.pdf} + \end{center} + \caption{Dining Philosohers Ploblem} + \label{DPP_imag} +\end{figure} + + \section{Gears OS} - 本研究室で開発しているGeasOS は CbC で記述されており、プログラムの処理が記述された code gear と変数などのデータを格納する data gear によって構成され、Code Gear 間の遷移にはgoto を用いて遷移する。このため CbC による記述は状態遷移記述になる性質がある。 -また goto による遷移は大域変数を持たない遷移であるため、遷移前の処理に囚われず遷移先を自由に変更する事が可能である。 -Gears OS はこの性質を利用して処理の間にメタレベルの計算である meta Code Gear またmeta Code Gear を入れることができる - メタ計算である meta Code Gear、meta Data Gaer と対比して、Coed Gear、Data Gaer をインターフェースといい、OSとしての重要な +Continuation based C (以下CbC) という言語を用いて Gears OS は拡張性と信頼性を両立させることを目的として本研究室で開発されている。CbC はプログラムの処理が記述された code gear と変数などのデータを格納する data gear によって構成される。CbC におけるプログラム間の遷移には goto を用いて遷移する。goto は関数呼び出しのような環境変数を持たず指定された行き先に引数だけを持ち遷移する。これを軽量継続と言い、呼び出し元に戻らない遷移であるため CbC における遷移記述はそのまま状態遷移記述にすることができる。 +また 遷移前の処理に囚われず、遷移先を自由に変更する事が可能であるため、goto 先を変更するだけで処理の間にメタレベルの計算を挿入する事が可能である。 + +\begin{figure}[tb] + \begin{center} + \includegraphics[width=70mm]{./pic/meta_Gaer.pdf} + \end{center} + \caption{Gears OS のメタ計算} + \label{meta_Gear} +\end{figure} + \section{GearsOSを用いたモデル検査}