Mercurial > hg > Papers > 2020 > tobaru-master

--- a/paper/Paging.tex	Fri Feb 07 16:53:09 2020 +0900
+++ b/paper/Paging.tex	Fri Feb 07 20:06:13 2020 +0900
@@ -8,7 +8,11 @@
 ANSI-C で書かれている Xv6 を CbC に書き直し、それを元に Gears OS を実装していく。

 \section{Paging}
-  メモリ管理の手法に、Paging がある。Paging ではメモリを Page と呼ばれる固定長の単位に分割し、メモリとスワップ領域で Page を入れ替えて管理を行う。
+実メモリをそのまま使うと様々な問題が生じる。
+ユーザープログラム側で空いているメモリ番地を探す必要がでてきたり、メモリ間にデータとして扱うには小さな隙間ができるフラグメンテーションが起こる。
+  メモリ管理の手法に、Paging がある。
+Paging ではメモリを Page と呼ばれる固定長の単位に分割し、メモリとスワップ領域で Page を入れ替えて管理を行う。
+Paging を扱うことでブロック単位で管理することによりフラグメンテーションが解消でき、MMUが実メモリを管理することによってプログラム側で空いているメモリを探す必要がなくなる。


 図 \ref{fig:MemoryConstitution} で Xv6の仮想メモリと実メモリについて説明する。
@@ -25,15 +29,19 @@
 \end{figure}


-\section{User Space で Paging をする利点}
- Context に必要な Page Tbale を提供する Interface と User Space からアクセスする API が必要である。
-Page Table に相当するデータを Input Data Gear で受け取って変更した後、Context にあるメモリコントロールを担当する Meta Data Gear に goto で遷移してアクセスする。 Meta Computation レベルで処理することで Use Spaceでも Page Table を操作することができる。
-Meta Computation に戻る際に、Page Table Entry のバリデーションをチェックして反映することで、他のプロセスから Page Table を書き換えられることを防ぐ。また、サンドボックスにしておいて、他のプロセスが書き換えられた時にエクセプションを飛ばすようにすることで信頼性の保証を行う。
+\section{CbCXv6 での Paging}
+ Context に必要な Page Table を提供する Interface が必要である。
+% と User Space からアクセスする API が必要である。
+Page Table に相当するデータを Input Data Gear で受け取って変更した後、Context にあるメモリコントロールを担当する Meta Data Gear に goto で遷移してアクセスする。
+% Meta Computation レベルで処理することで Use Spaceでも Page Table を操作することができる。
+メタレベルで処理することで カーネル側の処理である Page Table を操作することができる。
+% Meta Computation に戻る際に、
+Page Table Entry のバリデーションをチェックして反映することで、他のプロセスから Page Table を書き換えられることを防ぐ。また、サンドボックスにしておいて、他のプロセスが書き換えられた時にエクセプションを飛ばすようにすることで信頼性の保証を行う。


 \section{Paging の書き換え}
  Xv6 では実メモリ(Physical memory) から仮想メモリ(Virtual memory)の変換を vm.c で行なっている。
 vm.c を CbC で書き換えていく。
+次のチャプターで実際の書き換えについて説明する。


-
--- a/paper/Xv6.tex	Fri Feb 07 16:53:09 2020 +0900
+++ b/paper/Xv6.tex	Fri Feb 07 20:06:13 2020 +0900
@@ -49,3 +49,4 @@
 \section{Xv6-rpi}
 Xv6 は Arm のバイナリを出力するので、シングルボードコンピュータである Raspberry Pi や携帯電話など様々なハードウェアで動かすことができる。
 実際に Raspberry Pi 上で動かすために xv6-rpi という OS を用意して動作しているか検証中である。
+xv6-rpi は CbCXv6 と別で用意している。
--- a/paper/master_paper.aux	Fri Feb 07 16:53:09 2020 +0900
+++ b/paper/master_paper.aux	Fri Feb 07 20:06:13 2020 +0900
@@ -27,7 +27,7 @@
 \@writefile{lot}{\addvspace {10\p@ }}
 \@writefile{toc}{\contentsline {section}{\numberline {4.1}Xv6 を元にした Gears OS の実装}{10}\protected@file@percent }
 \@writefile{toc}{\contentsline {section}{\numberline {4.2}Paging}{10}\protected@file@percent }
