changeset 10:a882e390f9a2

dummy, reference, thanks
author tobaru
date Sun, 02 Feb 2020 19:47:49 +0900
parents dfb52a12c5a1
children f7ed2b4874f4
files paper/Paging.tex paper/Xv6.tex paper/cbc_interface.tex paper/master_paper.aux 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/reference.bib paper/thanks.tex thsis_paging.mm
diffstat 13 files changed, 342 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/paper/Paging.tex	Fri Jan 31 23:20:46 2020 +0900
+++ b/paper/Paging.tex	Sun Feb 02 19:47:49 2020 +0900
@@ -9,6 +9,7 @@
 
 \section{Paging}
   メモリ管理の手法に、Paging がある。Paging ではメモリを Page と呼ばれる固定長の単位に分割し、メモリとスワップ領域で Page を入れ替えて管理を行う。
+\par
 
 
  \begin{figure}[ht]
--- a/paper/Xv6.tex	Fri Jan 31 23:20:46 2020 +0900
+++ b/paper/Xv6.tex	Sun Feb 02 19:47:49 2020 +0900
@@ -42,3 +42,6 @@
         [SYS_close]   =sys_close,
 };
 \end{lstlisting}
+
+\section{Xv6-rpi}
+
--- a/paper/cbc_interface.tex	Fri Jan 31 23:20:46 2020 +0900
+++ b/paper/cbc_interface.tex	Sun Feb 02 19:47:49 2020 +0900
@@ -437,4 +437,80 @@
 \end{lstlisting}
 
 
-\section{dummy による実行}
+\section{インターフェースの呼び出し}
+ CbC の場合 goto による遷移を行うので、関数呼び出しのように goto 以降のコードを実行できない。
+例として、\ref{cbc_goto} の16行目のように goto によってインターフェースで定義した命令を行うと、戻ってこれないため17行目以降が実行されなくなる。
+
+
+\begin{lstlisting}[frame=lrbt,label=cbc_goto,caption={\footnotesize cbc インターフェースのgoto}]
+
+void userinit(void)
+{
+    struct proc* p;
+    extern char _binary_initcode_start[], _binary_initcode_size[];
+
+    p = allocproc();
+    initContext(&p->cbc_context);
+
+    initproc = p;
+
+    if((p->pgdir = kpt_alloc()) == NULL) {
+        panic("userinit: out of memory?");
+    }
+
+    goto cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
+    p->sz = PTE_SZ;
+
+    // craft the trapframe as if
+    memset(p->tf, 0, sizeof(*p->tf));
+
+
+\end{lstlisting}
+
+
+
+
+\begin{lstlisting}[frame=lrbt,label=impl_vm_private,caption={\footnotesize vm private の実装}]
+
+
+void dummy(struct proc *p, char _binary_initcode_start[], char _binary_initcode_size[])
+{
+    // inituvm(p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
+    goto cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
+
+}
+
+
+
+__ncode cbc_init_vmm_dummy(struct Context* cbc_context, struct proc* p, pde_t* pgdir, char* init, uint sz){//:skip
+
+    struct vm* vm = createvm_impl(cbc_context);
+    // goto vm->init_vmm(vm, pgdir, init, sz , vm->void_ret);
+        Gearef(cbc_context, vm)->vm = (union Data*) vm;
+        Gearef(cbc_context, vm)->pgdir = pgdir;
+        Gearef(cbc_context, vm)->init = init;
+        Gearef(cbc_context, vm)->sz = sz ;
+        Gearef(cbc_context, vm)->next = C_vm_void_ret ;
+    goto meta(cbc_context, vm->init_inituvm);
+}
+
+
+void userinit(void)
+{
+    struct proc* p;
+    extern char _binary_initcode_start[], _binary_initcode_size[];
+
+    p = allocproc();
+    initContext(&p->cbc_context);
+
+    initproc = p;
+
+    if((p->pgdir = kpt_alloc()) == NULL) {
+        panic("userinit: out of memory?");
+    }
+
+    dummy(p, _binary_initcode_start, _binary_initcode_size);
+
+
+
+\end{lstlisting}
--- a/paper/master_paper.aux	Fri Jan 31 23:20:46 2020 +0900
+++ b/paper/master_paper.aux	Sun Feb 02 19:47:49 2020 +0900
@@ -21,6 +21,7 @@
 \@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{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
@@ -44,5 +45,29 @@
 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.3}\footnotesize  vm private のヘッダーファイル}{15}\protected@file@percent }
 \newlabel{impl_vm_private}{{5.4}{17}}
 \@writefile{lol}{\contentsline {lstlisting}{\numberline {5.4}\footnotesize  vm private の実装}{17}\protected@file@percent }
