comparison final_pre/finalPre.tex @ 12:cc8ff782067c

update
author mir3636
date Wed, 15 Feb 2017 19:23:54 +0900
parents 86f6bb9be40a
children 4c3b39b281eb
comparison
equal deleted inserted replaced
11:299ae52e63a6 12:cc8ff782067c
27 \author{135756F 氏名 {宮城}{光希} 指導教員 : 河野 真治} 27 \author{135756F 氏名 {宮城}{光希} 指導教員 : 河野 真治}
28 \date{} 28 \date{}
29 \twocolumn [ 29 \twocolumn [
30 \maketitle 30 \maketitle
31 \begin{onecolabstract} 31 \begin{onecolabstract}
32 We are developping Gears OS using Continuation based C (CbC).
33 Gears OS provids highly reliable computation using meta computation.
34 CbC gives Code Gear and Data Gear as programing units.
35 A transfar from a Code Gear to another Code Gear is implemented using a CbC's goto statement,
36 which is compiled as a jump instraction in CbC.
37 Meta computations are key components of Gears OS, which provids memory managements, thread managements,
38 managements of Data/Code Gear themselves.
39 CbC's goto statments provids a ways of implementing meta computations.
40 From a view point of meta computation, Data Gear or Code Gear are uniform data units, which are implemented
41 as union Data in CbC.
42 In the meta level, a transfar from a Code Gear is a goto statement to meta Code Gear with next Code Gear number and
43 a Context which coresponds thread structure or an enviroments in a functional programing.
44 A meta Code Gear handles meta computations such as meta computations.
45 From a user level, meta structures are not visible directly and a Code Gear looks like a function using continuations.
46 A stub Code Gear is used as a bridge between meta level and user(nomal) level.
47 In this paper we create scripts which generate meta Code Gear and stub Code Gear from nomal level Code Gear and Data Gear.
48 Using these scripts, we can provide a interface mechanisms which are packages of Code Gears and Data Gears.
49 A simple TaskManager is constracted using the interfaces which is a simple operating systems.
50 We will constracts various compornents of Gears OS and meta computations which provids reliabilty.
51 For an example, generating agda program from nomal level Code Gear provids proof suports of the Code Gear.
52 %CbC で OS を記述する。
53 %CbCはLLVMで実装されている。
54 %codeとcode のあいだをcall ではなくjmpで結ぶことができる(goto)
55 %gotoをつかうことによりOSに必須なmeta計算を実現できる
56 %メタ計算は例えばメモリ管理スレッド管理CPUやGPUの資源管理そしてData/Code Gear の管理などである
57 %metaレベルではcode/data gear は一つの塊として操作される。これをcbcではunion dataとして実装している
58 %code gear 間の接続はつぎのcode gearの番号とthread structure に相当するcontextをmeta code gear にgoto する
59 %meta code gear で os の 機能であるメモリ管理やスレッド管理を行う。
60 %ユーザーレベルではmeta構造を直接見ることはなく、継続を用いた関数型プログラミングに見える
61 %metaレベルから見たdata gearをゆーざーれべるのcode gearに接続するにはstub というmeta code gear を用いる
62 %stubとmetaはユーザーレベルcodegear とdatagearから生成することができる
63 %本論文ではstub とcontext 管理構造を生成するスクリプトを作成した
64 %これによりcode gear とdeta gear をデータを操作するinterface というまとまりにすることができる。
65 %この仕組みの上に並列処理用のtaskmanagerを簡単なosとして構成することができた。
66 %こんごはgears os の様々な構成要素を作成していきたい。
67 %またメタ計算を用いて信頼性をあげる方法についても研究を進めていく。
68 %例えばユーザーレベルプログラムから定理証明支援系であるagdaのコードを生成することにより、プログラムの正しさを証明していくことが考えられる。
32 \end{onecolabstract}] 69 \end{onecolabstract}]
33 \thispagestyle{fancy} 70 \thispagestyle{fancy}
34 71
35 \section{メタ計算の重要性} 72 \section{メタ計算の重要性}
36 プログラムを記述する際、通常の処理の他に、メモリ管理、スレッドの待ち合わせやネットワークの管理、エラーハンドリング等、記述しなければならない処理が存在する。 73 プログラムを記述する際、通常の処理の他に、メモリ管理、スレッドの待ち合わせやネットワークの管理、エラーハンドリング等、記述しなければならない処理が存在する。