-\@writefile{toc}{\contentsline {section}{\numberline {4.3}User Space で Paging をする利点}{10}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {4.3}CbCXv6 での Paging}{10}\protected@file@percent }
 \@writefile{toc}{\contentsline {section}{\numberline {4.4}Paging の書き換え}{11}\protected@file@percent }
 \@writefile{lof}{\contentsline {figure}{\numberline {4.1}{\ignorespaces On the left, xv6’s kernel address space. RWX refer to PTE read, write, and execute permissions. On the right, the RISC-V physical address space that xv6 expects to see. Russ Cox(2014) xv6 a simple, Unix-like teaching operating system (Frans Kaashoek, Robert Morris)}}{12}\protected@file@percent }
 \newlabel{fig:MemoryConstitution}{{4.1}{12}}
--- a/paper/master_paper.log	Fri Feb 07 16:53:09 2020 +0900
+++ b/paper/master_paper.log	Fri Feb 07 20:06:13 2020 +0900
@@ -1,4 +1,4 @@
-This is e-pTeX, Version 3.14159265-p3.8.2-190131-2.6 (utf8.euc) (TeX Live 2019) (preloaded format=platex 2020.1.16)  7 FEB 2020 16:46
+This is e-pTeX, Version 3.14159265-p3.8.2-190131-2.6 (utf8.euc) (TeX Live 2019) (preloaded format=platex 2020.1.16)  7 FEB 2020 20:05
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
@@ -389,9 +389,9 @@
 第 4 章(10ページ)
 File: ./fig/MemoryConstitution.pdf Graphic file (type pdf)
 <./fig/MemoryConstitution.pdf>
