# HG changeset patch # User tobaru # Date 1580981927 -32400 # Node ID b7ae3aa6548e46821d9e9f206e745f1ac872ae19 # Parent 3952ffd84dfea2de06693ab7ab0277932991ccca English abstract diff -r 3952ffd84dfe -r b7ae3aa6548e paper/abstract.tex --- 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. + diff -r 3952ffd84dfe -r b7ae3aa6548e paper/fig/meta_cg_dg.pdf Binary file paper/fig/meta_cg_dg.pdf has changed diff -r 3952ffd84dfe -r b7ae3aa6548e paper/master_paper.log --- 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). diff -r 3952ffd84dfe -r b7ae3aa6548e paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r 3952ffd84dfe -r b7ae3aa6548e paper/master_paper.synctex.gz Binary file paper/master_paper.synctex.gz has changed diff -r 3952ffd84dfe -r b7ae3aa6548e thsis_paging.mm --- 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 @@ - - + + + + + @@ -32,12 +35,11 @@ - - + + - - - + + @@ -57,11 +59,12 @@ - + + - - - + + + @@ -80,9 +83,8 @@ - - - + + @@ -105,9 +107,13 @@ - + + + - + + +