-\@writefile{toc}{\contentsline {section}{\numberline {5.4}dummy による実行}{20}\protected@file@percent }
-\@writefile{toc}{\contentsline {chapter}{付録}{20}\protected@file@percent }
+\@writefile{toc}{\contentsline {section}{\numberline {5.4}インターフェースの呼び出し}{20}\protected@file@percent }
+\newlabel{cbc_goto}{{5.5}{20}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.5}\footnotesize  cbc インターフェースのgoto}{20}\protected@file@percent }
+\newlabel{impl_vm_private}{{5.6}{20}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.6}\footnotesize  vm private の実装}{20}\protected@file@percent }
+\@writefile{toc}{\contentsline {chapter}{謝辞}{21}\protected@file@percent }
+\citation{*}
+\bibdata{reference}
+\bibcite{os}{1}
+\bibcite{rpi}{2}
+\bibcite{xv6rpi}{3}
+\bibcite{cbc}{4}
+\bibcite{moggi-monad}{5}
+\bibcite{Yang:2010:SLI:1806596.1806610}{6}
+\bibcite{Klein:2009:SFV:1629575.1629596}{7}
+\bibcite{Sigurbjarnarson:2016:PVF:3026877.3026879}{8}
+\bibcite{agda-ryokka}{9}
+\bibcite{agda}{10}
+\@writefile{toc}{\contentsline {chapter}{参考文献}{23}\protected@file@percent }
+\bibcite{llvm}{11}
+\bibcite{gcc}{12}
+\bibcite{gears}{13}
+\bibcite{arm}{14}
+\bibcite{xv6}{15}
+\bibstyle{junsrt}
+\@writefile{toc}{\contentsline {chapter}{付録}{24}\protected@file@percent }
--- a/paper/master_paper.log	Fri Jan 31 23:20:46 2020 +0900
+++ b/paper/master_paper.log	Sun Feb 02 19:47:49 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)  31 JAN 2020 21:31
+This is e-pTeX, Version 3.14159265-p3.8.2-190131-2.6 (utf8.euc) (TeX Live 2019) (preloaded format=platex 2020.1.16)  2 FEB 2020 19:36
 entering extended mode
  restricted \write18 enabled.
  file:line:error style messages enabled.
@@ -216,7 +216,11 @@
 
 
 Writing index file master_paper.idx
-(./master_paper.aux)
+(./master_paper.aux
+
+LaTeX Warning: Label `impl_vm_private' multiply defined.
+
+)
 \openout1 = `master_paper.aux'.
 
 LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 65.
@@ -395,19 +399,58 @@
 第 5 章(11ページ)
 [11
 
-] [12] [13] [14] [15] [16] [17] [18]) [19] [20] (./master_paper.aux)
+] [12] [13] [14] [15] [16] [17] [18] [19] [20]) (./thanks.tex [21])
+(./master_paper.bbl [22
+
+]
+Underfull \hbox (badness 10000) in paragraph at lines 9--11
+[]\OT1/cmr/m/n/12 Raspberry Pi \JY1/hmc/m/n/12 ― \OT1/cmr/m/n/12 Teach, Learn,
+ and Make with Rasp-berry Pi.
+ []
+
+LaTeX Font Info:    Font shape `JT1/hgt/m/n' will be
+(Font)              scaled to size 11.54663pt on input line 20.
+LaTeX Font Info:    Font shape `JY1/hgt/m/n' will be
+(Font)              scaled to size 11.54663pt on input line 20.
+
+LaTeX Font Warning: Font shape `JT1/hgt/m/it' undefined
+(Font)              using `JT1/hgt/m/n' instead on input line 20.
+
+
+LaTeX Font Warning: Font shape `JY1/hgt/m/it' undefined
+(Font)              using `JY1/hgt/m/n' instead on input line 20.
+
+LaTeX Font Info:    Font shape `JT1/hgt/m/it' will be
+(Font)              scaled to size 11.54663pt on input line 25.
+LaTeX Font Info:    Font shape `JY1/hgt/m/it' will be
+(Font)              scaled to size 11.54663pt on input line 25.
+[23
+
+]
+Overfull \hbox (8.48145pt too wide) in paragraph at lines 81--84
+[]\OT1/cmr/m/n/12 ARM Ar-chi-tec-ture Ref-er-ence Man-ual.  \OT1/cmr/m/it/12 ht
+tp://infocenter.arm.com/help/topic/com.arm. 
+ []
+
+) [24] (./master_paper.aux)
 
 LaTeX Font Warning: Size substitutions with differences
 (Font)              up to 1.28pt have occurred.
 
