Mercurial > hg > Papers > 2020 > tobaru-master
changeset 17:6afd90dba6db
slide chapter1
| author | tobaru |
|---|---|
| date | Fri, 07 Feb 2020 16:53:09 +0900 |
| parents | b35cb5777a5c |
| children | afc36230cf4f |
| files | paper/GearsOS.tex paper/fig/Meta_Code_Gear.graffle paper/fig/Meta_Code_Gear.pdf paper/fig/normal_Data.pdf paper/master_paper.aux paper/master_paper.lof paper/master_paper.log paper/master_paper.lol paper/master_paper.pdf paper/master_paper.synctex.gz paper/master_paper.tex paper/master_paper.toc paper/memory_manage.tex slide/CbCXv6.html slide/fig/Meta_Code_Gear.graffle slide/fig/Meta_Code_Gear.pdf slide/fig/Meta_Code_Gear.png slide/fig/normal_Code.graffle slide/fig/normal_Code.pdf slide/fig/normal_Code.png slide/fig/normal_Data.graffle slide/fig/normal_Data.pdf slide/fig/normal_Data.png thsis_paging.mm thsis_paging.pdf |
| diffstat | 25 files changed, 511 insertions(+), 149 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/GearsOS.tex Thu Feb 06 18:40:10 2020 +0900 +++ b/paper/GearsOS.tex Fri Feb 07 16:53:09 2020 +0900 @@ -8,7 +8,7 @@ Gears OS は Code Gear と Data Gear という単位でプログラムを記述する CbC を用いて実装する。 Code Gear は CbC における最も基本的な処理の単位である。 Code Gear 間で入力(Input Data Gear)と出力(Output Data Gear)を持ち、goto によって Code Gear から次の Code Gear へ遷移し、継続的に処理を行う。 -関数呼び出しとは異なり、呼び出し元には戻らない。j +関数呼び出しとは異なり、呼び出し元には戻らない。 Code Gear 間の処理の流れを図 \ref{fig:codegear} に示す。 @@ -30,13 +30,17 @@ CbC ではノーマルレベルの記述と別にメタレベルで記述することができる。メタレベルの記述によって User Space 側からメモリ管理を行えるようになる。 -メタ計算は Meta Code Gear と Meta Data Gear を用いる。この2つはノーマルレベルからメタレベルの変換する時に使われる。メタレベルの変換は Perl スクリプトで実装している。Gears OS での Meta Code Gear は Code Gear の直前、 直後に挿入され、メタ計算を実行する。 +メタ計算は Meta Code Gear と Meta Data Gear を用いる。 +この2つはノーマルレベルからメタレベルの変換する時に使われる。 +メタレベルの変換は Perl スクリプトで実装している。 +Gears OS での Meta Code Gear は Code Gear の直前、 直後に挿入され、メタ計算を実行する。 +それぞれの Code Gear, Meta Code Gear の継続には入力される Data Gear(Input Data Gear) と出力されるData Gear(Output Data Gear)が存在する。 Code Gear 間の継続はノーマルレベルでは 図 \ref{fig:codegear} のように見えるが、メタレベルでの Code Gear は図 \ref{fig:meta_cg_dg} の下のように継続を行っている。 \begin{figure}[ht] \begin{center} - \includegraphics[width=160mm]{./fig/meta_cg_dg} + \includegraphics[width=160mm]{./fig/Meta_Code_Gear} \end{center} \caption{ノーマルレベルとメタレベルの継続の見え方} \label{fig:meta_cg_dg}
--- a/paper/master_paper.aux Thu Feb 06 18:40:10 2020 +0900 +++ b/paper/master_paper.aux Fri Feb 07 16:53:09 2020 +0900 @@ -2,64 +2,64 @@ \@writefile{toc}{\contentsline {chapter}{\numberline {第1章}OS の信頼性の保障}{2}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\@writefile{toc}{\contentsline {chapter}{\numberline {第2章}CbC による Geas OS の開発}{3}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{\numberline {第2章}CbC による Geas OS の開発}{4}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\@writefile{toc}{\contentsline {section}{\numberline {2.1}Code Gear と Data Gear}{3}\protected@file@percent } -\@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces Code Gear 間の継続}}{3}\protected@file@percent } -\newlabel{fig:codegear}{{2.1}{3}} -\@writefile{toc}{\contentsline {section}{\numberline {2.2}Meta Code Gear と Meta Data Gear}{4}\protected@file@percent } -\@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces ノーマルレベルとメタレベルの継続の見え方}}{4}\protected@file@percent } -\newlabel{fig:meta_cg_dg}{{2.2}{4}} -\@writefile{toc}{\contentsline {section}{\numberline {2.3}Context}{4}\protected@file@percent } -\newlabel{contexth}{{2.1}{5}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.1}\footnotesize 生成された Context}{5}\protected@file@percent } -\@writefile{toc}{\contentsline {chapter}{\numberline {第3章}Xv6}{7}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {2.1}Code Gear と Data Gear}{4}\protected@file@percent } +\@writefile{lof}{\contentsline {figure}{\numberline {2.1}{\ignorespaces Code Gear 間の継続}}{4}\protected@file@percent } +\newlabel{fig:codegear}{{2.1}{4}} +\@writefile{toc}{\contentsline {section}{\numberline {2.2}Meta Code Gear と Meta Data Gear}{5}\protected@file@percent } +\@writefile{lof}{\contentsline {figure}{\numberline {2.2}{\ignorespaces ノーマルレベルとメタレベルの継続の見え方}}{5}\protected@file@percent } +\newlabel{fig:meta_cg_dg}{{2.2}{5}} +\@writefile{toc}{\contentsline {section}{\numberline {2.3}Context}{5}\protected@file@percent } +\newlabel{contexth}{{2.1}{6}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.1}\footnotesize 生成された Context}{6}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{\numberline {第3章}Xv6}{8}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\@writefile{toc}{\contentsline {section}{\numberline {3.1}Kernel Space と User Space}{7}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {3.2}system call}{7}\protected@file@percent } -\newlabel{syscall_list}{{3.1}{7}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.1}\footnotesize xv6 のシステムコールのリスト}{7}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {3.3}Xv6-rpi}{8}\protected@file@percent } -\@writefile{toc}{\contentsline {chapter}{\numberline {第4章}CbCXv6 での Paging}{9}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {3.1}Kernel Space と User Space}{8}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {3.2}system call}{8}\protected@file@percent } +\newlabel{syscall_list}{{3.1}{8}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {3.1}\footnotesize xv6 のシステムコールのリスト}{8}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {3.3}Xv6-rpi}{9}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{\numberline {第4章}CbCXv6 での Paging}{10}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\@writefile{toc}{\contentsline {section}{\numberline {4.1}Xv6 を元にした Gears OS の実装}{9}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {4.2}Paging}{9}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {4.3}User Space で Paging をする利点}{9}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {4.4}Paging の書き換え}{10}\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)}}{11}\protected@file@percent } -\newlabel{fig:MemoryConstitution}{{4.1}{11}} -\@writefile{toc}{\contentsline {chapter}{\numberline {第5章}CbC インターフェース}{12}\protected@file@percent } +\@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.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}} +\@writefile{toc}{\contentsline {chapter}{\numberline {第5章}CbC インターフェース}{13}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\@writefile{toc}{\contentsline {section}{\numberline {5.1}インターフェースの定義}{12}\protected@file@percent } -\newlabel{interface}{{5.1}{12}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.1}\footnotesize vm のインターフェースの定義(vm.h)}{12}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {5.2}インターフェースの実装}{13}\protected@file@percent } -\newlabel{impl_vm}{{5.2}{14}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.2}\footnotesize vm インターフェースの実装}{14}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {5.3}インターフェース内の private メソッド}{17}\protected@file@percent } -\newlabel{impl_vm_privateh}{{5.3}{17}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.3}\footnotesize vm private のヘッダーファイル}{17}\protected@file@percent } -\newlabel{vm_loaduvm}{{5.4}{18}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.4}\footnotesize vm.c のloaduvm}{18}\protected@file@percent } -\newlabel{impl_vm_loaduvm}{{5.5}{19}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.5}\footnotesize privateでの loaduvm の実装}{19}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {5.4}インターフェースの呼び出し}{21}\protected@file@percent } -\newlabel{cbc_goto}{{5.6}{21}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.6}\footnotesize cbc インターフェースのgoto}{21}\protected@file@percent } -\newlabel{dummy}{{5.7}{22}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.7}\footnotesize dummy を使った呼び出し}{22}\protected@file@percent } -\@writefile{toc}{\contentsline {chapter}{\numberline {第6章}評価}{24}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {5.1}インターフェースの定義}{13}\protected@file@percent } +\newlabel{interface}{{5.1}{13}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.1}\footnotesize vm のインターフェースの定義(vm.h)}{13}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {5.2}インターフェースの実装}{14}\protected@file@percent } +\newlabel{impl_vm}{{5.2}{15}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.2}\footnotesize vm インターフェースの実装}{15}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {5.3}インターフェース内の private メソッド}{18}\protected@file@percent } +\newlabel{impl_vm_privateh}{{5.3}{18}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.3}\footnotesize vm private のヘッダーファイル}{18}\protected@file@percent } +\newlabel{vm_loaduvm}{{5.4}{19}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.4}\footnotesize vm.c のloaduvm}{19}\protected@file@percent } +\newlabel{impl_vm_loaduvm}{{5.5}{20}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.5}\footnotesize privateでの loaduvm の実装}{20}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {5.4}インターフェースの呼び出し}{22}\protected@file@percent } +\newlabel{cbc_goto}{{5.6}{22}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.6}\footnotesize cbc インターフェースのgoto}{22}\protected@file@percent } +\newlabel{dummy}{{5.7}{23}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.7}\footnotesize dummy を使った呼び出し}{23}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{\numberline {第6章}評価}{25}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\@writefile{toc}{\contentsline {chapter}{\numberline {第7章}まとめ}{25}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{\numberline {第7章}まとめ}{26}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\@writefile{toc}{\contentsline {section}{\numberline {7.1}今後の書き換え方針}{25}\protected@file@percent } -\@writefile{toc}{\contentsline {chapter}{謝辞}{25}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {7.1}今後の書き換え方針}{26}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{謝辞}{26}\protected@file@percent } \citation{*} \bibdata{reference} \bibcite{xv6}{1} @@ -73,19 +73,19 @@ \bibcite{Sigurbjarnarson:2016:PVF:3026877.3026879}{9} \bibcite{agda-ryokka}{10} \bibcite{agda}{11} -\@writefile{toc}{\contentsline {chapter}{参考文献}{27}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{参考文献}{28}\protected@file@percent } \bibcite{llvm}{12} \bibcite{gcc}{13} \bibcite{gears}{14} \bibcite{arm}{15} \bibstyle{junsrt} -\@writefile{toc}{\contentsline {chapter}{発表履歴}{28}\protected@file@percent } -\@writefile{toc}{\contentsline {chapter}{付録}{29}\protected@file@percent } -\@writefile{toc}{\contentsline {chapter}{\numberline {付 録A }ソースコード一覧}{30}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{発表履歴}{29}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{付録}{30}\protected@file@percent } +\@writefile{toc}{\contentsline {chapter}{\numberline {付 録A }ソースコード一覧}{31}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\@writefile{toc}{\contentsline {section}{\numberline {A-1}インターフェース内の private メソッドの実装}{30}\protected@file@percent } -\newlabel{vm_c_all}{{A.1}{30}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {A.1}\footnotesize Xv6 の vm.c}{30}\protected@file@percent } -\newlabel{vm_impl_private}{{A.2}{38}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {A.2}\footnotesize vm の実装の private}{38}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {A-1}インターフェース内の private メソッドの実装}{31}\protected@file@percent } +\newlabel{vm_c_all}{{A.1}{31}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {A.1}\footnotesize Xv6 の vm.c}{31}\protected@file@percent } +\newlabel{vm_impl_private}{{A.2}{39}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {A.2}\footnotesize vm の実装の private}{39}\protected@file@percent }
--- a/paper/master_paper.lof Thu Feb 06 18:40:10 2020 +0900 +++ b/paper/master_paper.lof Fri Feb 07 16:53:09 2020 +0900 @@ -1,10 +1,10 @@ \addvspace {10\p@ } \addvspace {10\p@ } -\contentsline {figure}{\numberline {2.1}{\ignorespaces Code Gear 間の継続}}{3}% -\contentsline {figure}{\numberline {2.2}{\ignorespaces ノーマルレベルとメタレベルの継続の見え方}}{4}% +\contentsline {figure}{\numberline {2.1}{\ignorespaces Code Gear 間の継続}}{4}% +\contentsline {figure}{\numberline {2.2}{\ignorespaces ノーマルレベルとメタレベルの継続の見え方}}{5}% \addvspace {10\p@ } \addvspace {10\p@ } -\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)}}{11}% +\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}% \addvspace {10\p@ } \addvspace {10\p@ } \addvspace {10\p@ }
--- a/paper/master_paper.log Thu Feb 06 18:40:10 2020 +0900 +++ b/paper/master_paper.log Fri Feb 07 16:53:09 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) 6 FEB 2020 18:35 +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 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -359,10 +359,10 @@ ] 第 1 章(2ページ) -) (./GearsOS.tex [2 +[2 -] -第 2 章(3ページ) +]) (./GearsOS.tex [3] +第 2 章(4ページ) LaTeX Font Info: Font shape `JT1/hmc/m/n' will be (Font) scaled to size 16.62714pt on input line 7. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be @@ -373,30 +373,30 @@ (Font) scaled to size 16.62714pt on input line 7. File: ./fig/codegear.pdf Graphic file (type pdf) <./fig/codegear.pdf> -[3 +[4 ] -File: ./fig/meta_cg_dg.pdf Graphic file (type pdf) -<./fig/meta_cg_dg.pdf> - [4] (./src/context.h +File: ./fig/Meta_Code_Gear.pdf Graphic file (type pdf) +<./fig/Meta_Code_Gear.pdf> + [5] (./src/context.h LaTeX Font Info: Font shape `JT1/hmc/m/n' will be (Font) scaled to size 7.69775pt on input line 1. - [5])) (./Xv6.tex [6] -第 3 章(7ページ) -[7 + [6])) (./Xv6.tex [7] +第 3 章(8ページ) +[8 -]) (./Paging.tex [8] -第 4 章(9ページ) +]) (./Paging.tex [9] +第 4 章(10ページ) File: ./fig/MemoryConstitution.pdf Graphic file (type pdf) <./fig/MemoryConstitution.pdf> -) (./cbc_interface.tex [9 +) (./cbc_interface.tex [10 -] [10] [11] -第 5 章(12ページ) -(./src/vm.h [12 +] [11] [12] +第 5 章(13ページ) +(./src/vm.h [13 -]) (./src/vm_impl.cbc [13] [14] [15]) [16] -(./src/vm_impl_private.h [17]) [18] +]) (./src/vm_impl.cbc [14] [15] [16]) [17] +(./src/vm_impl_private.h [18]) [19] Overfull \hbox (39.8747pt too wide) in paragraph at lines 168--170 []\OT1/cmr/m/n/12 vm[]impl.cbc \JY1/hmc/m/n/12 の \OT1/cmr/m/n/12 Code Gear \JY 1/hmc/m/n/12 である \OT1/cmr/m/n/12 load-u-vmvm[]impl \JY1/hmc/m/n/12 から \OT1 @@ -412,16 +412,16 @@ uvm[]ptesize[]checkvm[]impl [] -[19] [20] (./src/failure_example_userinit [21]) (./src/dummy [22])) -(./evaluation.tex [23] -第 6 章(24ページ) -) (./summary.tex [24 +[20] [21] (./src/failure_example_userinit [22]) (./src/dummy [23])) +(./evaluation.tex [24] +第 6 章(25ページ) +) (./summary.tex [25 ] -第 7 章(25ページ) -) (./thanks.tex [25 +第 7 章(26ページ) +) (./thanks.tex [26 -]) (./master_paper.bbl [26 +]) (./master_paper.bbl [27 ] Underfull \hbox (badness 10000) in paragraph at lines 14--16 @@ -445,7 +445,7 @@ (Font) scaled to size 11.54663pt on input line 30. LaTeX Font Info: Font shape `JY1/hgt/m/it' will be (Font) scaled to size 11.54663pt on input line 30. -[27 +[28 ] Overfull \hbox (8.48145pt too wide) in paragraph at lines 86--89 @@ -453,7 +453,7 @@ tp://infocenter.arm.com/help/topic/com.arm. [] -) (./history.tex [28] +) (./history.tex [29] LaTeX Font Info: Trying to load font information for OMS+cmr on input line 3 . @@ -463,15 +463,15 @@ LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <12> not available (Font) Font shape `OMS/cmsy/m/n' tried instead on input line 3. ) -(./sources.tex [29 +(./sources.tex [30 ] -付 録 A (30ページ) -(./src/vm_all.c [30 +付 録 A (31ページ) +(./src/vm_all.c [31 -] [31] [32] [33] [34] [35] [36] [37]) -(./src/vm_impl_private_all.cbc [38] [39] [40] [41] [42] [43] [44] [45] [46])) -[47] (./master_paper.aux) +] [32] [33] [34] [35] [36] [37] [38]) +(./src/vm_impl_private_all.cbc [39] [40] [41] [42] [43] [44] [45] [46] [47])) +[48] (./master_paper.aux) LaTeX Font Warning: Size substitutions with differences (Font) up to 1.28pt have occurred. @@ -482,11 +482,11 @@ ) Here is how much of TeX's memory you used: 6421 strings out of 493985 - 91080 string characters out of 6166648 - 375234 words of memory out of 5000000 + 91100 string characters out of 6166648 + 375245 words of memory out of 5000000 10693 multiletter control sequences out of 15000+600000 17126 words of font info for 87 fonts, out of 8000000 for 9000 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 (55 pages, 241604 bytes). +Output written on master_paper.dvi (56 pages, 242880 bytes).
--- a/paper/master_paper.lol Thu Feb 06 18:40:10 2020 +0900 +++ b/paper/master_paper.lol Fri Feb 07 16:53:09 2020 +0900 @@ -1,11 +1,11 @@ -\contentsline {lstlisting}{\numberline {2.1}\footnotesize 生成された Context}{5}% -\contentsline {lstlisting}{\numberline {3.1}\footnotesize xv6 のシステムコールのリスト}{7}% -\contentsline {lstlisting}{\numberline {5.1}\footnotesize vm のインターフェースの定義(vm.h)}{12}% -\contentsline {lstlisting}{\numberline {5.2}\footnotesize vm インターフェースの実装}{14}% -\contentsline {lstlisting}{\numberline {5.3}\footnotesize vm private のヘッダーファイル}{17}% -\contentsline {lstlisting}{\numberline {5.4}\footnotesize vm.c のloaduvm}{18}% -\contentsline {lstlisting}{\numberline {5.5}\footnotesize privateでの loaduvm の実装}{19}% -\contentsline {lstlisting}{\numberline {5.6}\footnotesize cbc インターフェースのgoto}{21}% -\contentsline {lstlisting}{\numberline {5.7}\footnotesize dummy を使った呼び出し}{22}% -\contentsline {lstlisting}{\numberline {A.1}\footnotesize Xv6 の vm.c}{30}% -\contentsline {lstlisting}{\numberline {A.2}\footnotesize vm の実装の private}{38}% +\contentsline {lstlisting}{\numberline {2.1}\footnotesize 生成された Context}{6}% +\contentsline {lstlisting}{\numberline {3.1}\footnotesize xv6 のシステムコールのリスト}{8}% +\contentsline {lstlisting}{\numberline {5.1}\footnotesize vm のインターフェースの定義(vm.h)}{13}% +\contentsline {lstlisting}{\numberline {5.2}\footnotesize vm インターフェースの実装}{15}% +\contentsline {lstlisting}{\numberline {5.3}\footnotesize vm private のヘッダーファイル}{18}% +\contentsline {lstlisting}{\numberline {5.4}\footnotesize vm.c のloaduvm}{19}% +\contentsline {lstlisting}{\numberline {5.5}\footnotesize privateでの loaduvm の実装}{20}% +\contentsline {lstlisting}{\numberline {5.6}\footnotesize cbc インターフェースのgoto}{22}% +\contentsline {lstlisting}{\numberline {5.7}\footnotesize dummy を使った呼び出し}{23}% +\contentsline {lstlisting}{\numberline {A.1}\footnotesize Xv6 の vm.c}{31}% +\contentsline {lstlisting}{\numberline {A.2}\footnotesize vm の実装の private}{39}%
--- a/paper/master_paper.tex Thu Feb 06 18:40:10 2020 +0900 +++ b/paper/master_paper.tex Fri Feb 07 16:53:09 2020 +0900 @@ -12,7 +12,7 @@ %\input{dummy.tex} %% font -\jtitle{GearsOS の Paging} +\jtitle{CbCインターフェースによる CbCXv6 の書き換え} \etitle{} % 英文例題まだ \year{2020年 3月} \eyear{March 2020}
--- a/paper/master_paper.toc Thu Feb 06 18:40:10 2020 +0900 +++ b/paper/master_paper.toc Fri Feb 07 16:53:09 2020 +0900 @@ -1,28 +1,28 @@ \contentsline {chapter}{\numberline {第1章}OS の信頼性の保障}{2}% -\contentsline {chapter}{\numberline {第2章}CbC による Geas OS の開発}{3}% -\contentsline {section}{\numberline {2.1}Code Gear と Data Gear}{3}% -\contentsline {section}{\numberline {2.2}Meta Code Gear と Meta Data Gear}{4}% -\contentsline {section}{\numberline {2.3}Context}{4}% -\contentsline {chapter}{\numberline {第3章}Xv6}{7}% -\contentsline {section}{\numberline {3.1}Kernel Space と User Space}{7}% -\contentsline {section}{\numberline {3.2}system call}{7}% -\contentsline {section}{\numberline {3.3}Xv6-rpi}{8}% -\contentsline {chapter}{\numberline {第4章}CbCXv6 での Paging}{9}% -\contentsline {section}{\numberline {4.1}Xv6 を元にした Gears OS の実装}{9}% -\contentsline {section}{\numberline {4.2}Paging}{9}% -\contentsline {section}{\numberline {4.3}User Space で Paging をする利点}{9}% -\contentsline {section}{\numberline {4.4}Paging の書き換え}{10}% -\contentsline {chapter}{\numberline {第5章}CbC インターフェース}{12}% -\contentsline {section}{\numberline {5.1}インターフェースの定義}{12}% -\contentsline {section}{\numberline {5.2}インターフェースの実装}{13}% -\contentsline {section}{\numberline {5.3}インターフェース内の private メソッド}{17}% -\contentsline {section}{\numberline {5.4}インターフェースの呼び出し}{21}% -\contentsline {chapter}{\numberline {第6章}評価}{24}% -\contentsline {chapter}{\numberline {第7章}まとめ}{25}% -\contentsline {section}{\numberline {7.1}今後の書き換え方針}{25}% -\contentsline {chapter}{謝辞}{25}% -\contentsline {chapter}{参考文献}{27}% -\contentsline {chapter}{発表履歴}{28}% -\contentsline {chapter}{付録}{29}% -\contentsline {chapter}{\numberline {付 録A }ソースコード一覧}{30}% -\contentsline {section}{\numberline {A-1}インターフェース内の private メソッドの実装}{30}% +\contentsline {chapter}{\numberline {第2章}CbC による Geas OS の開発}{4}% +\contentsline {section}{\numberline {2.1}Code Gear と Data Gear}{4}% +\contentsline {section}{\numberline {2.2}Meta Code Gear と Meta Data Gear}{5}% +\contentsline {section}{\numberline {2.3}Context}{5}% +\contentsline {chapter}{\numberline {第3章}Xv6}{8}% +\contentsline {section}{\numberline {3.1}Kernel Space と User Space}{8}% +\contentsline {section}{\numberline {3.2}system call}{8}% +\contentsline {section}{\numberline {3.3}Xv6-rpi}{9}% +\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.4}Paging の書き換え}{11}% +\contentsline {chapter}{\numberline {第5章}CbC インターフェース}{13}% +\contentsline {section}{\numberline {5.1}インターフェースの定義}{13}% +\contentsline {section}{\numberline {5.2}インターフェースの実装}{14}% +\contentsline {section}{\numberline {5.3}インターフェース内の private メソッド}{18}% +\contentsline {section}{\numberline {5.4}インターフェースの呼び出し}{22}% +\contentsline {chapter}{\numberline {第6章}評価}{25}% +\contentsline {chapter}{\numberline {第7章}まとめ}{26}% +\contentsline {section}{\numberline {7.1}今後の書き換え方針}{26}% +\contentsline {chapter}{謝辞}{26}% +\contentsline {chapter}{参考文献}{28}% +\contentsline {chapter}{発表履歴}{29}% +\contentsline {chapter}{付録}{30}% +\contentsline {chapter}{\numberline {付 録A }ソースコード一覧}{31}% +\contentsline {section}{\numberline {A-1}インターフェース内の private メソッドの実装}{31}%
--- a/paper/memory_manage.tex Thu Feb 06 18:40:10 2020 +0900 +++ b/paper/memory_manage.tex Fri Feb 07 16:53:09 2020 +0900 @@ -4,17 +4,19 @@ OS 自体に信頼性が求められるが、複雑な機能が多く、短期間のアップデートが必要な OS では、全てのコードに対して検証を行うのは困難である。 -CPU やメモリなどの資源管理は基本的には OS が行なっている。資源管理が複雑な上、アクセスされたり書き換えられることを防ぐためだと考えられる。 -これによってユーザーは資源を気にすることなくコンピュータを扱うことができる。 +CPU やメモリなどの資源管理は基本的には OS が行なっているため、ユーザーが信頼性を保証こともできない。 +これは資源管理が複雑な上、アクセスされたり書き換えられることを防ぐためだと考えられる。 +OS による資源管理によってユーザーは資源を気にすることなくコンピュータを扱うことができる。 このように OS には資源管理やシステムコールされた後の処理などユーザーが記述するプログラム以外の部分が存在する。 その処理をメタレベルの計算、ユーザーが記述する部分をノーマルレベルの計算と呼ぶ。 - 本研究室ではノーマルレベルとメタレベルの記述を行える CbC というプログラミング言語を開発してきた。 -CbC はノーマルレベルとメタレベルの記述の間を関数型プログラミング言語のように goto によって継続する。そのため、状態遷移モデルに落とし込むことができる。関数の1つ1つをモデル検査することで信頼性を保証したい。 +CbC は Code Gear という基本的な処理の単位と Data Gear というデータの単位を用いる。 +細かい処理に対してノーマルレベルとメタレベルの Code Gear を記述し、その間を関数型プログラミング言語のように goto によって継続する。そのため、状態遷移モデルに落とし込むことができる。 +Code Gear に対して入力の Data Gear と出力の Data Gear が存在し、入力に対して期待される出力がされてるか検査することで信頼性を保証する。 モデル検査には定理証明支援系である Agda を用いる。 @@ -27,7 +29,7 @@ % 資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する Xv6 という OS を参考にした Geas OS の書き換えの説明を行う。 OS の信頼性の基本であるメモリ管理部分を書き換えることで Page のバリデーションチェックによる不正なデータの変更やサンドボックスによるエクセプションをが可能となる。 -また、Gears OS のメタレベルとノーマルレベルの記述が煩雑になるため、インターフェースによるモジュール化を導入した。 +また、Gears OS のメタレベルとノーマルレベルでは書き換えなどを防ぐために見えるデータに違いが生じ、Code Gear と Meta Code Gear の記述も煩雑になる。それを解消するために、インターフェースによるモジュール化を導入した。 % インターフェースは Agda に対応するようになっている。これにより Code Gear、Data Gearんの Agda による証明が可能になるように Geas OS の構築を行った。 インターフェースを使うことで機能の入れ替えによる拡張性や Agda による証明が可能となることを目的する。 @@ -35,10 +37,6 @@ % しているが、 さらに資源管理を行える CbC で軽量なハードウェアでも動かせるように Arm のバイナリを出力する Xv6 を参考に GearsOS にメモリ管理を行う API を考察する。 - +% Page をいじるのは メタレベル % しかし、ユーザー空間で資源管理を行えるようにすることで、 % Page のバリデーションをチェックしたり、サンドボックスによる信頼性の保証を行えるようになる。また、適切な記述をすれば最適な資源管理にも繋がる。 - - - -
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/slide/CbCXv6.html Fri Feb 07 16:53:09 2020 +0900 @@ -0,0 +1,356 @@ +<!DOCTYPE html> + +<html lang="en"> + +<head> + <meta charset="utf-8"> + <meta http-equiv="X-UA-Compatible" content="IE=edge"> + <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=no"> + <meta name="apple-mobile-web-app-capable" content="yes"> + <meta name="apple-mobile-web-app-status-bar-style" content="black"> + <meta name="mobile-web-app-capable" content="yes"> + <title> + CbCインターフェースによる CbCXv6 の書き換え - HackMD + </title> + <link rel="icon" type="image/png" href="https://hackmd.io/favicon.png"> + <link rel="apple-touch-icon" href="https://hackmd.io/apple-touch-icon.png"> + + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/twitter-bootstrap/3.3.7/css/bootstrap.min.css" integrity="sha256-916EbMg70RQy9LHiGkXzG8hSg9EdNy97GazNG/aiY1w=" crossorigin="anonymous" /> + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/4.7.0/css/font-awesome.min.css" integrity="sha256-eZrrJcwDc/3uDhsdt61sL2oOBY362qM3lon1gyExkL0=" crossorigin="anonymous" /> + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/ionicons/2.0.1/css/ionicons.min.css" integrity="sha256-3iu9jgsy9TpTwXKb7bNQzqWekRX7pPK+2OLj3R922fo=" crossorigin="anonymous" /> + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/octicons/3.5.0/octicons.min.css" integrity="sha256-QiWfLIsCT02Sdwkogf6YMiQlj4NE84MKkzEMkZnMGdg=" crossorigin="anonymous" /> + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/prism/1.5.1/themes/prism.min.css" integrity="sha256-vtR0hSWRc3Tb26iuN2oZHt3KRUomwTufNIf5/4oeCyg=" crossorigin="anonymous" /> + <link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/emojify.js/1.1.0/css/basic/emojify.min.css" integrity="sha256-UOrvMOsSDSrW6szVLe8ZDZezBxh5IoIfgTwdNDgTjiU=" crossorigin="anonymous" /> + <style> + @charset "UTF-8";@import url(https://fonts.googleapis.com/css?family=Roboto:300,300i,400,400i,500,500i|Source+Code+Pro:300,400,500|Source+Sans+Pro:300,300i,400,400i,600,600i|Source+Serif+Pro&subset=latin-ext);.hljs{display:block;background:#fff;padding:.5em;color:#333;overflow-x:auto}.hljs-comment,.hljs-meta{color:#969896}.hljs-emphasis,.hljs-quote,.hljs-string,.hljs-strong,.hljs-template-variable,.hljs-variable{color:#df5000}.hljs-keyword,.hljs-selector-tag,.hljs-type{color:#a71d5d}.hljs-attribute,.hljs-bullet,.hljs-literal,.hljs-number,.hljs-symbol{color:#0086b3}.hljs-built_in,.hljs-builtin-name{color:#005cc5}.hljs-name,.hljs-section{color:#63a35c}.hljs-tag{color:#333}.hljs-attr,.hljs-selector-attr,.hljs-selector-class,.hljs-selector-id,.hljs-selector-pseudo,.hljs-title{color:#795da3}.hljs-addition{color:#55a532;background-color:#eaffea}.hljs-deletion{color:#bd2c00;background-color:#ffecec}.hljs-link{text-decoration:underline}.markdown-body{font-size:16px;line-height:1.5;word-wrap:break-word}.markdown-body:after,.markdown-body:before{display:table;content:""}.markdown-body:after{clear:both}.markdown-body>:first-child{margin-top:0!important}.markdown-body>:last-child{margin-bottom:0!important}.markdown-body a:not([href]){color:inherit;text-decoration:none}.markdown-body .absent{color:#c00}.markdown-body .anchor{float:left;padding-right:4px;margin-left:-20px;line-height:1}.markdown-body .anchor:focus{outline:none}.markdown-body blockquote,.markdown-body dl,.markdown-body ol,.markdown-body p,.markdown-body pre,.markdown-body table,.markdown-body ul{margin-top:0;margin-bottom:16px}.markdown-body hr{height:.25em;padding:0;margin:24px 0;background-color:#e7e7e7;border:0}.markdown-body blockquote{font-size:16px;padding:0 1em;color:#777;border-left:.25em solid #ddd}.markdown-body blockquote>:first-child{margin-top:0}.markdown-body blockquote>:last-child{margin-bottom:0}.markdown-body kbd,.popover kbd{display:inline-block;padding:3px 5px;font-size:11px;line-height:10px;color:#555;vertical-align:middle;background-color:#fcfcfc;border:1px solid #ccc;border-bottom-color:#bbb;border-radius:3px;box-shadow:inset 0 -1px 0 #bbb}.markdown-body .loweralpha{list-style-type:lower-alpha}.markdown-body h1,.markdown-body h2,.markdown-body h3,.markdown-body h4,.markdown-body h5,.markdown-body h6{margin-top:24px;margin-bottom:16px;font-weight:600;line-height:1.25}.markdown-body h1 .octicon-link,.markdown-body h2 .octicon-link,.markdown-body h3 .octicon-link,.markdown-body h4 .octicon-link,.markdown-body h5 .octicon-link,.markdown-body h6 .octicon-link{color:#000;vertical-align:middle;visibility:hidden}.markdown-body h1:hover .anchor,.markdown-body h2:hover .anchor,.markdown-body h3:hover .anchor,.markdown-body h4:hover .anchor,.markdown-body h5:hover .anchor,.markdown-body h6:hover .anchor{text-decoration:none}.markdown-body h1:hover .anchor .octicon-link,.markdown-body h2:hover .anchor .octicon-link,.markdown-body h3:hover .anchor .octicon-link,.markdown-body h4:hover .anchor .octicon-link,.markdown-body h5:hover .anchor .octicon-link,.markdown-body h6:hover .anchor .octicon-link{visibility:visible}.markdown-body h1 code,.markdown-body h1 tt,.markdown-body h2 code,.markdown-body h2 tt,.markdown-body h3 code,.markdown-body h3 tt,.markdown-body h4 code,.markdown-body h4 tt,.markdown-body h5 code,.markdown-body h5 tt,.markdown-body h6 code,.markdown-body h6 tt{font-size:inherit}.markdown-body h1{font-size:2em}.markdown-body h1,.markdown-body h2{padding-bottom:.3em;border-bottom:1px solid #eee}.markdown-body h2{font-size:1.5em}.markdown-body h3{font-size:1.25em}.markdown-body h4{font-size:1em}.markdown-body h5{font-size:.875em}.markdown-body h6{font-size:.85em;color:#777}.markdown-body ol,.markdown-body ul{padding-left:2em}.markdown-body ol.no-list,.markdown-body ul.no-list{padding:0;list-style-type:none}.markdown-body ol ol,.markdown-body ol ul,.markdown-body ul ol,.markdown-body ul ul{margin-top:0;margin-bottom:0}.markdown-body li>p{margin-top:16px}.markdown-body li+li{padding-top:.25em}.markdown-body dl{padding:0}.markdown-body dl dt{padding:0;margin-top:16px;font-size:1em;font-style:italic;font-weight:700}.markdown-body dl dd{padding:0 16px;margin-bottom:16px}.markdown-body table{display:block;width:100%;overflow:auto;word-break:normal;word-break:keep-all}.markdown-body table th{font-weight:700}.markdown-body table td,.markdown-body table th{padding:6px 13px;border:1px solid #ddd}.markdown-body table tr{background-color:#fff;border-top:1px solid #ccc}.markdown-body table tr:nth-child(2n){background-color:#f8f8f8}.markdown-body img{max-width:100%;box-sizing:content-box;background-color:#fff}.markdown-body img[align=right]{padding-left:20px}.markdown-body img[align=left]{padding-right:20px}.markdown-body .emoji{max-width:none;vertical-align:text-top;background-color:transparent}.markdown-body span.frame{display:block;overflow:hidden}.markdown-body span.frame>span{display:block;float:left;width:auto;padding:7px;margin:13px 0 0;overflow:hidden;border:1px solid #ddd}.markdown-body span.frame span img{display:block;float:left}.markdown-body span.frame span span{display:block;padding:5px 0 0;clear:both;color:#333}.markdown-body span.align-center{display:block;overflow:hidden;clear:both}.markdown-body span.align-center>span{display:block;margin:13px auto 0;overflow:hidden;text-align:center}.markdown-body span.align-center span img{margin:0 auto;text-align:center}.markdown-body span.align-right{display:block;overflow:hidden;clear:both}.markdown-body span.align-right>span{display:block;margin:13px 0 0;overflow:hidden;text-align:right}.markdown-body span.align-right span img{margin:0;text-align:right}.markdown-body span.float-left{display:block;float:left;margin-right:13px;overflow:hidden}.markdown-body span.float-left span{margin:13px 0 0}.markdown-body span.float-right{display:block;float:right;margin-left:13px;overflow:hidden}.markdown-body span.float-right>span{display:block;margin:13px auto 0;overflow:hidden;text-align:right}.markdown-body code,.markdown-body tt{padding:0;padding-top:.2em;padding-bottom:.2em;margin:0;font-size:85%;background-color:rgba(0,0,0,.04);border-radius:3px}.markdown-body code:after,.markdown-body code:before,.markdown-body tt:after,.markdown-body tt:before{letter-spacing:-.2em;content:"\00a0"}.markdown-body code br,.markdown-body tt br{display:none}.markdown-body del code{text-decoration:inherit}.markdown-body pre{word-wrap:normal}.markdown-body pre>code{padding:0;margin:0;font-size:100%;word-break:normal;white-space:pre;background:transparent;border:0}.markdown-body .highlight{margin-bottom:16px}.markdown-body .highlight pre{margin-bottom:0;word-break:normal}.markdown-body .highlight pre,.markdown-body pre{padding:16px;overflow:auto;font-size:85%;line-height:1.45;background-color:#f7f7f7;border-radius:3px}.markdown-body pre code,.markdown-body pre tt{display:inline;max-width:auto;padding:0;margin:0;overflow:visible;line-height:inherit;word-wrap:normal;background-color:transparent;border:0}.markdown-body pre code:after,.markdown-body pre code:before,.markdown-body pre tt:after,.markdown-body pre tt:before{content:normal}.markdown-body .csv-data td,.markdown-body .csv-data th{padding:5px;overflow:hidden;font-size:12px;line-height:1;text-align:left;white-space:nowrap}.markdown-body .csv-data .blob-line-num{padding:10px 8px 9px;text-align:right;background:#fff;border:0}.markdown-body .csv-data tr{border-top:0}.markdown-body .csv-data th{font-weight:700;background:#f8f8f8;border-top:0}.news .alert .markdown-body blockquote{padding:0 0 0 40px;border:0 none}.activity-tab .news .alert .commits,.activity-tab .news .markdown-body blockquote{padding-left:0}.task-list-item{list-style-type:none}.task-list-item label{font-weight:400}.task-list-item.enabled label{cursor:pointer}.task-list-item+.task-list-item{margin-top:3px}.task-list-item-checkbox{float:left;margin:.31em 0 .2em -1.3em!important;vertical-align:middle;cursor:default!important}.markdown-body{padding-top:40px;padding-bottom:40px;max-width:758px;overflow:visible!important}.markdown-body .emoji{vertical-align:top}.markdown-body pre{border:inherit!important}.markdown-body code{color:inherit!important}.markdown-body pre code .wrapper{display:-moz-inline-flex;display:-ms-inline-flex;display:-o-inline-flex;display:inline-flex}.markdown-body pre code .gutter{float:left;overflow:hidden;-webkit-user-select:none;user-select:none}.markdown-body pre code .gutter.linenumber{text-align:right;position:relative;display:inline-block;cursor:default;z-index:4;padding:0 8px 0 0;min-width:20px;box-sizing:content-box;color:#afafaf!important;border-right:3px solid #6ce26c!important}.markdown-body pre code .gutter.linenumber>span:before{content:attr(data-linenumber)}.markdown-body pre code .code{float:left;margin:0 0 0 16px}.markdown-body .gist .line-numbers{border-left:none;border-top:none;border-bottom:none}.markdown-body .gist .line-data{border:none}.markdown-body .gist table{border-spacing:0;border-collapse:inherit!important}.markdown-body code[data-gist-id]{background:none;padding:0}.markdown-body code[data-gist-id]:after,.markdown-body code[data-gist-id]:before{content:""}.markdown-body code[data-gist-id] .blob-num{border:unset}.markdown-body code[data-gist-id] table{overflow:unset;margin-bottom:unset}.markdown-body code[data-gist-id] table tr{background:unset}.markdown-body[dir=rtl] pre{direction:ltr}.markdown-body[dir=rtl] code{direction:ltr;unicode-bidi:embed}.markdown-body .alert>p{margin-bottom:0}.markdown-body pre.abc,.markdown-body pre.flow-chart,.markdown-body pre.graphviz,.markdown-body pre.mermaid,.markdown-body pre.sequence-diagram{text-align:center;background-color:inherit;border-radius:0;white-space:inherit}.markdown-body pre.abc>code,.markdown-body pre.flow-chart>code,.markdown-body pre.graphviz>code,.markdown-body pre.mermaid>code,.markdown-body pre.sequence-diagram>code{text-align:left}.markdown-body pre.abc>svg,.markdown-body pre.flow-chart>svg,.markdown-body pre.graphviz>svg,.markdown-body pre.mermaid>svg,.markdown-body pre.sequence-diagram>svg{max-width:100%;height:100%}.markdown-body pre>code.wrap{white-space:pre-wrap;white-space:-moz-pre-wrap;white-space:-pre-wrap;white-space:-o-pre-wrap;word-wrap:break-word}.markdown-body .alert>p,.markdown-body .alert>ul{margin-bottom:0}.markdown-body summary{display:list-item}.markdown-body summary:focus{outline:none}.markdown-body details summary{cursor:pointer}.markdown-body details:not([open])>:not(summary){display:none}.markdown-body figure{margin:1em 40px}.markdown-body .mark,.markdown-body mark{background-color:#fff1a7}.vimeo,.youtube{cursor:pointer;display:table;text-align:center;background-position:50%;background-repeat:no-repeat;background-size:contain;background-color:#000;overflow:hidden}.vimeo,.youtube{position:relative;width:100%}.youtube{padding-bottom:56.25%}.vimeo img{width:100%;object-fit:contain;z-index:0}.youtube img{object-fit:cover;z-index:0}.vimeo iframe,.youtube iframe,.youtube img{width:100%;height:100%;position:absolute;top:0;left:0}.vimeo iframe,.youtube iframe{vertical-align:middle;z-index:1}.vimeo .icon,.youtube .icon{position:absolute;height:auto;width:auto;top:50%;left:50%;transform:translate(-50%,-50%);color:#fff;opacity:.3;transition:opacity .2s;z-index:0}.vimeo:hover .icon,.youtube:hover .icon{opacity:.6;transition:opacity .2s}.slideshare .inner,.speakerdeck .inner{position:relative;width:100%}.slideshare .inner iframe,.speakerdeck .inner iframe{position:absolute;top:0;bottom:0;left:0;right:0;width:100%;height:100%}.MJX_Assistive_MathML{display:none}.ui-infobar{position:relative;z-index:2;max-width:760px;margin:25px auto -25px;padding:0 15px;color:#777}.toc .invisable-node{list-style-type:none}.ui-toc{position:fixed;bottom:20px;z-index:998}.ui-toc-label{opacity:.3;background-color:#ccc;border:none;transition:opacity .2s}.ui-toc .open .ui-toc-label{opacity:1;color:#fff;transition:opacity .2s}.ui-toc-label:focus{opacity:.3;background-color:#ccc;color:#000}.ui-toc-label:hover{opacity:1;background-color:#ccc;transition:opacity .2s}.ui-toc-dropdown{margin-top:23px;margin-bottom:20px;padding-left:10px;padding-right:10px;max-width:45vw;width:25vw;max-height:70vh;overflow:auto;text-align:inherit}.ui-toc-dropdown>.toc{max-height:calc(70vh - 100px);overflow:auto}.ui-toc-dropdown[dir=rtl] .nav{padding-right:0;letter-spacing:.0029em}.ui-toc-dropdown a{overflow:hidden;text-overflow:ellipsis;white-space:pre}.ui-toc-dropdown .nav>li>a{display:block;padding:4px 20px;font-size:13px;font-weight:500;color:#767676}.ui-toc-dropdown .nav>li:first-child:last-child > ul,.ui-toc-dropdown .toc.expand ul{display:block}.ui-toc-dropdown .nav>li>a:focus,.ui-toc-dropdown .nav>li>a:hover{padding-left:19px;color:#000;text-decoration:none;background-color:transparent;border-left:1px solid #000}.ui-toc-dropdown[dir=rtl] .nav>li>a:focus,.ui-toc-dropdown[dir=rtl] .nav>li>a:hover{padding-right:19px;border-left:none;border-right:1px solid #000}.ui-toc-dropdown .nav>.active:focus>a,.ui-toc-dropdown .nav>.active:hover>a,.ui-toc-dropdown .nav>.active>a{padding-left:18px;font-weight:700;color:#000;background-color:transparent;border-left:2px solid #000}.ui-toc-dropdown[dir=rtl] .nav>.active:focus>a,.ui-toc-dropdown[dir=rtl] .nav>.active:hover>a,.ui-toc-dropdown[dir=rtl] .nav>.active>a{padding-right:18px;border-left:none;border-right:2px solid #000}.ui-toc-dropdown .nav .nav{display:none;padding-bottom:10px}.ui-toc-dropdown .nav>.active>ul{display:block}.ui-toc-dropdown .nav .nav>li>a{padding-top:1px;padding-bottom:1px;padding-left:30px;font-size:12px;font-weight:400}.ui-toc-dropdown[dir=rtl] .nav .nav>li>a{padding-right:30px}.ui-toc-dropdown .nav .nav>li>ul>li>a{padding-top:1px;padding-bottom:1px;padding-left:40px;font-size:12px;font-weight:400}.ui-toc-dropdown[dir=rtl] .nav .nav>li>ul>li>a{padding-right:40px}.ui-toc-dropdown .nav .nav>li>a:focus,.ui-toc-dropdown .nav .nav>li>a:hover{padding-left:29px}.ui-toc-dropdown[dir=rtl] .nav .nav>li>a:focus,.ui-toc-dropdown[dir=rtl] .nav .nav>li>a:hover{padding-right:29px}.ui-toc-dropdown .nav .nav>li>ul>li>a:focus,.ui-toc-dropdown .nav .nav>li>ul>li>a:hover{padding-left:39px}.ui-toc-dropdown[dir=rtl] .nav .nav>li>ul>li>a:focus,.ui-toc-dropdown[dir=rtl] .nav .nav>li>ul>li>a:hover{padding-right:39px}.ui-toc-dropdown .nav .nav>.active:focus>a,.ui-toc-dropdown .nav .nav>.active:hover>a,.ui-toc-dropdown .nav .nav>.active>a{padding-left:28px;font-weight:500}.ui-toc-dropdown[dir=rtl] .nav .nav>.active:focus>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active:hover>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active>a{padding-right:28px}.ui-toc-dropdown .nav .nav>.active>.nav>.active:focus>a,.ui-toc-dropdown .nav .nav>.active>.nav>.active:hover>a,.ui-toc-dropdown .nav .nav>.active>.nav>.active>a{padding-left:38px;font-weight:500}.ui-toc-dropdown[dir=rtl] .nav .nav>.active>.nav>.active:focus>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active>.nav>.active:hover>a,.ui-toc-dropdown[dir=rtl] .nav .nav>.active>.nav>.active>a{padding-right:38px}.markdown-body{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica Neue,Helvetica,Roboto,Arial,sans-serif}html[lang^=ja] .markdown-body{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica Neue,Helvetica,Roboto,Arial,Hiragino Kaku Gothic Pro,ヒラギノ角ゴ Pro W3,Osaka,Meiryo,メイリオ,MS Gothic,ＭＳ\ ゴシック,sans-serif}html[lang=zh-tw] .markdown-body{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica Neue,Helvetica,Roboto,Arial,PingFang TC,Microsoft JhengHei,微軟正黑,sans-serif}html[lang=zh-cn] .markdown-body{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica Neue,Helvetica,Roboto,Arial,PingFang SC,Microsoft YaHei,微软雅黑,sans-serif}html .markdown-body[lang^=ja]{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica Neue,Helvetica,Roboto,Arial,Hiragino Kaku Gothic Pro,ヒラギノ角ゴ Pro W3,Osaka,Meiryo,メイリオ,MS Gothic,ＭＳ\ ゴシック,sans-serif}html .markdown-body[lang=zh-tw]{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica Neue,Helvetica,Roboto,Arial,PingFang TC,Microsoft JhengHei,微軟正黑,sans-serif}html .markdown-body[lang=zh-cn]{font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica Neue,Helvetica,Roboto,Arial,PingFang SC,Microsoft YaHei,微软雅黑,sans-serif}html[lang^=ja] .ui-toc-dropdown{font-family:Source Sans Pro,Helvetica,Arial,Meiryo UI,MS PGothic,ＭＳ\ Ｐゴシック,sans-serif}html[lang=zh-tw] .ui-toc-dropdown{font-family:Source Sans Pro,Helvetica,Arial,Microsoft JhengHei UI,微軟正黑UI,sans-serif}html[lang=zh-cn] .ui-toc-dropdown{font-family:Source Sans Pro,Helvetica,Arial,Microsoft YaHei UI,微软雅黑UI,sans-serif}html .ui-toc-dropdown[lang^=ja]{font-family:Source Sans Pro,Helvetica,Arial,Meiryo UI,MS PGothic,ＭＳ\ Ｐゴシック,sans-serif}html .ui-toc-dropdown[lang=zh-tw]{font-family:Source Sans Pro,Helvetica,Arial,Microsoft JhengHei UI,微軟正黑UI,sans-serif}html .ui-toc-dropdown[lang=zh-cn]{font-family:Source Sans Pro,Helvetica,Arial,Microsoft YaHei UI,微软雅黑UI,sans-serif}.ui-affix-toc{position:fixed;top:0;max-width:15vw;max-height:70vh;overflow:auto}.back-to-top,.expand-toggle,.go-to-bottom{display:block;padding:4px 10px;margin-top:10px;margin-left:10px;font-size:12px;font-weight:500;color:#999}.back-to-top:focus,.back-to-top:hover,.expand-toggle:focus,.expand-toggle:hover,.go-to-bottom:focus,.go-to-bottom:hover{color:#563d7c;text-decoration:none}.back-to-top,.go-to-bottom{margin-top:0}.ui-user-icon{width:20px;height:20px;display:block;border-radius:3px;margin-top:2px;margin-bottom:2px;margin-right:5px;background-position:50%;background-repeat:no-repeat;background-size:cover}.ui-user-icon.small{width:18px;height:18px;display:inline-block;vertical-align:middle;margin:0 0 .2em}.ui-infobar>small>span{line-height:22px}.ui-infobar>small .dropdown{display:inline-block}.ui-infobar>small .dropdown a:focus,.ui-infobar>small .dropdown a:hover{text-decoration:none}.ui-published-note{color:#337ab7}.ui-published-note .fa{font-size:20px;vertical-align:top}.unselectable{-webkit-user-select:none;-o-user-select:none;user-select:none}@media print{blockquote,div,img,pre,table{page-break-inside:avoid!important}a[href]:after{font-size:12px!important}}.markdown-body.slides{position:relative;z-index:1;color:#222}.markdown-body.slides:before{content:"";display:block;position:absolute;top:0;left:0;right:0;bottom:0;z-index:-1;background-color:currentColor;box-shadow:0 0 0 50vw}.markdown-body.slides section[data-markdown]{position:relative;margin-bottom:1.5em;background-color:#fff;text-align:center}.markdown-body.slides section[data-markdown] code{text-align:left}.markdown-body.slides section[data-markdown]:before{content:"";display:block;padding-bottom:56.23%}.markdown-body.slides section[data-markdown]>div:first-child{position:absolute;top:50%;left:1em;right:1em;transform:translateY(-50%);max-height:100%;overflow:hidden}.markdown-body.slides section[data-markdown]>ul{display:inline-block}.markdown-body.slides>section>section+section:after{content:"";position:absolute;top:-1.5em;right:1em;height:1.5em;border:3px solid #777}body{font-smoothing:subpixel-antialiased!important;-webkit-font-smoothing:subpixel-antialiased!important;-moz-osx-font-smoothing:auto!important;text-shadow:0 0 1em transparent,1px 1px 1.2px rgba(0,0,0,.004);-webkit-overflow-scrolling:touch;letter-spacing:.025em}.focus,:focus{outline:none!important}::-moz-focus-inner{border:0!important}body{font-family:Source Sans Pro,Helvetica,Arial,sans-serif}html[lang^=ja] body{font-family:Source Sans Pro,Helvetica,Arial,Hiragino Kaku Gothic Pro,ヒラギノ角ゴ Pro W3,Osaka,Meiryo,メイリオ,MS Gothic,ＭＳ\ ゴシック,sans-serif}html[lang=zh-tw] body{font-family:Source Sans Pro,Helvetica,Arial,PingFang TC,Microsoft JhengHei,微軟正黑,sans-serif}html[lang=zh-cn] body{font-family:Source Sans Pro,Helvetica,Arial,PingFang SC,Microsoft YaHei,微软雅黑,sans-serif}abbr[title]{border-bottom:none;text-decoration:underline;-webkit-text-decoration:underline dotted;text-decoration:underline dotted}abbr[data-original-title],abbr[title]{cursor:help}body.modal-open{overflow-y:auto;padding-right:0!important} + </style> + <!-- HTML5 shim and Respond.js for IE8 support of HTML5 elements and media queries --> + <!-- WARNING: Respond.js doesn't work if you view the page via file:// --> + <!--[if lt IE 9]> + <script src="https://cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv.min.js" integrity="sha256-3Jy/GbSLrg0o9y5Z5n1uw0qxZECH7C6OQpVBgNFYa0g=" crossorigin="anonymous"></script> + <script src="https://cdnjs.cloudflare.com/ajax/libs/respond.js/1.4.2/respond.min.js" integrity="sha256-g6iAfvZp+nDQ2TdTR/VVKJf3bGro4ub5fvWSWVRi2NE=" crossorigin="anonymous"></script> + <script src="https://cdnjs.cloudflare.com/ajax/libs/es5-shim/4.5.9/es5-shim.min.js" integrity="sha256-8E4Is26QH0bD52WoQpcB+R/tcWQtpzlCojrybUd7Mxo=" crossorigin="anonymous"></script> + <![endif]--> +</head> + +<body> + <div id="doc" class="markdown-body container-fluid comment-enabled" data-hard-breaks="true" style="position: relative;"><h1 id="CbCインターフェースによる-CbCXv6-の書き換え" style=""><a class="anchor hidden-xs" href="#CbCインターフェースによる-CbCXv6-の書き換え" title="CbCインターフェースによる-CbCXv6-の書き換え"><span class="octicon octicon-link"></span></a>CbCインターフェースによる CbCXv6 の書き換え</h1><ul> +<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>CbC による Gears OS の開発</li> +<li>Xv6</li> +<li>CbCXv6 での Paging</li> +<li>CbC インターフェース</li> +<li>評価</li> +<li>まとめ</li> +</ol><hr><h1 id="OS-の信頼性の重要性" style=""><a class="anchor hidden-xs" href="#OS-の信頼性の重要性" title="OS-の信頼性の重要性"><span class="octicon octicon-link"></span></a>OS の信頼性の重要性</h1><ul> +<li>OS のバグは日常生活に支障をきたす +<ul> +<li>パスワードなしで root にアクセスできるバグ</li> +<li>日付設定でコンピュータが壊れる</li> +<li>-> OS自体に信頼性が求められる</li> +</ul> +</li> +</ul><hr><h1 id="OS-の信頼性の重要性1" style=""><a class="anchor hidden-xs" href="#OS-の信頼性の重要性1" title="OS-の信頼性の重要性1"><span class="octicon octicon-link"></span></a>OS の信頼性の重要性</h1><ul> +<li> +<p>全てのOSのコードに対して検証を行うのは困難</p> +<ul> +<li>複雑な機能が多い</li> +<li>短期間のアップデート</li> +</ul> +</li> +<li> +<p>ユーザーが検証を行うこともできない</p> +<ul> +<li>資源管理はOSが行なってる</li> +<li>そもそも資源管理が複雑</li> +<li>アクセスされたり書き換えられるリスク</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>ノーマルレベル +<ul> +<li>ユーザーがプログラミング言語によって記述する部分の処理</li> +</ul> +</li> +<li>メタレベル +<ul> +<li>ユーザーが記述しないOS 側の処理 +<ul> +<li>CPU</li> +<li>メモリ</li> +</ul> +</li> +</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> +<ul> +<li>基本的な処理の単位</li> +</ul> +</li> +<li> +<p>Data Gear</p> +<ul> +<li>データの単位</li> +</ul> +</li> +</ul><hr><h1 id="goto-による継続" style=""><a class="anchor hidden-xs" href="#goto-による継続" title="goto-による継続"><span class="octicon octicon-link"></span></a>goto による継続</h1><ul> +<li>Code Gear の処理の間を goto によって遷移していく</li> +</ul><p><img src="https://i.imgur.com/etfQund.png" alt=""></p><hr><h1 id="Data-Gear-の継続" style=""><a class="anchor hidden-xs" href="#Data-Gear-の継続" title="Data-Gear-の継続"><span class="octicon octicon-link"></span></a>Data Gear の継続</h1><ul> +<li>goto の際に Data Gear も継続される</li> +</ul><p><img src="https://i.imgur.com/3E0DGWA.png" alt=""></p><hr><h1 id="Meta-Code-Gear" style=""><a class="anchor hidden-xs" href="#Meta-Code-Gear" title="Meta-Code-Gear"><span class="octicon octicon-link"></span></a>Meta Code Gear</h1><ul> +<li>実際にはノーマルレベルの間にメタレベルの処理がある</li> +<li>Meta Level では Data Gear の見え方は変わる(Meta Data Gear)</li> +</ul><p><img src="https://i.imgur.com/vy0NxrG.png" alt=""></p><hr><h1 id="状態遷移モデル" style=""><a class="anchor hidden-xs" href="#状態遷移モデル" title="状態遷移モデル"><span class="octicon octicon-link"></span></a>状態遷移モデル</h1><ul> +<li>goto の遷移によって状態遷移モデルに落とし込める</li> +<li>Code Gear に対しての入力に対して期待される出力がされているかで検査して<strong>信頼性を保証する</strong></li> +</ul><hr><h1 id="Agda-による検証" style=""><a class="anchor hidden-xs" href="#Agda-による検証" title="Agda-による検証"><span class="octicon octicon-link"></span></a>Agda による検証</h1><ul> +<li>モデル検査 +<ul> +<li>定理証明支援系である Agda を用いる。</li> +</ul> +</li> +<li>Agda +<ul> +<li>Haure Logic という検証手法を扱える。</li> +</ul> +</li> +</ul><hr><h1 id="Haure-Logic" style=""><a class="anchor hidden-xs" href="#Haure-Logic" title="Haure-Logic"><span class="octicon octicon-link"></span></a>Haure Logic</h1><ul> +<li>検証手法 +<ul> +<li>事前条件を使ってある関数を実行して事後条件を満たすことを確認する</li> +</ul> +</li> +<li>CbCと相性がいい +<ul> +<li>継続に事前条件(Input Data Gear)と事後条件(Output Data Gear)を持たせることができる</li> +</ul> +</li> +</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> +<li>OS の信頼性の1つであるメモリ管理部分を CbC で書き換える +<ul> +<li>Page のバリデーションチェック</li> +<li>サンドボックスによるエクセプション</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> +<p>書き換えを防ぐために見える Data Gear に違いが生じる</p> +</li> +<li> +<p>-> Gears OS のノーマルレベルからメタレベルの記述が記述が煩雑になるためインターフェースを導入</p> +</li> +<li> +<p>機能の入れ替えによる他のメリット</p> +<ul> +<li>機能の入れ替え</li> +<li>Agda による証明</li> +</ul> +</li> +</ul></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"> + <i class="fa fa-bars"></i> + </a> + <ul id="ui-toc" class="ui-toc-dropdown dropdown-menu" aria-labelledby="tocLabel"> + <div class="toc"><ul class="nav"> +<li><a href="#CbCインターフェースによる-CbCXv6-の書き換え" title="CbCインターフェースによる CbCXv6 の書き換え">CbCインターフェースによる CbCXv6 の書き換え</a></li> +<li><a href="#目次0" title="目次">目次</a></li> +<li><a href="#OS-の信頼性の重要性" title="OS の信頼性の重要性">OS の信頼性の重要性</a></li> +<li><a href="#OS-の信頼性の重要性1" title="OS の信頼性の重要性">OS の信頼性の重要性</a></li> +<li><a href="#メタレベルとノーマルレベル" title="メタレベルとノーマルレベル">メタレベルとノーマルレベル</a></li> +<li><a href="#Continuation-based-C" title="Continuation based C">Continuation based C</a></li> +<li><a href="#goto-による継続" title="goto による継続">goto による継続</a></li> +<li><a href="#Data-Gear-の継続" title="Data Gear の継続">Data Gear の継続</a></li> +<li><a href="#Meta-Code-Gear" title="Meta Code Gear">Meta Code Gear</a></li> +<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="#インターフェース" 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> + </div> + </div> + <div id="ui-toc-affix" class="ui-affix-toc ui-toc-dropdown unselectable hidden-print" data-spy="affix" style="top:17px;display:none;" null null> + <div class="toc"><ul class="nav"> +<li><a href="#CbCインターフェースによる-CbCXv6-の書き換え" title="CbCインターフェースによる CbCXv6 の書き換え">CbCインターフェースによる CbCXv6 の書き換え</a></li> +<li><a href="#目次0" title="目次">目次</a></li> +<li><a href="#OS-の信頼性の重要性" title="OS の信頼性の重要性">OS の信頼性の重要性</a></li> +<li><a href="#OS-の信頼性の重要性1" title="OS の信頼性の重要性">OS の信頼性の重要性</a></li> +<li><a href="#メタレベルとノーマルレベル" title="メタレベルとノーマルレベル">メタレベルとノーマルレベル</a></li> +<li><a href="#Continuation-based-C" title="Continuation based C">Continuation based C</a></li> +<li><a href="#goto-による継続" title="goto による継続">goto による継続</a></li> +<li><a href="#Data-Gear-の継続" title="Data Gear の継続">Data Gear の継続</a></li> +<li><a href="#Meta-Code-Gear" title="Meta Code Gear">Meta Code Gear</a></li> +<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="#インターフェース" 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> + <script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.1.1/jquery.min.js" integrity="sha256-hVVnYaiADRTO2PzUGmuLJr8BLUSjGIZsDYGmIJLv2b8=" crossorigin="anonymous"></script> + <script src="https://cdnjs.cloudflare.com/ajax/libs/twitter-bootstrap/3.3.7/js/bootstrap.min.js" integrity="sha256-U5ZEeKfGNOja007MMD3YBI0A3OSZOQbeG6z2f2Y0hu8=" crossorigin="anonymous" defer></script> + <script src="https://cdnjs.cloudflare.com/ajax/libs/gist-embed/2.6.0/gist-embed.min.js" integrity="sha256-KyF2D6xPIJUW5sUDSs93vWyZm+1RzIpKCexxElmxl8g=" crossorigin="anonymous" defer></script> + <script> + var markdown = $(".markdown-body"); + //smooth all hash trigger scrolling + function smoothHashScroll() { + var hashElements = $("a[href^='#']").toArray(); + for (var i = 0; i < hashElements.length; i++) { + var element = hashElements[i]; + var $element = $(element); + var hash = element.hash; + if (hash) { + $element.on('click', function (e) { + // store hash + var hash = this.hash; + if ($(hash).length <= 0) return; + // prevent default anchor click behavior + e.preventDefault(); + // animate + $('body, html').stop(true, true).animate({ + scrollTop: $(hash).offset().top + }, 100, "linear", function () { + // when done, add hash to url + // (default click behaviour) + window.location.hash = hash; + }); + }); + } + } + } + + smoothHashScroll(); + var toc = $('.ui-toc'); + var tocAffix = $('.ui-affix-toc'); + var tocDropdown = $('.ui-toc-dropdown'); + //toc + tocDropdown.click(function (e) { + e.stopPropagation(); + }); + + var enoughForAffixToc = true; + + function generateScrollspy() { + $(document.body).scrollspy({ + target: '' + }); + $(document.body).scrollspy('refresh'); + if (enoughForAffixToc) { + toc.hide(); + tocAffix.show(); + } else { + tocAffix.hide(); + toc.show(); + } + $(document.body).scroll(); + } + + function windowResize() { + //toc right + var paddingRight = parseFloat(markdown.css('padding-right')); + var right = ($(window).width() - (markdown.offset().left + markdown.outerWidth() - paddingRight)); + toc.css('right', right + 'px'); + //affix toc left + var newbool; + var rightMargin = (markdown.parent().outerWidth() - markdown.outerWidth()) / 2; + //for ipad or wider device + if (rightMargin >= 133) { + newbool = true; + var affixLeftMargin = (tocAffix.outerWidth() - tocAffix.width()) / 2; + var left = markdown.offset().left + markdown.outerWidth() - affixLeftMargin; + tocAffix.css('left', left + 'px'); + } else { + newbool = false; + } + if (newbool != enoughForAffixToc) { + enoughForAffixToc = newbool; + generateScrollspy(); + } + } + $(window).resize(function () { + windowResize(); + }); + $(document).ready(function () { + windowResize(); + generateScrollspy(); + }); + + //remove hash + function removeHash() { + window.location.hash = ''; + } + + var backtotop = $('.back-to-top'); + var gotobottom = $('.go-to-bottom'); + + backtotop.click(function (e) { + e.preventDefault(); + e.stopPropagation(); + if (scrollToTop) + scrollToTop(); + removeHash(); + }); + gotobottom.click(function (e) { + e.preventDefault(); + e.stopPropagation(); + if (scrollToBottom) + scrollToBottom(); + removeHash(); + }); + + var toggle = $('.expand-toggle'); + var tocExpand = false; + + checkExpandToggle(); + toggle.click(function (e) { + e.preventDefault(); + e.stopPropagation(); + tocExpand = !tocExpand; + checkExpandToggle(); + }) + + function checkExpandToggle () { + var toc = $('.ui-toc-dropdown .toc'); + var toggle = $('.expand-toggle'); + if (!tocExpand) { + toc.removeClass('expand'); + toggle.text('Expand all'); + } else { + toc.addClass('expand'); + toggle.text('Collapse all'); + } + } + + function scrollToTop() { + $('body, html').stop(true, true).animate({ + scrollTop: 0 + }, 100, "linear"); + } + + function scrollToBottom() { + $('body, html').stop(true, true).animate({ + scrollTop: $(document.body)[0].scrollHeight + }, 100, "linear"); + } + </script> +</body> + +</html>
--- a/thsis_paging.mm Thu Feb 06 18:40:10 2020 +0900 +++ b/thsis_paging.mm Fri Feb 07 16:53:09 2020 +0900 @@ -1,6 +1,6 @@ <map version="1.0.1"> <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> -<node CREATED="1580099260489" ID="ID_1614065797" MODIFIED="1580214673106" TEXT="CbC インターフェースによる CbCXv6 の書き換え"> +<node CREATED="1580099260489" ID="ID_1614065797" MODIFIED="1580994945568" TEXT="CbC インターフェースによる CbCXv6 の書き換え"> <node CREATED="1580207637653" ID="ID_721168585" MODIFIED="1580207641017" POSITION="right" TEXT="英文タイトル"> <node CREATED="1580207641694" ID="ID_182987953" MODIFIED="1580207649805" TEXT="Rewriting CbCXv6 by CbC interface "/> </node> @@ -111,7 +111,10 @@ <icon BUILTIN="idea"/> <icon BUILTIN="full-1"/> </node> -<node CREATED="1580979068578" ID="ID_1698688073" MODIFIED="1580979075066" TEXT="exec.cbc"/> +<node CREATED="1580979068578" ID="ID_1698688073" MODIFIED="1580979079895" TEXT="exec.cbc"> +<icon BUILTIN="idea"/> +<icon BUILTIN="full-1"/> +</node> </node> <node CREATED="1578979830870" ID="ID_251771531" MODIFIED="1580979001896" POSITION="right" TEXT="Paging の評価"> <icon BUILTIN="idea"/> @@ -127,6 +130,7 @@ <node CREATED="1580462109134" ID="ID_273350504" MODIFIED="1580558686526" TEXT="proc.cbc実装(dummy後)"/> <node CREATED="1580462212464" ID="ID_1766947302" MODIFIED="1580462217795" TEXT="Xv6頭に入れる"/> <node CREATED="1580462094519" ID="ID_1481533529" MODIFIED="1580462105250" TEXT="参考文献読む"/> +<node CREATED="1580994919390" ID="ID_1863120896" MODIFIED="1580994922714" TEXT="スライド作る"/> </node> </node> </map>