Mercurial > hg > Papers > 2019 > mitsuki-master
view slide/slide.md @ 59:09c168f8116a
update
author | mir3636 |
---|---|
date | Wed, 13 Feb 2019 09:47:53 +0900 |
parents | a75b7b214f13 |
children | ecf9d73f18f5 |
line wrap: on
line source
title: 継続を基本とした言語による OS のモジュール化 author: 宮城 光希 profile: 琉球大学理工学研究科 河野研 lang: Japanese code-engine: coderay ## 研究目的 - 現代の OS では拡張性と信頼性を両立させることが要求されている。 - 信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。 - ノーマルレベルの計算とメタレベルの計算を切り離して記述するために Code Gear と Data Gear という単位を用いている - Gears OS は Continuation based C(CbC) によってアプリケーションと OS そのものを記述する。 - 本研究では、CbC を用いた Gears OS のモジュール化と信頼性のある OS を実現するために xv6 の CbC による書き換えを行う。 ## OS の拡張性と信頼性の両立 - さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。 - 時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。 - その信頼性を保証するには、従来のテストとデバッグでは不十分であり、テストしきれない部分が残ってしまう。 ## OS の拡張性と信頼性の両立 - これに対処するためには、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。 - 検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しくなることに検証をやり直す必要がある。 - このため信頼性と拡張性を両立させることが重要である。 ## メタ計算とは - プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理やスレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する。これらの計算をメタ計算と呼ぶ。 - メタ計算はノーマルレベルの計算から切り離して記述したい。 - そのためには処理を細かく分割する必要があるが、関数やクラスなどの単位は容易に分割できない。 - そこで当研究室ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を提案している。 ## Continuation based C (CbC) - Continuation based C (CbC) は Code Gear を処理の単位としたプログラミング言語として開発している。 - Code Gear は 関数呼び出しとは異なり、次の Code Gear へと goto 文によって遷移する。 - この goto 文による遷移を軽量継続と呼ぶ。 - 継続を用いることによって状態遷移ベースでのプログラミングが可能である。 - CbC は C と互換性のある言語なので、C の関数も呼び出すことができる。 ## Gears OS - Gears OS は Code Gear と、データの単位である Data Gear を用いて開発されており、CbC で記述されている。 - Gears OS は Context と呼ばれる全ての Code Gear と Data Gear を持ったデータ構造体を常に持ち歩いて処理を行う。 - 必要な Code Gear、Data Gear は、この Context から取り出して処理を実行する。 ## xv6 の CbC 書き換え - xv6 は 2006 年に MIT のオペレーティングシステムコースで教育用の目的として開発されたオペレーティングシステムである。 - xv6 は UNIX V6 を x86 向けに再実装した OS である。 - OS としての基本的な構造を持つにも関わらず、シンプルで扱いやすい。 - 信頼性を保証するために xv6 を CbC で書き換え、Gears OS の機能を導入したい。 - さらに、継続を用いる CbC で記述することにより、実行可能な OS がそのまま状態遷移モデルに落ちる。 ## 目次 - 今回の研究発表は大きく分けて 2部の構成となっている。 - 第1部では Gears OS のモジュール化の仕組みの導入と解説。 - 第2部では xv6 の CbC による書き換え について発表する。 ## 目次 - Code Gear と Data Gear - Gears OS におけるメタ計算 - Context - Meta Code Gear - Interface ## CbC のコード例 - Code Gear は\_\_code Code Gear 名 (引数) の形で記述される。 - Code Gear は戻り値を持たないので、return 文は存在しない。 - goto Code Gear 名 (引数) で次の Code Gear への遷移を表し、これを継続と呼ぶ。 ```Code_Gear __code cg0(int a, int b){ goto cg1(a+b); } __code cg1(int c){ goto cg2(c); } ``` ## CbC の継続 - Code Gear の継続を表す図である。 - Code Gear 間の遷移は goto によって行われる。 - アセンブラレベルで見ると call ではなく jmp となっている。 <div style="text-align: center;"> <img src="./images/normal_Code_Gear.pdf" alt="normalCodeGear" width="600"> </div> ## Data Gear の表現 - Data Gear は Gears OS におけるデータの単位である。 - メタ計算では任意の Data Gear を一律に扱うため、全ての Data Gear は共用体の中で定義される - Data Gear をメモリに確保する際のサイズ情報はこの型から決定する ``` c /* data Gear define */ union Data { struct Timer { union Data* timer; enum Code start; enum Code end; enum Code next; } Timer; struct TimerImpl { double time; } TimerImpl; .... }; ``` ## Gears でのメタ計算 - Gears OS ではメタ計算を Meta Code/Data Gear で表現する。 - Meta Code Gear は通常の Code Gear の直後で遷移し、メタ計算を実行する。 - Meta Code Gear で OS の機能であるメモリ管理やスレッド管理を行う。 <div style="text-align: center;"> <img src="./images/meta_Code_Gear.pdf" alt="MetaCodeGear" width="600"> </div> ## Gears でのメタ計算 - ノーマルレベルとメタレベルの処理はそれぞれ並行して存在するものではなく、 メタレベルの処理にも Meta Meta Gear となるメタレベルの処理が存在するように、 階層上の構造となっている。 - この2つのレベルはプログラミング言語レベルでの変換として実現される。 - 本研究では Perl スクリプトによってノーマルレベルからメタレベルへの変換が実装されている。 ## Meta Gear - Gears OS では、Meta Code Gear は通常の Code Gear の直前、直後に挿入され、メタ計算を実行する。 - 通常の計算からはメタ計算は見ることができない。 <div style="text-align: center;"> <img src="./images/meta_gear.pdf" alt="MetaGear" width="600"> </div> ## Context - Gears OS では Context と呼ばれる、使用されるすべての Code Gear、Data Gear を持つ Meta Data Gear を持っている。 - Gears OS は必要な Code Gear、Data Gear を参照したい場合、この Context を通す必要がある。 - Context は Meta Data Gear であるため、Meta Code Gear を介してアクセスする。 ## Context - Context は全ての Code Gear のリストを持っており、enum で番号とアドレスを対応付けている。 ```c enum Code { C_popSingleLinkedStack, C_pushSingleLinkedStack, C_stackTest3, C_assert3, ... }; ``` ```c context->code[C_popSingleLinkedStack] = popSingleLinkedStack_stub; context->code[C_pushSingleLinkedStack] = pushSingleLinkedStack_stub; context->code[C_stackTest3] = stackTest3_stub; context->code[C_assert3] = assert3_stub; ``` ## Context - Data Gear も Code Gear と同様に Context が全ての Data Gear のリストを持っている。 - Data Gear のリストも enum で管理されている。 - これは引数格納用の Data Gear の番号である。 ```c enum DataType { D_Code, D_SingleLinkedStack, D_Stack, D_TaskManager, D_Worker, ... }; ``` ## stub Code Gear - ノーマルレベルの Gears OS では継続先に渡す Data Gear は引数の集合に見える。 - しかし、メタレベルで見ると、Data Gear は Context が管理しており、 アクセスするには Context を介さなくてはならない。 ```c __code cg1(struct Stack* stack) { Node* node = new Node(); node->color = Red; goto stackPush(stack, node); } __code stackPush(struct Stack* stack, struct Node* node) { Element* element = new Element(); element->next = stack->top; element->data = (union Data*)node; stack->stack->SingleLinkedStack.top = element; goto cg2(...); } ``` ## stub Code Gear - このノーマルレベルとメタレベルのズレを合わせるための Meta Code Gear である Stub Code Gear が Code Gear の間に挿入される。 - stub Code Gear は Context から継続先の Code Gear が必要とする Data Gear を取り出す作業を行う。 ```c __code stackPush_stub(struct Contet* context) { Stack* stack = &context->data[D_Stack]->Stack; Node* node = &context->data[D_Node]->Node; goto stackPush(context, stack, node); } __code stackPush(struct Stack* stack, struct Node* node) { Element* element = new Element(); element->next = stack->top; element->data = (union Data*)node; stack->stack->SingleLinkedStack.top = element; goto cg2(...); } ``` ## stub Code Gear - メタレベル で見た Code Gear の引き渡し <div style="text-align: center;"> <img src="./images/Context_ref.pdf" alt="Context_ref" width="600"> </div> ## goto meta - Gears OS では Code Gear もリストで管理しており、継続する際には一度 \_\_code meta へと継続する。 - ここでノーマルレベルの Code Gear には変換が行われているが、これはコンパイル時に変換される。 - この変換によりノーマルレベルでは隠れていた Context が見えるようになっている。 - context に引き渡しているコードもここで生成される。 ```c __code cg1(struct Context* context, struct Stack* stack) { Node* node = new Node(); node->color = Red; &context->data[D_Stack]->Stack = (union Data*) stack; &context->data[D_Node]->Node = node; goto meta(C_stackPush); } __code meta(struct Context* context, enum Code next) { goto (context->code[next])(context); } ``` ## Interface - Interface は Gears OS のモジュール化の仕組みである。 - Interface はある Data Gear と、それに対する操作(API)を行う Code Gear とその操作に用いる Data Gear の集合を表現する。 - Java の Interface に対応し、定義することで複数の実装を持つことができる。 ## Interface の定義 - Stack の Interface の例である。 - typedef struct Interface 名で記述する。 - Impl は実際に実装した際のデータ構造の型になる。 ```c typedef struct Stack<Impl> { union Data* stack; union Data* data; __code next(...); __code whenEmpty(...); __code clear(Impl* stack, __code next(...)); __code push(Impl* stack, union Data* data, __code next(...)); __code pop(Impl* stack, __code next(union Data* ...)); __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...)); } ``` ## Interface の定義 - Data Gear は 操作する Data Gear と 操作に必要な全ての Data Gear Gear が記述されている。 - \_\_code で記述されているものが操作の Code Gear である。 ```c typedef struct Stack<Impl> { union Data* stack; union Data* data; __code next(...); __code whenEmpty(...); __code clear(Impl* stack, __code next(...)); __code push(Impl* stack, union Data* data, __code next(...)); __code pop(Impl* stack, __code next(union Data* ...)); __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...)); } ``` ## Interface の実装の記述 - ソースコードは Interface の実装の初期化のコードである。 - 操作の Code Gear には実装した Code Gear の番号が代入されるが、ここを入れ替えることで、複数の実装を持つことができる。 ```c Stack* createSingleLinkedStack(struct Context* context) { struct Stack* stack = new Stack(); struct SingleLinkedStack* singleLinkedStack = new SingleLinkedStack(); stack->stack = (union Data*)singleLinkedStack; singleLinkedStack->top = NULL; stack->push = C_pushSingleLinkedStack; stack->pop = C_popSingleLinkedStack; stack->isEmpty = C_isEmptySingleLinkedStack; stack->clear = C_clearSingleLinkedStack; return stack; } ``` ## Interface の操作の呼び出し - Interface の操作の呼び出しは、ノーマルレベルでは `goto interface->method` の形で記述される。 - interface は Interface を表す Data Gear 、method は実装した Code Gear に対応する。 ```c __code stackTest1(struct Stack* stack) { Node* node = new Node(); node->color = Red; goto stack->push(node, stackTest2) } ``` ## Interface の操作の呼び出し - interface の操作の呼び出しは、メタレベルでは以下のように変換される。 - stack->push には enum の番号が入っているため、\_\_code meta で 対応する番号の Code Gear へと継続する。 ```c __code stackTest1(struct Context *context, struct Stack* stack) { Node* node = new Node(); node->color = Red; Gearef(context, Stack)->stack = (union Data*)stack; Gearef(context, Stack)->data = node; Gearef(context, Stack)->next = C_stackTest2; goto meta(context, stack->push) } ``` ## Interface の操作の呼び出し - ここで Gearef という記述があるが、これは Context を参照するためのマクロである。 `Gearef(context, t) (&(context)->data[D_##t]->t)` - 格納先は Interface の型が持つ Data Gear へ格納される。 ```c __code stackTest1(struct Context *context, struct Stack* stack) { Node* node = new Node(); node->color = Red; Gearef(context, Stack)->stack = (union Data*)stack; Gearef(context, Stack)->data = node; Gearef(context, Stack)->next = C_stackTest2; goto meta(context, stack->push) } ``` ## Interface における stub Code Gear - Interface の情報から stub Code Gear は自動生成される。 - 引数に必要な Data Gear は Interface の型が持つ Data Gear から取り出す。 - GearImpl は interface の操作が対象にする Data Gear を取り出すマクロである。 `GearImpl(context, intf, name) (Gearef(context, intf)->name->intf.name)` ```c __code pushSingleLinkedStack(struct Context *context,struct SingleLinkedStack* stack,union Data* data, enum Code next) { ... } __code pushSingleLinkedStack_stub(struct Context* context) { SingleLinkedStack* stack = (SingleLinkedStack*)GearImpl(context, Stack, stack); Data* data = Gearef(context, Stack)->data; enum Code next = Gearef(context, Stack)->next; goto pushSingleLinkedStack(context, stack, data, next); } ``` ## 目次 - xv6 の書き換えの方針について - システムコールの書き換えについての考察 - 書き換えたシステムコールを追う ## xv6 の CbC 書き換え - xv6 は UNIX V6 を x86 向けに再実装した OS である。 - プロセスや仮想メモリ、カーネルとユーザーの分離、割り込み、ファイルシステムなどの基本的な Unix の構造を持つ - CbC は Code Gear 間の遷移が goto による継続で行われるため、状態遷移ベースでのプログラミングに適している。 - CbC で xv6 を書き換えることにより、状態遷移モデルによるモデル検査が可能となることを期待する。 ## xv6 の書き換えの方針 - xv6 を CbC で書き換え、Gears OS の機能と置き換えることで Gears OS に OS の基本構造を持たせたい。 - このためには xv6 をモジュール化することで、xv6 の機能を明らかにする必要がある。 - xv6 の Interface を定義し、Gears OS の機能をこれに合わせることによって実現したい。 ## システムコールの書き換え - CbC は C と互換性のある言語であるため、元のソースコードから大きく崩すことなく必要な機能のみを CbC へと書き換えることが可能である。 - ここでは実際にシステムコールを CbC で書き換えることによって、状態遷移ベースで書き換えるには何が必要か示すことにした。 - 今回は read システムコールの CbC 書き換えを行なった。 ## syscall関数 - syscall 関数 はシステムコールを呼び出す関数である。 ```c void syscall(void) { int num; int ret; num = proc->tf->r0; if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) { proc->cbc_arg.cbc_console_arg.num = num; goto (cbccodes[num])(cbc_ret); } if((num > 0) && (num <= NELEM(syscalls)) && syscalls[num]) { ret = syscalls[num](); if (num != SYS_exec) { proc->tf->r0 = ret; } } else { cprintf("%d %s: unknown sys call %d\n", proc->pid, proc->name, num); proc->tf->r0 = -1; } } ``` ## sys\_read 関数 - 読み込むファイルの情報とアドレスを取り出し、fileread に渡している ```c int sys_read(void) { struct file *f; int n; char *p; if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) { return -1; } return fileread(f, p, n); } ``` ## cbc\_read ```c __code cbc_read(__code (*next)(int ret)){ struct file *f; int n; char *p; if(argfd(0, 0, &f) < 0 || argint(2, &n) < 0 || argptr(1, &p, n) < 0) { goto next(-1); } goto cbc_fileread(f, p, n, next); } ``` ## fileread - file の状態を確認し、対応した関数へ移行する。 ```c int fileread (struct file *f, char *addr, int n) { int r; if (f->readable == 0) { return -1; } if (f->type == FD_PIPE) { return piperead(f->pipe, addr, n); } if (f->type == FD_INODE) { ilock(f->ip); if ((r = readi(f->ip, addr, f->off, n)) > 0) { f->off += r; } iunlock(f->ip); return r; } panic("fileread"); } ``` ## cbc\_fileread ```c __code cbc_fileread1 (int r) { struct file *f = proc->cbc_arg.cbc_console_arg.f; __code (*next)(int ret) = cbc_ret; if (r > 0) f->off += r; iunlock(f->ip); goto next(r); } __code cbc_fileread (struct file *f, char *addr, int n, __code (*next)(int ret)) { if (f->readable == 0) { goto next(-1); } if (f->type == FD_PIPE) { //goto cbc_piperead(f->pipe, addr, n, next); goto next(-1); } if (f->type == FD_INODE) { ilock(f->ip); proc->cbc_arg.cbc_console_arg.f = f; goto cbc_readi(f->ip, addr, f->off, n, cbc_fileread1); } goto cbc_panic("fileread"); } ``` ## readi - readi はファイルシステム上か特殊なデバイスを制御するかどうかで分岐する - ここでは consoleread へ向かう処理を確認する。 ```c int readi (struct inode *ip, char *dst, uint off, uint n) { uint tot, m; struct buf *bp; if (ip->type == T_DEV) { if (ip->major < 0 || ip->major >= NDEV || !devsw[ip->major].read) { return -1; } return devsw[ip->major].read(ip, dst, n); } ... ``` ## cbc\_readi ```c __code cbc_readi (struct inode *ip, char *dst, uint off, uint n, __code (*next)(int ret)) { uint tot, m; struct buf *bp; if (ip->type == T_DEV) { if (ip->major < 0 || ip->major >= NDEV || !cbc_devsw[ip->major].read) { goto next(-1); } goto cbc_devsw[ip->major].read(ip, dst, n, next); } ... ``` ## consoleread - console への入力を読み込み、待っている間スリープする ```c int consoleread (struct inode *ip, char *dst, int n) { uint target; int c; iunlock(ip); target = n; acquire(&input.lock); while (n > 0) { while (input.r == input.w) { if (proc->killed) { release(&input.lock); ilock(ip); return -1; } sleep(&input.r, &input.lock); } c = input.buf[input.r++ % INPUT_BUF]; if (c == C('D')) { // EOF if (n < target) { input.r--; } break; } *dst++ = c; --n; if (c == '\n') { break; } } release(&input.lock); ilock(ip); return target - n; } ``` ## cbc\_consoleread ```c __code cbc_consoleread (struct inode *ip, char *dst, int n, __code(*next)(int ret)) { uint target; iunlock(ip); target = n; acquire(&input.lock); if (n > 0) { proc->cbc_arg.cbc_console_arg.n = n; proc->cbc_arg.cbc_console_arg.target = target; proc->cbc_arg.cbc_console_arg.dst = dst; proc->cbc_arg.cbc_console_arg.ip = ip; proc->cbc_arg.cbc_console_arg.next = next; goto cbc_consoleread2(); } goto cbc_consoleread1(); } ``` ## cbc\_consoleread ```c __code cbc_consoleread2 () { struct inode *ip = proc->cbc_arg.cbc_console_arg.ip; __code(*next)(int ret) = proc->cbc_arg.cbc_console_arg.next; if (input.r == input.w) { if (proc->killed) { release(&input.lock); ilock(ip); goto next(-1); } goto cbc_sleep(&input.r, &input.lock, cbc_consoleread2); } goto cbc_consoleread1(); } __code cbc_consoleread1 () { int cont = 1; int n = proc->cbc_arg.cbc_console_arg.n; int target = proc->cbc_arg.cbc_console_arg.target; char* dst = proc->cbc_arg.cbc_console_arg.dst; struct inode *ip = proc->cbc_arg.cbc_console_arg.ip; __code(*next)(int ret) = proc->cbc_arg.cbc_console_arg.next; int c = input.buf[input.r++ % INPUT_BUF]; if (c == C('D')) { // EOF if (n < target) { input.r--; } cont = 0; } *dst++ = c; --n; if (c == '\n') { cont = 0; } if (cont == 1) { if (n > 0) { proc->cbc_arg.cbc_console_arg.n = n; proc->cbc_arg.cbc_console_arg.target = target; proc->cbc_arg.cbc_console_arg.dst = dst; proc->cbc_arg.cbc_console_arg.ip = ip; proc->cbc_arg.cbc_console_arg.next = next; goto cbc_sleep(&input.r, &input.lock, cbc_consoleread2); } } release(&input.lock); ilock(ip); goto next(target - n); } ``` ## sleep - プロセスをスリープ状態にしてスケジューラーへ引き渡す。 ```c void sleep(void *chan, struct spinlock *lk) { if(proc == 0) { panic("sleep"); } if(lk == 0) { panic("sleep without lk"); } if(lk != &ptable.lock){ //DOC: sleeplock0 acquire(&ptable.lock); //DOC: sleeplock1 release(lk); } proc->chan = chan; proc->state = SLEEPING; sched(); proc->chan = 0; if(lk != &ptable.lock){ //DOC: sleeplock2 release(&ptable.lock); acquire(lk); } } ``` ## cbc\_sleep ```c __code cbc_sleep1() { struct spinlock *lk = proc->lk; proc->chan = 0; if(lk != &ptable.lock){ //DOC: sleeplock2 release(&ptable.lock); acquire(lk); } goto proc->cbc_next(); } __code cbc_sleep(void *chan, struct spinlock *lk, __code(*next1)()) { if(proc == 0) { panic("sleep"); } if(lk == 0) { panic("sleep without lk"); } if(lk != &ptable.lock){ //DOC: sleeplock0 acquire(&ptable.lock); //DOC: sleeplock1 release(lk); } proc->chan = chan; proc->state = SLEEPING; proc->lk = lk; proc->cbc_next = next1; goto cbc_sched(cbc_sleep1); } ``` ## sched - レジスタの値を切り替えて、スケジューラーへと戻る - 再開時は swtch の下から再開する。 ```c void sched(void) { int intena; if(!holding(&ptable.lock)) { panic("sched ptable.lock"); } if(cpu->ncli != 1) { panic("sched locks"); } if(proc->state == RUNNING) { panic("sched running"); } if(int_enabled ()) { panic("sched interruptible"); } intena = cpu->intena; swtch(&proc->context, cpu->scheduler); cpu->intena = intena; } ``` ## cbc\_sched ```c __code cbc_sched(__code(*next)()) { int intena; if(!holding(&ptable.lock)) { panic("sched ptable.lock"); } if(cpu->ncli != 1) { panic("sched locks"); } if(proc->state == RUNNING) { panic("sched running"); } if(int_enabled ()) { panic("sched interruptible"); } intena = cpu->intena; swtch(&proc->context, cpu->scheduler); cpu->intena = intena; goto next(); } ``` ## read システムコールの遷移図 - CbC へ書き換えることで状態遷移ベースのプログラムに書き換えることができた。 - 現在はシステムコールのみだが、カーネル全体を書き換えることで、OS の状態遷移モデルができる。 <div style="text-align: center;"> <img src="./images/state.pdf" alt="state" width="600"> </div>