+
+LaTeX Font Warning: Some font shapes were not available, defaults substituted.
+
+
+LaTeX Warning: There were multiply-defined labels.
+
  ) 
 Here is how much of TeX's memory you used:
- 6319 strings out of 493985
- 89633 string characters out of 6166648
- 368175 words of memory out of 5000000
- 10637 multiletter control sequences out of 15000+600000
- 16577 words of font info for 84 fonts, out of 8000000 for 9000
+ 6352 strings out of 493985
+ 90039 string characters out of 6166648
+ 368228 words of memory out of 5000000
+ 10662 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
  32i,11n,36p,470b,1800s stack positions out of 5000i,500n,10000p,200000b,80000s
 
-Output written on master_paper.dvi (27 pages, 98212 bytes).
+Output written on master_paper.dvi (31 pages, 112664 bytes).
--- a/paper/master_paper.lol	Fri Jan 31 23:20:46 2020 +0900
+++ b/paper/master_paper.lol	Sun Feb 02 19:47:49 2020 +0900
@@ -4,3 +4,5 @@
 \contentsline {lstlisting}{\numberline {5.2}\footnotesize vm インターフェースの実装}{12}%
 \contentsline {lstlisting}{\numberline {5.3}\footnotesize vm private のヘッダーファイル}{15}%
 \contentsline {lstlisting}{\numberline {5.4}\footnotesize vm private の実装}{17}%
+\contentsline {lstlisting}{\numberline {5.5}\footnotesize cbc インターフェースのgoto}{20}%
+\contentsline {lstlisting}{\numberline {5.6}\footnotesize vm private の実装}{20}%
Binary file paper/master_paper.pdf has changed
Binary file paper/master_paper.synctex.gz has changed
--- a/paper/master_paper.tex	Fri Jan 31 23:20:46 2020 +0900
+++ b/paper/master_paper.tex	Sun Feb 02 19:47:49 2020 +0900
@@ -103,13 +103,14 @@
 
 % 
 % %謝辞
-% \addcontentsline{toc}{chapter}{謝辞}
-% \input{thanks.tex}
+\addcontentsline{toc}{chapter}{謝辞}
+\input{thanks.tex}
 % 
-% %参考文献
-% \nocite{*}
-% \bibliographystyle{junsrt}
-% \bibliography{reference}
+%参考文献
+\nocite{*}
+\bibliography{reference}
+\bibliographystyle{junsrt}
+
 
 %付録
 \addcontentsline{toc}{chapter}{付録}
--- a/paper/master_paper.toc	Fri Jan 31 23:20:46 2020 +0900
+++ b/paper/master_paper.toc	Sun Feb 02 19:47:49 2020 +0900
@@ -6,6 +6,7 @@
 \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}%
@@ -15,5 +16,7 @@
 \contentsline {section}{\numberline {5.1}インターフェースの定義}{11}%
 \contentsline {section}{\numberline {5.2}インターフェースの実装}{12}%
 \contentsline {section}{\numberline {5.3}インターフェース内の private メソッド}{15}%
