# HG changeset patch # User mir3636 # Date 1487154234 -32400 # Node ID cc8ff782067c43534fdae2bdee6a59494ce8fd84 # Parent 299ae52e63a6b9e24a92e6589079e6f0c82b4c2f update diff -r 299ae52e63a6 -r cc8ff782067c final_pre/finalPre.tex --- a/final_pre/finalPre.tex Wed Feb 15 18:26:16 2017 +0900 +++ b/final_pre/finalPre.tex Wed Feb 15 19:23:54 2017 +0900 @@ -29,6 +29,43 @@ \twocolumn [ \maketitle \begin{onecolabstract} +We are developping Gears OS using Continuation based C (CbC). +Gears OS provids highly reliable computation using meta computation. +CbC gives Code Gear and Data Gear as programing units. +A transfar from a Code Gear to another Code Gear is implemented using a CbC's goto statement, +which is compiled as a jump instraction in CbC. +Meta computations are key components of Gears OS, which provids memory managements, thread managements, +managements of Data/Code Gear themselves. +CbC's goto statments provids a ways of implementing meta computations. +From a view point of meta computation, Data Gear or Code Gear are uniform data units, which are implemented +as union Data in CbC. +In the meta level, a transfar from a Code Gear is a goto statement to meta Code Gear with next Code Gear number and +a Context which coresponds thread structure or an enviroments in a functional programing. +A meta Code Gear handles meta computations such as meta computations. +From a user level, meta structures are not visible directly and a Code Gear looks like a function using continuations. +A stub Code Gear is used as a bridge between meta level and user(nomal) level. +In this paper we create scripts which generate meta Code Gear and stub Code Gear from nomal level Code Gear and Data Gear. +Using these scripts, we can provide a interface mechanisms which are packages of Code Gears and Data Gears. +A simple TaskManager is constracted using the interfaces which is a simple operating systems. +We will constracts various compornents of Gears OS and meta computations which provids reliabilty. +For an example, generating agda program from nomal level Code Gear provids proof suports of the Code Gear. +%CbC で OS を記述する。 +%CbCはLLVMで実装されている。 +%codeとcode のあいだをcall ではなくjmpで結ぶことができる(goto) +%gotoをつかうことによりOSに必須なmeta計算を実現できる +%メタ計算は例えばメモリ管理スレッド管理CPUやGPUの資源管理そしてData/Code Gear の管理などである +%metaレベルではcode/data gear は一つの塊として操作される。これをcbcではunion dataとして実装している +%code gear 間の接続はつぎのcode gearの番号とthread structure に相当するcontextをmeta code gear にgoto する +%meta code gear で os の 機能であるメモリ管理やスレッド管理を行う。 +%ユーザーレベルではmeta構造を直接見ることはなく、継続を用いた関数型プログラミングに見える +%metaレベルから見たdata gearをゆーざーれべるのcode gearに接続するにはstub というmeta code gear を用いる +%stubとmetaはユーザーレベルcodegear とdatagearから生成することができる +%本論文ではstub とcontext 管理構造を生成するスクリプトを作成した +%これによりcode gear とdeta gear をデータを操作するinterface というまとまりにすることができる。 +%この仕組みの上に並列処理用のtaskmanagerを簡単なosとして構成することができた。 +%こんごはgears os の様々な構成要素を作成していきたい。 +%またメタ計算を用いて信頼性をあげる方法についても研究を進めていく。 +%例えばユーザーレベルプログラムから定理証明支援系であるagdaのコードを生成することにより、プログラムの正しさを証明していくことが考えられる。 \end{onecolabstract}] \thispagestyle{fancy}