-) (./cbc_interface.tex [10
+[10

-] [11] [12]
+]) (./cbc_interface.tex [11] [12]
 第 5 章(13ページ)
 (./src/vm.h [13

@@ -489,4 +489,4 @@
  107 hyphenation exceptions out of 8191
  33i,11n,36p,410b,1835s stack positions out of 5000i,500n,10000p,200000b,80000s

-Output written on master_paper.dvi (56 pages, 242880 bytes).
+Output written on master_paper.dvi (56 pages, 243800 bytes).
Binary file paper/master_paper.pdf has changed
Binary file paper/master_paper.synctex.gz has changed
--- a/paper/master_paper.toc	Fri Feb 07 16:53:09 2020 +0900
+++ b/paper/master_paper.toc	Fri Feb 07 20:06:13 2020 +0900
@@ -10,7 +10,7 @@
 \contentsline {chapter}{\numberline {第4章}CbCXv6 での Paging}{10}%
 \contentsline {section}{\numberline {4.1}Xv6 を元にした Gears OS の実装}{10}%
 \contentsline {section}{\numberline {4.2}Paging}{10}%
-\contentsline {section}{\numberline {4.3}User Space で Paging をする利点}{10}%
+\contentsline {section}{\numberline {4.3}CbCXv6 での Paging}{10}%
 \contentsline {section}{\numberline {4.4}Paging の書き換え}{11}%
 \contentsline {chapter}{\numberline {第5章}CbC インターフェース}{13}%
 \contentsline {section}{\numberline {5.1}インターフェースの定義}{13}%
--- a/slide/CbCXv6.html	Fri Feb 07 16:53:09 2020 +0900
+++ b/slide/CbCXv6.html	Fri Feb 07 20:06:13 2020 +0900
@@ -38,7 +38,7 @@
 <li>並列信頼研</li>
 <li>桃原 優</li>
 </ul><hr><h1 id="目次0" style=""><a class="anchor hidden-xs" href="#目次0" title="目次0"><span class="octicon octicon-link"></span></a>目次</h1><ol>
-<li><strong>OS の信頼性の保障</strong></li>
+<li><strong>OS の信頼性の保証</strong></li>
 <li>CbC による Gears OS の開発</li>
 <li>Xv6</li>
 <li>CbCXv6 での Paging</li>
@@ -86,17 +86,13 @@
 </ul>
 </li>
 </ul><hr><h1 id="Continuation-based-C" style=""><a class="anchor hidden-xs" href="#Continuation-based-C" title="Continuation-based-C"><span class="octicon octicon-link"></span></a>Continuation based C</h1><ul>
-<li>
-<p>ノーマルレベルとメタレベルの処理を同じ言語で行えるようにした言語(以下CbC)</p>
-</li>
-<li>
-<p>Code Gear</p>
+<li>ノーマルレベルとメタレベルの処理を同じ言語で行えるようにした言語(以下CbC)</li>
+<li>Code Gear
 <ul>
 <li>基本的な処理の単位</li>
 </ul>
 </li>
-<li>
-<p>Data Gear</p>
+<li>Data Gear
 <ul>
 <li>データの単位</li>
 </ul>
@@ -136,7 +132,7 @@
 </ul><hr><h1 id="Geas-OS" style=""><a class="anchor hidden-xs" href="#Geas-OS" title="Geas-OS"><span class="octicon octicon-link"></span></a>Geas OS</h1><ul>
 <li>CbC を使って信頼性の保証と拡張性を持たせる Gears OS の開発を行なっている</li>
 <li>Xv6 という OS を参考に書き換えをしている</li>
-</ul><hr><h1 id="メモリ管理" style=""><a class="anchor hidden-xs" href="#メモリ管理" title="メモリ管理"><span class="octicon octicon-link"></span></a>メモリ管理</h1><ul>
+</ul><hr><h1 id="メモリ管理0" style=""><a class="anchor hidden-xs" href="#メモリ管理0" title="メモリ管理0"><span class="octicon octicon-link"></span></a>メモリ管理</h1><ul>
 <li>OS の信頼性の1つであるメモリ管理部分を CbC で書き換える
 <ul>
 <li>Page のバリデーションチェック</li>
@@ -144,20 +140,137 @@
 </ul>
 </li>
 </ul><hr><h1 id="インターフェース" style=""><a class="anchor hidden-xs" href="#インターフェース" title="インターフェース"><span class="octicon octicon-link"></span></a>インターフェース</h1><ul>
-<li>
-<p>書き換えを防ぐために見える Data Gear に違いが生じる</p>
-</li>
-<li>
-<p>-&gt; Gears OS のノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入</p>
-</li>
-<li>
-<p>機能の入れ替えによる他のメリット</p>
+<li>書き換えを防ぐために見える Data Gear に違いが生じる</li>
+<li>-&gt; Gears OS のノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入</li>
+<li>機能の入れ替えによる他のメリット
 <ul>
+<li>煩雑な記述の解消</li>
 <li>機能の入れ替え</li>
 <li>Agda による証明</li>
 </ul>
 </li>
-</ul></div>
+</ul><hr><h1 id="目次0" style=""><a class="anchor hidden-xs" href="#目次0" title="目次0"><span class="octicon octicon-link"></span></a>目次</h1><ol>
+<li>OS の信頼性の保証</li>
+<li><strong>CbC による Gears OS の開発</strong></li>
+<li>Xv6</li>
+<li>CbCXv6 での Paging</li>
+<li>CbC インターフェース</li>
+<li>評価</li>
+<li>まとめ</li>
+</ol><hr><h1 id="CbC-による-Gears-OS-の開発" style=""><a class="anchor hidden-xs" href="#CbC-による-Gears-OS-の開発" title="CbC-による-Gears-OS-の開発"><span class="octicon octicon-link"></span></a>CbC による Gears OS の開発</h1><ul>
+<li>a</li>
+</ul><hr><h1 id="Context" style=""><a class="anchor hidden-xs" href="#Context" title="Context"><span class="octicon octicon-link"></span></a>Context</h1><ul>
+<li>a</li>
+</ul><hr><h1 id="目次1" style=""><a class="anchor hidden-xs" href="#目次1" title="目次1"><span class="octicon octicon-link"></span></a>目次</h1><ol>
+<li>OS の信頼性の保証</li>
+<li>CbC による Gears OS の開発</li>
+<li><strong>Xv6</strong></li>
+<li>CbCXv6 での Paging</li>
+<li>CbC インターフェース</li>
+<li>評価</li>
+<li>まとめ</li>
+</ol><hr><h1 id="Xv60" style=""><a class="anchor hidden-xs" href="#Xv60" title="Xv60"><span class="octicon octicon-link"></span></a>Xv6</h1><ul>
+<li>MIT の講義用教材として作られたOS
+<ul>
+<li>企画課される前のCで書かれたUNIX V6 を書き換えた</li>
+<li>1万行程の軽量なOS</li>
+<li>Linuxだと数千万行</li>
+</ul>
+</li>
+<li>Xv6 を参考に CbC で書き直すことで Gears OS を実装する</li>
+</ul><hr><h1 id="カーネル空間" style=""><a class="anchor hidden-xs" href="#カーネル空間" title="カーネル空間"><span class="octicon octicon-link"></span></a>カーネル空間</h1><ul>
+<li>OS の中核となるプログラムで Meta Level に相当する</li>
+<li>Xv6 ではカーネルとユーザープログラムは分離されている</li>
+<li>ユーザープログラムはカーネルに直接アクセスできない。
+<ul>
+<li>書き換えやアクセスを防ぐため</li>
+<li>呼び出す場合は system call</li>
+</ul>
+</li>
+</ul><hr><h1 id="カーネルが提供するもの" style=""><a class="anchor hidden-xs" href="#カーネルが提供するもの" title="カーネルが提供するもの"><span class="octicon octicon-link"></span></a>カーネルが提供するもの</h1><ul>
+<li>プロセス管理</li>
+<li>メモリ管理</li>
+<li>ファイル管理
+<ul>
+<li>I/O, read, write</li>
+</ul>
+</li>
+</ul><hr><h1 id="カーネルの保護機構" style=""><a class="anchor hidden-xs" href="#カーネルの保護機構" title="カーネルの保護機構"><span class="octicon octicon-link"></span></a>カーネルの保護機構</h1><ul>
+<li>CPUのハードウェア保護機構を持っている</li>
+<li>ユーザー空間で実行されているプロセスが自身のメモリのみアクセスできるように保護</li>
+<li>system call
+<ul>
+<li>ハードウェアが一時的に特権レベルをあげ、カーネルのプログラムが実行される</li>
+</ul>
+</li>
+</ul><hr><h1 id="system-call0" style=""><a class="anchor hidden-xs" href="#system-call0" title="system-call0"><span class="octicon octicon-link"></span></a>system call</h1><ul>
+<li>system call 呼び出し</li>
+<li>トラップ の発生</li>
+<li>ユーザープログラムの中断</li>
+<li>処理がカーネルに切り替わる</li>
+</ul><hr><h1 id="system-call" style=""><a class="anchor hidden-xs" href="#system-call" title="system-call"><span class="octicon octicon-link"></span></a>system call</h1><ul>
+<li>ソースコード載せる</li>
+</ul><hr><h1 id="Xv6-rpi" style=""><a class="anchor hidden-xs" href="#Xv6-rpi" title="Xv6-rpi"><span class="octicon octicon-link"></span></a>Xv6-rpi</h1><ul>
+<li>Xv6 は　Arm のバイナリを出力するので様々なハードウェアで動かすことができる
+<ul>
+<li>Raspberry Pi</li>
+<li>携帯電話</li>
+</ul>
+</li>
+<li>実際にRaspberry Pi で動かすために xv6-rpi を用意して動作しているかコンソールで確認中
+<ul>
+<li>CbCxv6 とは別</li>
+</ul>
+</li>
+</ul><hr><h1 id="目次0" style=""><a class="anchor hidden-xs" href="#目次0" title="目次0"><span class="octicon octicon-link"></span></a>目次</h1><ol>
+<li>OS の信頼性の保証</li>
+<li>CbC による Gears OS の開発</li>
+<li>Xv6</li>
+<li><strong>CbCXv6 での Paging</strong></li>
+<li>CbC インターフェース</li>
+<li>評価</li>
+<li>まとめ</li>
+</ol><hr><h1 id="CbCXv6-での-Paging0" style=""><a class="anchor hidden-xs" href="#CbCXv6-での-Paging0" title="CbCXv6-での-Paging0"><span class="octicon octicon-link"></span></a>CbCXv6 での Paging</h1><ul>
+<li>OS の信頼性の1つであるメモリ管理部分の書き換えについて説明</li>
+</ul><hr><h1 id="実メモリの直接操作" style=""><a class="anchor hidden-xs" href="#実メモリの直接操作" title="実メモリの直接操作"><span class="octicon octicon-link"></span></a>実メモリの直接操作</h1><ul>
+<li>実メモリを直接扱うと様々な問題が生じる
+<ul>
+<li>ユーザープログラムで空いているメモリ番地を探す必要</li>
+<li>フラグメンテーションが起こる
+<ul>
+<li>メモリ間に扱うには小さな隙間ができる</li>
+</ul>
+</li>
+</ul>
+</li>
+</ul><hr><h1 id="Paging0" style=""><a class="anchor hidden-xs" href="#Paging0" title="Paging0"><span class="octicon octicon-link"></span></a>Paging</h1><ul>
+<li>メモリ管理の手法</li>
+<li>Page と呼ばれる固定長のブロックに分割して、メモリとスワップ領域で Page を入れ替えて管理</li>
+<li>仮想メモリとして扱うことでフラグメンテーションの解消と空き番地を探す必要がなくなる</li>
+</ul><hr><h1 id="Pagingの図" style=""><a class="anchor hidden-xs" href="#Pagingの図" title="Pagingの図"><span class="octicon octicon-link"></span></a>Pagingの図</h1><ul>
+<li>必要？</li>
+</ul><hr><h1 id="メタレベルでの-Paging-の操作" style=""><a class="anchor hidden-xs" href="#メタレベルでの-Paging-の操作" title="メタレベルでの-Paging-の操作"><span class="octicon octicon-link"></span></a>メタレベルでの Paging の操作</h1><ul>
+<li>Page Table に相当するデータを Input Data Gear で受け取って変更した後、Context にある Meta Data Gear に goto で遷移してアクセス</li>
+<li>メタレベルで処理することで本来カーネル側の処理である Page Table を操作できる</li>
+</ul><hr><h1 id="Paging-の信頼性" style=""><a class="anchor hidden-xs" href="#Paging-の信頼性" title="Paging-の信頼性"><span class="octicon octicon-link"></span></a>Paging の信頼性</h1><ul>
+<li>Input Data Gear に対しての Output Data Gear をバリデーションチェックすることで他のプロセスから書き換えられることを防ぐ</li>
+<li>サンドボックス
+<ul>
+<li>他のプロセスから書き換えられた時にエクセプションを飛ばす</li>
+</ul>
+</li>
+</ul><hr><h1 id="Paging-の書き換え" style=""><a class="anchor hidden-xs" href="#Paging-の書き換え" title="Paging-の書き換え"><span class="octicon octicon-link"></span></a>Paging の書き換え</h1><ul>
+<li>Xv6 では実メモリから仮想メモリの変換をvm.cで行なっている。</li>
+<li>次の章で書き換えについて説明する</li>
+</ul><hr><h1 id="目次" style=""><a class="anchor hidden-xs" href="#目次" title="目次"><span class="octicon octicon-link"></span></a>目次</h1><ol>
+<li>OS の信頼性の保証</li>
+<li>CbC による Gears OS の開発</li>
+<li>Xv6</li>
+<li>CbCXv6 での Paging**</li>
+<li><strong>CbC インターフェース</strong></li>
+<li>評価</li>
+<li>まとめ</li>
+</ol><hr></div>
     <div class="ui-toc dropup unselectable hidden-print" style="display:none;">
         <div class="pull-right dropdown">
             <a id="tocLabel" class="ui-toc-label btn btn-default" data-toggle="dropdown" href="#" role="button" aria-haspopup="true" aria-expanded="false" title="Table of content">
@@ -177,9 +290,29 @@
 <li><a href="#状態遷移モデル" title="状態遷移モデル">状態遷移モデル</a></li>
 <li><a href="#Agda-による検証" title="Agda による検証">Agda による検証</a></li>
 <li><a href="#Haure-Logic" title="Haure Logic">Haure Logic</a></li>
-<li class=""><a href="#Geas-OS" title="Geas OS">Geas OS</a></li>
-<li><a href="#メモリ管理" title="メモリ管理">メモリ管理</a></li>
+<li><a href="#Geas-OS" title="Geas OS">Geas OS</a></li>
+<li><a href="#メモリ管理0" title="メモリ管理">メモリ管理</a></li>
 <li><a href="#インターフェース" title="インターフェース">インターフェース</a></li>
+<li><a href="#目次0" title="目次">目次</a></li>
+<li><a href="#CbC-による-Gears-OS-の開発" title="CbC による Gears OS の開発">CbC による Gears OS の開発</a></li>
+<li><a href="#Context" title="Context">Context</a></li>
+<li><a href="#目次1" title="目次">目次</a></li>
+<li><a href="#Xv60" title="Xv6">Xv6</a></li>
+<li><a href="#カーネル空間" title="カーネル空間">カーネル空間</a></li>
+<li><a href="#カーネルが提供するもの" title="カーネルが提供するもの">カーネルが提供するもの</a></li>
+<li><a href="#カーネルの保護機構" title="カーネルの保護機構">カーネルの保護機構</a></li>
+<li><a href="#system-call0" title="system call">system call</a></li>
+<li><a href="#system-call" title="system call">system call</a></li>
+<li><a href="#Xv6-rpi" title="Xv6-rpi">Xv6-rpi</a></li>
+<li><a href="#目次0" title="目次">目次</a></li>
+<li><a href="#CbCXv6-での-Paging0" title="CbCXv6 での Paging">CbCXv6 での Paging</a></li>
+<li><a href="#実メモリの直接操作" title="実メモリの直接操作">実メモリの直接操作</a></li>
+<li><a href="#Paging0" title="Paging">Paging</a></li>
+<li><a href="#Pagingの図" title="Pagingの図">Pagingの図</a></li>
+<li><a href="#メタレベルでの-Paging-の操作" title="メタレベルでの Paging の操作">メタレベルでの Paging の操作</a></li>
+<li class=""><a href="#Paging-の信頼性" title="Paging の信頼性">Paging の信頼性</a></li>
+<li><a href="#Paging-の書き換え" title="Paging の書き換え">Paging の書き換え</a></li>
+<li><a href="#目次" title="目次">目次</a></li>
 </ul>
 </div><div class="toc-menu"><a class="expand-toggle" href="#">Expand all</a><a class="back-to-top" href="#">Back to top</a><a class="go-to-bottom" href="#">Go to bottom</a></div>
             </ul>
@@ -199,9 +332,29 @@
 <li><a href="#状態遷移モデル" title="状態遷移モデル">状態遷移モデル</a></li>
 <li><a href="#Agda-による検証" title="Agda による検証">Agda による検証</a></li>
 <li><a href="#Haure-Logic" title="Haure Logic">Haure Logic</a></li>
-<li class=""><a href="#Geas-OS" title="Geas OS">Geas OS</a></li>
-<li><a href="#メモリ管理" title="メモリ管理">メモリ管理</a></li>
+<li><a href="#Geas-OS" title="Geas OS">Geas OS</a></li>
+<li><a href="#メモリ管理0" title="メモリ管理">メモリ管理</a></li>
 <li><a href="#インターフェース" title="インターフェース">インターフェース</a></li>
+<li><a href="#目次0" title="目次">目次</a></li>
+<li><a href="#CbC-による-Gears-OS-の開発" title="CbC による Gears OS の開発">CbC による Gears OS の開発</a></li>
+<li><a href="#Context" title="Context">Context</a></li>
+<li><a href="#目次1" title="目次">目次</a></li>
+<li><a href="#Xv60" title="Xv6">Xv6</a></li>
+<li><a href="#カーネル空間" title="カーネル空間">カーネル空間</a></li>
+<li><a href="#カーネルが提供するもの" title="カーネルが提供するもの">カーネルが提供するもの</a></li>
+<li><a href="#カーネルの保護機構" title="カーネルの保護機構">カーネルの保護機構</a></li>
+<li><a href="#system-call0" title="system call">system call</a></li>
+<li><a href="#system-call" title="system call">system call</a></li>
+<li><a href="#Xv6-rpi" title="Xv6-rpi">Xv6-rpi</a></li>
+<li><a href="#目次0" title="目次">目次</a></li>
+<li><a href="#CbCXv6-での-Paging0" title="CbCXv6 での Paging">CbCXv6 での Paging</a></li>
+<li><a href="#実メモリの直接操作" title="実メモリの直接操作">実メモリの直接操作</a></li>
+<li><a href="#Paging0" title="Paging">Paging</a></li>
+<li><a href="#Pagingの図" title="Pagingの図">Pagingの図</a></li>
+<li><a href="#メタレベルでの-Paging-の操作" title="メタレベルでの Paging の操作">メタレベルでの Paging の操作</a></li>
+<li class=""><a href="#Paging-の信頼性" title="Paging の信頼性">Paging の信頼性</a></li>
+<li><a href="#Paging-の書き換え" title="Paging の書き換え">Paging の書き換え</a></li>
+<li><a href="#目次" title="目次">目次</a></li>
 </ul>
 </div><div class="toc-menu"><a class="expand-toggle" href="#">Expand all</a><a class="back-to-top" href="#">Back to top</a><a class="go-to-bottom" href="#">Go to bottom</a></div>
     </div>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slide/CbCXv6.md	Fri Feb 07 20:06:13 2020 +0900
@@ -0,0 +1,291 @@
+# CbCインターフェースによる CbCXv6 の書き換え
+- 並列信頼研
+- 桃原 優
+
+---
+
+# 目次
+1. **OS の信頼性の保証**
+2. CbC による Gears OS の開発
+3. Xv6
+4. CbCXv6 での Paging
+5. CbC インターフェース
+6. 評価
+7. まとめ
+
+---
+
+# OS の信頼性の重要性
+- OS のバグは日常生活に支障をきたす
+    - パスワードなしで root にアクセスできるバグ
+    - 日付設定でコンピュータが壊れる
+    - -> OS自体に信頼性が求められる
+
+---
+
+# OS の信頼性の重要性
+
+- 全てのOSのコードに対して検証を行うのは困難
+    - 複雑な機能が多い
+    - 短期間のアップデート
+
+- ユーザーが検証を行うこともできない
+    - 資源管理はOSが行なってる
+    - そもそも資源管理が複雑
+    - アクセスされたり書き換えられるリスク
+
+---
+
+
+# メタレベルとノーマルレベル
+- ノーマルレベル
+    - ユーザーがプログラミング言語によって記述する部分の処理
+- メタレベル
+    - ユーザーが記述しないOS 側の処理
+        - CPU
+        - メモリ
+
+---
+
+# Continuation based C
+- ノーマルレベルとメタレベルの処理を同じ言語で行えるようにした言語(以下CbC)
+- Code Gear
+    - 基本的な処理の単位
+- Data Gear
+    - データの単位
+
+---
+
+# goto による継続
+
+- Code Gear の処理の間を goto によって遷移していく
+
+![](https://i.imgur.com/etfQund.png)
+
+---
+
+# Data Gear の継続
+- goto の際に Data Gear も継続される
+
+![](https://i.imgur.com/3E0DGWA.png)
+
+---
+
+# Meta Code Gear
+- 実際にはノーマルレベルの間にメタレベルの処理がある
+- Meta Level では Data Gear の見え方は変わる(Meta Data Gear)
+
+![](https://i.imgur.com/vy0NxrG.png)
+
+---
+
+# 状態遷移モデル
+- goto の遷移によって状態遷移モデルに落とし込める
+- Code Gear に対しての入力に対して期待される出力がされているかで検査して**信頼性を保証する**
+
+----
+
+# Agda による検証
+- モデル検査
+    - 定理証明支援系である Agda を用いる。
+- Agda
+    - Haure Logic という検証手法を扱える。
+
+---
+
+# Haure Logic
+- 検証手法
+    - 事前条件を使ってある関数を実行して事後条件を満たすことを確認する
+- CbCと相性がいい
+    - 継続に事前条件(Input Data Gear)と事後条件(Output Data Gear)を持たせることができる
+
+---
+
+# Geas OS
+- CbC を使って信頼性の保証と拡張性を持たせる Gears OS の開発を行なっている
+- Xv6 という OS を参考に書き換えをしている
+
+---
+
+# メモリ管理
+- OS の信頼性の1つであるメモリ管理部分を CbC で書き換える
+    - Page のバリデーションチェック
+    - サンドボックスによるエクセプション
+
+---
+
+# インターフェース
+- 書き換えを防ぐために見える Data Gear に違いが生じる
+- -> Gears OS のノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入
+- 機能の入れ替えによる他のメリット
+    - 煩雑な記述の解消
+    - 機能の入れ替え
+    - Agda による証明
+
+
+---
+
+# 目次
+1. OS の信頼性の保証
+2. **CbC による Gears OS の開発**
+3. Xv6
+4. CbCXv6 での Paging
+5. CbC インターフェース
+6. 評価
+7. まとめ
+
+---
+
+# CbC による Gears OS の開発
+- a
+
+
+
+---
+
+
+# Context
+- a
+
+---
+
+# 目次
+1. OS の信頼性の保証
+2. CbC による Gears OS の開発
+3. **Xv6**
+4. CbCXv6 での Paging
+5. CbC インターフェース
+6. 評価
+7. まとめ
+
+---
+
+# Xv6
+- MIT の講義用教材として作られたOS
+    - 企画課される前のCで書かれたUNIX V6 を書き換えた
+    - 1万行程の軽量なOS
+    - Linuxだと数千万行
+- Xv6 を参考に CbC で書き直すことで Gears OS を実装する
+
+---
+
+# カーネル空間
+- OS の中核となるプログラムで Meta Level に相当する
+- Xv6 ではカーネルとユーザープログラムは分離されている
+- ユーザープログラムはカーネルに直接アクセスできない。
+    - 書き換えやアクセスを防ぐため
+    - 呼び出す場合は system call
+
+---
+
+# カーネルが提供するもの
+- プロセス管理
+- メモリ管理
+- ファイル管理
+    - I/O, read, write
+
+
+---
+
+# カーネルの保護機構
+- CPUのハードウェア保護機構を持っている
+- ユーザー空間で実行されているプロセスが自身のメモリのみアクセスできるように保護
+- system call
+    - ハードウェアが一時的に特権レベルをあげ、カーネルのプログラムが実行される
+
+---
+
+# system call
+- system call 呼び出し
+- トラップ の発生
+- ユーザープログラムの中断
+- 処理がカーネルに切り替わる
+
+---
+
+# system call
+- ソースコード載せる
+
+---
+
+# Xv6-rpi
+- Xv6 は　Arm のバイナリを出力するので様々なハードウェアで動かすことができる
+    - Raspberry Pi
+    - 携帯電話
+- 実際にRaspberry Pi で動かすために xv6-rpi を用意して動作しているかコンソールで確認中
+    - CbCxv6 とは別
+
+
+---
+
+# 目次
+1. OS の信頼性の保証
+2. CbC による Gears OS の開発
+3. Xv6
+4. **CbCXv6 での Paging**
+5. CbC インターフェース
+6. 評価
+7. まとめ
+
+---
+
+# CbCXv6 での Paging
+- OS の信頼性の1つであるメモリ管理部分の書き換えについて説明
+
+---
+
+# 実メモリの直接操作
+- 実メモリを直接扱うと様々な問題が生じる
+    - ユーザープログラムで空いているメモリ番地を探す必要
+    - フラグメンテーションが起こる
+        - メモリ間に扱うには小さな隙間ができる
+
+---
+
+# Paging
+- メモリ管理の手法
+- Page と呼ばれる固定長のブロックに分割して、メモリとスワップ領域で Page を入れ替えて管理
+- 仮想メモリとして扱うことでフラグメンテーションの解消と空き番地を探す必要がなくなる
+
+---
+
+# Pagingの図
+- 必要？
+
+---
+
+# メタレベルでの Paging の操作
+- Page Table に相当するデータを Input Data Gear で受け取って変更した後、Context にある Meta Data Gear に goto で遷移してアクセス
+- メタレベルで処理することで本来カーネル側の処理である Page Table を操作できる
+
+---
+
+# Paging の信頼性
+- Input Data Gear に対しての Output Data Gear をバリデーションチェックすることで他のプロセスから書き換えられることを防ぐ
+- サンドボックス
+    - 他のプロセスから書き換えられた時にエクセプションを飛ばす
+
+---
+
+# Paging の書き換え
+- Xv6 では実メモリから仮想メモリの変換をvm.cで行なっている。
+- 次の章で書き換えについて説明する
+
+
+
+---
+
+# 目次
+1. OS の信頼性の保証
+2. CbC による Gears OS の開発
+3. Xv6
+4. CbCXv6 での Paging**
+5. **CbC インターフェース**
+6. 評価
+7. まとめ
+
+---
+
+
+
+