-\contentsline {section}{\numberline {5.4}dummy による実行}{20}%
-\contentsline {chapter}{付録}{20}%
+\contentsline {section}{\numberline {5.4}インターフェースの呼び出し}{20}%
+\contentsline {chapter}{謝辞}{21}%
+\contentsline {chapter}{参考文献}{23}%
+\contentsline {chapter}{付録}{24}%
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/reference.bib	Sun Feb 02 19:47:49 2020 +0900
@@ -0,0 +1,160 @@
+@article{os,
+    author = {Andrew S.Tanenbaum, Herbert Bos},
+    title = "{Modern Operating Systems}",
+    publisher = {PEASON},
+    year = {2015},
+}
+
+@misc{rpi,
+title     = "{Raspberry Pi — Teach, Learn, and Make with Raspberry Pi}",
+howpublished    = {https://www.raspberrypi.org}
+}
+
+@misc{xv6rpi,
+author    = {Zhiyi Wang},
+title     = "{xv6-rpi}",
+howpublished      = "{https://code.google.com/archive/p/xv6-rpi/}",
+year      = {2013}
+}
+
+@article{
+    cbc,
+    author = "Kaito TOKKMORI and Shinji KONO",
+    title = "Implementing Continuation based language in LLVM and Clang",
+    journal = "LOLA 2015",
+    month = "July",
+    year = 2015
+}
+
+@article{moggi-monad,
+    author     = {Moggi, Eugenio},
+    title      = {Notions of Computation and Monads},
+    journal    = {Inf. Comput.},
+    issue_date = {July 1991},
+    volume     = {93},
+    number     = {1},
+    month      = jul,
+    year       = {1991},
+    issn       = {0890-5401},
+    pages      = {55--92},
+    numpages   = {38},
+    url        = {http://dx.doi.org/10.1016/0890-5401(91)90052-4},
+    doi        = {10.1016/0890-5401(91)90052-4},
+    acmid      = {116984},
+    publisher  = {Academic Press, Inc.},
+    address    = {Duluth, MN, USA},
+}
+
+@inproceedings{Yang:2010:SLI:1806596.1806610,
+ author = {Yang, Jean and Hawblitzel, Chris},
+ title = {Safe to the Last Instruction: Automated Verification of a Type-safe Operating System},
+ booktitle = {Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation},
+ series = {PLDI '10},
+ year = {2010},
+ isbn = {978-1-4503-0019-3},
+ location = {Toronto, Ontario, Canada},
+ pages = {99--110},
+ numpages = {12},
+ url = {http://doi.acm.org/10.1145/1806596.1806610},
+ doi = {10.1145/1806596.1806610},
+ acmid = {1806610},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {operating system, run-time system, type safety, verification},
+}
+
+@inproceedings{Klein:2009:SFV:1629575.1629596,
+ author = {Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and Sewell, Thomas and Tuch, Harvey and Winwood, Simon},
+ title = {seL4: Formal Verification of an OS Kernel},
+ booktitle = {Proceedings of the ACM SIGOPS 22Nd Symposium on Operating Systems Principles},
+ series = {SOSP '09},
+ year = {2009},
+ isbn = {978-1-60558-752-3},
+ location = {Big Sky, Montana, USA},
+ pages = {207--220},
+ numpages = {14},
+ url = {http://doi.acm.org/10.1145/1629575.1629596},
+ doi = {10.1145/1629575.1629596},
+ acmid = {1629596},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {isabelle/hol, l4, microkernel, sel4},
+} 
+
+@inproceedings{Sigurbjarnarson:2016:PVF:3026877.3026879,
+ author = {Sigurbjarnarson, Helgi and Bornholt, James and Torlak, Emina and Wang, Xi},
+ title = {Push-button Verification of File Systems via Crash Refinement},
+ booktitle = {Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation},
+ series = {OSDI'16},
+ year = {2016},
+ isbn = {978-1-931971-33-1},
+ location = {Savannah, GA, USA},
+ pages = {1--16},
+ numpages = {16},
+ url = {http://dl.acm.org/citation.cfm?id=3026877.3026879},
+ acmid = {3026879},
+ publisher = {USENIX Association},
+ address = {Berkeley, CA, USA},
+}
+
+@article{
+    agda-ryokka,
+    author = "Hokama MASATAKA and Shinji KONO",
+    title = "GearsOS の Hoare Logic をベースにした検証手法",
+    journal = "ソフトウェアサイエンス研究会",
+    month = "Jan",
+    year = 2019
+}
+
+@inproceedings{agda,
+ author = {Norell, Ulf},
+ title = {Dependently Typed Programming in Agda},
+ booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation},
+ series = {TLDI '09},
+ year = {2009},
+ isbn = {978-1-60558-420-1},
+ location = {Savannah, GA, USA},
+ pages = {1--2},
+ numpages = {2},
+ url = {http://doi.acm.org/10.1145/1481861.1481862},
+ doi = {10.1145/1481861.1481862},
+ acmid = {1481862},
+ publisher = {ACM},
+ address = {New York, NY, USA},
+ keywords = {dependent types, programming},
+}
+
+@InProceedings{llvm,
+author    = {Chris Lattner and Vikram Adve},
+title     = "{LLVM: A Compilation Framework for Lifelong Program Analysis \& Transformation}",
+booktitle = "{Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO'04)}",
+address   = {Palo Alto, California},
+month     = {Mar},
+year      = {2004}
+}
+
+@manual{gcc,
+author = "{GNU Compiler Collection (GCC) Internals}",
+title ="{http://gcc.gnu.org/onlinedocs/gccint/}",
+}
+
+@article{
+    gears,
+    author = "河野 真治 and 伊波 立樹 and  東恩納 琢偉",
+    title = "Code Gear、Data Gear に基づく OS のプロトタイプ",
+    journal = "情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)",
+    month = "May",
+    year = 2016
+}
+
+@manual{arm,
+author     = "{ARM Architecture Reference Manual}",
+title  = "{http://infocenter.arm.com/help/topic/com.arm.\\doc.subset.architecture.reference/index.html}"
+}
+
+@misc{xv6,
+author     = "{Russ Cox, Frans Kaashoek, Robert Morris}",
+title    = {xv6 a simple, Unix-like teaching operating system},
+howpublished   = {https://pdos.csail.mit.edu/6.828/2018/xv6/book-rev11.pdf},
+}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/thanks.tex	Sun Feb 02 19:47:49 2020 +0900
@@ -0,0 +1,6 @@
+\chapter*{謝辞}
+
+\begin{flushright}
+    2020年 3月 \\ 桃原 優
+\end{flushright}
+
--- a/thsis_paging.mm	Fri Jan 31 23:20:46 2020 +0900
+++ b/thsis_paging.mm	Sun Feb 02 19:47:49 2020 +0900
@@ -51,6 +51,7 @@
 <icon BUILTIN="idea"/>
 <icon BUILTIN="full-1"/>
 <node CREATED="1580206122141" ID="ID_263443526" MODIFIED="1580206132135" TEXT="Console &#x63a5;&#x7d9a;&#x66f8;&#x304f;"/>
+<node CREATED="1580474892496" ID="ID_1445151339" MODIFIED="1580474900889" TEXT="xv6-rpi&#x66f8;&#x304f;&#xff1f;"/>
 </node>
 </node>
 <node CREATED="1578979785550" ID="ID_1231580257" MODIFIED="1580292616993" POSITION="right" TEXT="CbCXv6&#x3067;&#x306e; Paging&#x306e;&#x66f8;&#x304d;&#x63db;&#x3048;">
@@ -102,7 +103,7 @@
 </node>
 <node CREATED="1580462062575" ID="ID_76123952" MODIFIED="1580462065622" POSITION="right" TEXT="&#x53c2;&#x8003;&#x6587;&#x732e;"/>
 <node CREATED="1580462087263" ID="ID_1850863059" MODIFIED="1580462091208" POSITION="left" TEXT="&#x3084;&#x308b;&#x3053;&#x3068;">
-<node CREATED="1580462109134" ID="ID_273350504" MODIFIED="1580462112678" TEXT="&#x5b9f;&#x88c5;"/>
+<node CREATED="1580462109134" ID="ID_273350504" MODIFIED="1580558686526" TEXT="proc.cbc&#x5b9f;&#x88c5;(dummy&#x5f8c;)"/>
 <node CREATED="1580462212464" ID="ID_1766947302" MODIFIED="1580462217795" TEXT="Xv6&#x982d;&#x306b;&#x5165;&#x308c;&#x308b;"/>
 <node CREATED="1580462094519" ID="ID_1481533529" MODIFIED="1580462105250" TEXT="&#x53c2;&#x8003;&#x6587;&#x732e;&#x8aad;&#x3080;"/>
 </node>