# HG changeset patch # User tobaru # Date 1581061989 -32400 # Node ID 6afd90dba6db2829ab539df3b0dc1470a5d9ce74 # Parent b35cb5777a5cdb95d4ad7bb5b333499385f36ebf slide chapter1 diff -r b35cb5777a5c -r 6afd90dba6db paper/GearsOS.tex --- 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} diff -r b35cb5777a5c -r 6afd90dba6db paper/fig/Meta_Code_Gear.graffle Binary file paper/fig/Meta_Code_Gear.graffle has changed diff -r b35cb5777a5c -r 6afd90dba6db paper/fig/Meta_Code_Gear.pdf Binary file paper/fig/Meta_Code_Gear.pdf has changed diff -r b35cb5777a5c -r 6afd90dba6db paper/fig/normal_Data.pdf Binary file paper/fig/normal_Data.pdf has changed diff -r b35cb5777a5c -r 6afd90dba6db paper/master_paper.aux --- 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 } diff -r b35cb5777a5c -r 6afd90dba6db paper/master_paper.lof --- 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@ } diff -r b35cb5777a5c -r 6afd90dba6db paper/master_paper.log --- 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). diff -r b35cb5777a5c -r 6afd90dba6db paper/master_paper.lol --- 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}% diff -r b35cb5777a5c -r 6afd90dba6db paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r b35cb5777a5c -r 6afd90dba6db paper/master_paper.synctex.gz Binary file paper/master_paper.synctex.gz has changed diff -r b35cb5777a5c -r 6afd90dba6db paper/master_paper.tex --- 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} diff -r b35cb5777a5c -r 6afd90dba6db paper/master_paper.toc --- 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}% diff -r b35cb5777a5c -r 6afd90dba6db paper/memory_manage.tex --- 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 のバリデーションをチェックしたり、サンドボックスによる信頼性の保証を行えるようになる。また、適切な記述をすれば最適な資源管理にも繋がる。 - - - - diff -r b35cb5777a5c -r 6afd90dba6db slide/CbCXv6.html --- /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 @@ + + + + + + + + + + + + + CbCインターフェースによる CbCXv6 の書き換え - HackMD + + + + + + + + + + + + + + + + + +

CbCインターフェースによる CbCXv6 の書き換え

目次

    +
  1. OS の信頼性の保障
    2. +
  2. CbC による Gears OS の開発
    3. +
  3. Xv6
    4. +
  4. CbCXv6 での Paging
    5. +
  5. CbC インターフェース
    6. +
  6. 評価
    7. +
  7. まとめ
    8. +

OS の信頼性の重要性

OS の信頼性の重要性

メタレベルとノーマルレベル

Continuation based C

goto による継続

Data Gear の継続

Meta Code Gear

状態遷移モデル

Agda による検証

Haure Logic

Geas OS

メモリ管理

インターフェース

+ + + + + + + + + diff -r b35cb5777a5c -r 6afd90dba6db slide/fig/Meta_Code_Gear.graffle Binary file slide/fig/Meta_Code_Gear.graffle has changed diff -r b35cb5777a5c -r 6afd90dba6db slide/fig/Meta_Code_Gear.pdf Binary file slide/fig/Meta_Code_Gear.pdf has changed diff -r b35cb5777a5c -r 6afd90dba6db slide/fig/Meta_Code_Gear.png Binary file slide/fig/Meta_Code_Gear.png has changed diff -r b35cb5777a5c -r 6afd90dba6db slide/fig/normal_Code.graffle Binary file slide/fig/normal_Code.graffle has changed diff -r b35cb5777a5c -r 6afd90dba6db slide/fig/normal_Code.pdf Binary file slide/fig/normal_Code.pdf has changed diff -r b35cb5777a5c -r 6afd90dba6db slide/fig/normal_Code.png Binary file slide/fig/normal_Code.png has changed diff -r b35cb5777a5c -r 6afd90dba6db slide/fig/normal_Data.graffle Binary file slide/fig/normal_Data.graffle has changed diff -r b35cb5777a5c -r 6afd90dba6db slide/fig/normal_Data.pdf Binary file slide/fig/normal_Data.pdf has changed diff -r b35cb5777a5c -r 6afd90dba6db slide/fig/normal_Data.png Binary file slide/fig/normal_Data.png has changed diff -r b35cb5777a5c -r 6afd90dba6db thsis_paging.mm --- 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 @@ - + @@ -111,7 +111,10 @@ - + + + + @@ -127,6 +130,7 @@ + diff -r b35cb5777a5c -r 6afd90dba6db thsis_paging.pdf Binary file thsis_paging.pdf has changed