Mercurial > hg > Papers > 2020 > tobaru-master
changeset 15:b7ae3aa6548e
English abstract
| author | tobaru |
|---|---|
| date | Thu, 06 Feb 2020 18:38:47 +0900 |
| parents | 3952ffd84dfe |
| children | b35cb5777a5c |
| files | paper/abstract.tex paper/fig/meta_cg_dg.pdf paper/master_paper.log paper/master_paper.pdf paper/master_paper.synctex.gz thsis_paging.mm |
| diffstat | 6 files changed, 38 insertions(+), 21 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/abstract.tex Thu Feb 06 17:45:09 2020 +0900 +++ b/paper/abstract.tex Thu Feb 06 18:38:47 2020 +0900 @@ -1,10 +1,10 @@ \chapter*{要旨} -OS を要する機器に依存している現代では、OS のバグは日常に支障を来たすことに繋がる。 +OS を要する機器に依存している現代では、OS のバグは日常生活に支障を来たすことに繋がる。 OS 自体に信頼性が求められるが、機能が多く短期間のアップデートが必要な OS では、全てのコードに対して何度も検証を行うのは困難である。 本研究室で開発したメタレベルの記述ができる CbC という言語を用いて OS の信頼性を保証するために Gears OS を開発中である。 -本研究での Gears OS の実装は、CbC で軽量なハードウェアでも動かせるように Arm のバイナリを 出力する OS である Xv6 を参考に行っている。 +本研究での Gears OS の実装は、Xv6 というOSを参考に行っている。 CbC は継続を中心とした言語であるため、状態遷移モデルに落とし込むことができる。 状態遷移の1つ1つの関数に対して検証を行うことで OS の機能の信頼性を保証することができる。 @@ -19,6 +19,17 @@ % 既存の Gears OS でのメモリ管理では単に Page Table Entry をコピーする Fork を実装しているが、 \chapter*{Abstract} -% 英語 +OS Bugs lead to hinder daily life, In the modern times of relying on devices that require an OS. +OS requires reliability. But It is defficult to verify all the code many times on an OS that has meny functions and requires short-term updates. +Our laboratory developing an OS called Gears OS to guarantee reliability. +Gears OS uses a programming language called CbC that can write meta-level. +GearsOS implementation is based on Xv6. +CbC is a language with a focus on continuation, it can be dropped into a state transition model. +The reliability of OS functions can be guaranteed by verifying each function of the state transition. +But, The description of continuation becomes complicated for data that looks defferent between the normal-level and the meta-level. +In this research, mojularization using interfaces. +Interface formalized and can be flexibly reused. +This paper describes and discusses the interface and implementation of the memory management part, which is the basis of OS reliability. +
--- a/paper/master_paper.log Thu Feb 06 17:45:09 2020 +0900 +++ b/paper/master_paper.log Thu Feb 06 18:38:47 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 17:42 +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 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -489,4 +489,4 @@ 107 hyphenation exceptions out of 8191 33i,11n,36p,410b,1835s stack positions out of 5000i,500n,10000p,200000b,80000s -Output written on master_paper.dvi (55 pages, 240400 bytes). +Output written on master_paper.dvi (55 pages, 241604 bytes).
--- a/thsis_paging.mm Thu Feb 06 17:45:09 2020 +0900 +++ b/thsis_paging.mm Thu Feb 06 18:38:47 2020 +0900 @@ -7,8 +7,11 @@ <node CREATED="1580462003106" ID="ID_394129445" MODIFIED="1580462034141" POSITION="right" TEXT="abdtract"> <icon BUILTIN="idea"/> <node CREATED="1580462021212" ID="ID_890799242" MODIFIED="1580462025706" TEXT="最後に書く"> -<node CREATED="1580782397745" ID="ID_79398832" MODIFIED="1580782421011" TEXT="メモリ管理よりインターフェースの内容を書く"/> -<node CREATED="1580887424881" ID="ID_1159285917" MODIFIED="1580887433476" TEXT="OSのバグ例調べる"> +<node CREATED="1580782397745" ID="ID_79398832" MODIFIED="1580978751187" TEXT="メモリ管理よりインターフェースの内容を書く"> +<icon BUILTIN="button_ok"/> +</node> +<node CREATED="1580887424881" ID="ID_1159285917" MODIFIED="1580978753417" TEXT="OSのバグ例調べる"> +<icon BUILTIN="button_ok"/> <node CREATED="1580887434966" ID="ID_306328321" MODIFIED="1580887444734" TEXT="そこから目的につなげる"/> </node> </node> @@ -32,12 +35,11 @@ <node CREATED="1580108797610" ID="ID_1365788482" MODIFIED="1580108810835" TEXT="Code Gear, Data Gear"/> <node CREATED="1580107798502" ID="ID_1870725834" MODIFIED="1580107827464" TEXT="Meta の説明と遷移図"/> <node CREATED="1580107483687" ID="ID_1285374455" MODIFIED="1580107511777" TEXT="Context"> -<node CREATED="1580782925878" ID="ID_720702973" MODIFIED="1580782933799" TEXT="ソースコードの説明"> -<icon BUILTIN="idea"/> +<node CREATED="1580782925878" ID="ID_720702973" MODIFIED="1580978765191" TEXT="ソースコードの説明"> +<icon BUILTIN="button_ok"/> </node> -<node CREATED="1580783543307" ID="ID_38181422" MODIFIED="1580806862676" TEXT="enum Code Gear の番号と Contextの初期化"> -<icon BUILTIN="idea"/> -<icon BUILTIN="full-1"/> +<node CREATED="1580783543307" ID="ID_38181422" MODIFIED="1580978740364" TEXT="enum Code Gear の番号と Contextの初期化"> +<icon BUILTIN="button_ok"/> </node> </node> <node CREATED="1580188243030" ID="ID_1781662530" MODIFIED="1580460456622" TEXT="Meta Computation"> @@ -57,11 +59,12 @@ <icon BUILTIN="idea"/> <icon BUILTIN="full-2"/> </node> -<node CREATED="1580107648436" ID="ID_422947198" MODIFIED="1580461790590" TEXT="Raspberry Pi は必要ない??"> +<node CREATED="1580107648436" ID="ID_422947198" MODIFIED="1580978775391" TEXT="Raspberry Pi は必要ない??"> +<node CREATED="1580206122141" ID="ID_263443526" MODIFIED="1580978782048" TEXT="Console 接続書く"> <icon BUILTIN="idea"/> -<icon BUILTIN="full-1"/> -<node CREATED="1580206122141" ID="ID_263443526" MODIFIED="1580206132135" TEXT="Console 接続書く"/> -<node CREATED="1580474892496" ID="ID_1445151339" MODIFIED="1580474900889" TEXT="xv6-rpi書く？"> +</node> +<node CREATED="1580474892496" ID="ID_1445151339" MODIFIED="1580978779299" TEXT="xv6-rpi書く？"> +<icon BUILTIN="button_ok"/> <node CREATED="1580806887593" ID="ID_300622813" MODIFIED="1580806893688" TEXT="crosscompile"/> </node> </node> @@ -80,9 +83,8 @@ </node> <node CREATED="1580365409191" ID="ID_421799143" MODIFIED="1580365426704" POSITION="right" TEXT="CbC インターフェース"> <node CREATED="1580206394524" ID="ID_1210911937" MODIFIED="1580206405182" TEXT="みつきさんの時は実装されてない"/> -<node CREATED="1580469746286" ID="ID_1576815683" MODIFIED="1580469929318" TEXT="vm.c のコード"> -<icon BUILTIN="idea"/> -<icon BUILTIN="full-1"/> +<node CREATED="1580469746286" ID="ID_1576815683" MODIFIED="1580978971263" TEXT="vm.c のコード"> +<icon BUILTIN="button_ok"/> </node> <node CREATED="1580458062566" ID="ID_379379906" MODIFIED="1580458068975" TEXT="インターフェースの定義"/> <node CREATED="1580458070270" ID="ID_1048176895" MODIFIED="1580458083599" TEXT="インターフェースの実装"> @@ -105,9 +107,13 @@ <icon BUILTIN="full-1"/> </node> </node> -<node CREATED="1580807041389" ID="ID_1062918094" MODIFIED="1580807044523" TEXT="goto panic "/> +<node CREATED="1580807041389" ID="ID_1062918094" MODIFIED="1580979062852" TEXT="goto panic "> +<icon BUILTIN="idea"/> +<icon BUILTIN="full-1"/> </node> -<node CREATED="1578979830870" ID="ID_251771531" MODIFIED="1580461826293" POSITION="right" TEXT="Paging の評価"> +<node CREATED="1580979068578" ID="ID_1698688073" MODIFIED="1580979075066" TEXT="exec.cbc"/> +</node> +<node CREATED="1578979830870" ID="ID_251771531" MODIFIED="1580979001896" POSITION="right" TEXT="Paging の評価"> <icon BUILTIN="idea"/> <icon BUILTIN="full-2"/> </node>