Mercurial > hg > Papers > 2021 > anatofuz-master
changeset 65:e88c0e26d331
...
| author | anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Feb 2021 15:44:54 +0900 |
| parents | f431abfba3b2 |
| children | ae6f626e8816 |
| files | paper/chapter/01-introduction.tex paper/chapter/02-cbc.tex paper/chapter/03-gears.tex paper/master_paper.pdf |
| diffstat | 4 files changed, 46 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/chapter/01-introduction.tex Wed Feb 03 14:45:20 2021 +0900 +++ b/paper/chapter/01-introduction.tex Wed Feb 03 15:44:54 2021 +0900 @@ -14,7 +14,7 @@ 非決定的な処理を持つOSの信頼性を保証するには、 テストコード以外の手法を用いる必要がある。 -テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。 +テストコード以外の方法として、 形式手法と呼ばれるアプローチがある。 形式手法の具体的な検証方法の中で、 証明を用いる方法\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402}とモデル検査を用いる方法がある。 証明を用いる方法ではAgda\cite{agda}やCoq\cite{coq}などの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。 Curry-Howard同型対応則により、型と論理式の命題が対応する。 @@ -22,10 +22,8 @@ 証明には特定の型を入力として受け取り、証明したい型を生成する関数を作成する。 整合性の確認は、記述した関数を元に定理証明支援系が検証する。 証明を使う手法の場合、 実際の証明を行うのは定理証明支援系であるため、 定理証明支援系が理解できるプログラムで実装する必要がある。 -AgdaやCoqの場合はAgda、 Cow自身のプログラムで記述する必要がある。 しかしAgdaで証明ができてもAgdaのコードを直接OSのソースコードとしてコンパイルすることはできない。 -Agda側でCのソースコードを吐き出せれば可能ではあるが、 現状は検証したコードと実際に動作するコードは分離されている。 -検証されたアルゴリズムをもとにCで実装することは可能であるが、 この場合移植時にバグが入る可能性がある。 +検証されたアルゴリズムをもとにCで実装することは可能であるが、 移植時にバグが入る可能性がある。 検証ができているソースコードそのものを使ってOSを動作させたい。 @@ -70,8 +68,10 @@ ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。 またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。 この場合は検証を実行するメタ計算と、 検証をしないメタ計算を手軽に切り替える必要がある。 +さらに検証用とそうでない用で、動作させたいアルゴリズムの実装そのもののコードを変更したくない。 +これも検証をメタレベルで行い、実装をノーマルレベルで行い、各レベルを切り離すことで実現可能である。 メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。 -この為にはノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。 +ノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。 プログラムのノーマルレベルの計算とメタレベルの計算を一貫して行う言語として、 Continuation Based C(CbC)を用いる。 CbCは基本\texttt{goto文}で\texttt{CodeGaar}というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と呼ばれる隠れた状態を持たない。 @@ -82,3 +82,18 @@ CbCは\texttt{GCC}\cite{gcc}\cite{weko_82695_1}あるいは\texttt{LLVM}\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。 Cのコンパイルシステムを使える為に、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。 + +CbCを用いてノーマルレベルとメタレベルの分離を行い、信頼性と拡張性を両立させることを目的としてGearsOSを開発している。 +GeasOSでは、 CbCの実行単位であるCodeGearとデータの単位であるDataGearを基本単位としている。 +GearsOSのメタ計算にはMetaCodeGearとMetaDataGearを用いる。 +信頼性の保証はMetaCodeGearで行いたい。 +その為にはGearsOSが柔軟にメタ計算を切り替えることが必要となる。 +また、GearsOSで実行されるメタ計算の数は膨大である。 +すべてをプログラミングするのではなく、いくつかのメタ計算は自動で生成されてほしい。 +GearsOSでは拡張性の保証も重要な課題である。 +拡張性を保証するにはすべて純粋なCbCで実装すると、実装がきわめて煩雑である。 +その為にはCbCとセマンティックが等しいより簡潔なGearsOS独自のシンタックスなどが必要である。 +これらを踏まえて実装したGearsOSを動作させる際のビルドフローもより効率的なものにしたい。 + +本研究ではGearsOSの信頼性と拡張性の保証につながる、メタ計算に関するAPIについて考察する。 +GearsOSがメタ計算を自動生成しているトランスコンパイラで従来のGearsOSのシステムよりさらに拡張性の充実と、信頼性の保証を図る。 \ No newline at end of file
--- a/paper/chapter/02-cbc.tex Wed Feb 03 14:45:20 2021 +0900 +++ b/paper/chapter/02-cbc.tex Wed Feb 03 15:44:54 2021 +0900 @@ -31,6 +31,12 @@ 各CodeGearの入力として受けるDataGearをInputDataGearと呼ぶ。 逆に次の継続に渡すDataGearをOutputDataGearと呼ぶ。 +メタレベルではDataGearはポインタを扱っているが、 ノーマルレベルのDataGearはポインタを扱っていないと仮定している。 +例えばリストのDataGearを考えると、 Cの実装の場合はポインタを使った単方向リストが考えられる。 +リストのそれぞれの要素には、メタレベルでは次の要素を指し示すポインタが含まれている。 +ノーマルレベルのDataGearとして見る場合は、 リストそのものや、 リストの中の値そのものとして判断するために、より抽象化された単位として見える。 +これは関数型プログラミングにおける末尾再起呼び出し時の値のやりとりに似た概念である。 + \section{CbCを使った例題} ソースコード\ref{src:cbcexample_test}にCbCを使った例題を、 ソースコード\ref{src:cbcexample_test_c}に通常のCで実装した例題を示す。 この例では構造体\texttt{struct test}をcodegear1に渡し、その次にcodegear2に継続している。 @@ -56,7 +62,7 @@ CbCの例題の場合のアセンブラのソースコード\ref{src:cbcexample_test_asm}はcodegear2へ25行目でjmp命令を使って遷移している。 対してC言語での実装の場合(ソースコード\ref{src:cbcexample_test_asm_void})は21行目でcallqを使っている。 jmp命令はプログラムカウンタを切り替えるのみの命令であり、 callは関数呼び出しの命令であるためにスタックの操作が行われる。 - +CbCでのgoto文はすべてこのjmp命令に変換されるため、 関数呼び出しより軽量に実行することが可能である。 \section{CbCを使ったシステムコールディスパッチの例題} @@ -107,23 +113,25 @@ 現状のプログラミング言語やOSでは、 この環境を常に持ち歩かなければならない。 ノーマルレベルとメタレベルを分離しようとすると、 環境の保存について考慮しなければならず、 結果的にシステムコールなどのAPIを使わなければならない。 システムコールを利用しても、 保存されている環境が常に存在する。 -この暗黙の環境のことを常に意識しなければならず、 既存言語でノーマルレベルとメタレベルの分離を完全に行うのは難しい。 +また関数単位での分離を行っても、 呼び出す関数の数が細かくなってしまい、スタックの容量を容易に消費してしまう。 +既存言語ではメタ計算の分離が困難である。 CbCではgoto文による軽量継続によって、 スタックをgotoの度に捨てていく。 そもそもスタックが存在しないため、 暗黙の環境も存在せずに自由にプログラミングが可能となる。 +またCodeGearをどれだけ呼び出しても、関数呼び出し時に伴うスタックの消費も存在しない。 +メタ計算の単位で細かくCodeGearを切り分けても、実行の問題が生じない。 その為従来のプログラミング言語ではできなかった、ノーマルレベルとメタレベルのコードの分離が容易に行える。 CbCでのメタ計算はCodeGear、 DataGearの単位がそのまま使用できる。 メタ計算を行うCodeGearや、 メタな情報を持つDataGearが存在する。 これらの単位はそれぞれ、 MetaCodeGear、 MetaDataGearと呼ばれる。 - \section{MetaCodeGear} - 遷移する各CodeGearの実行に必要なデータの整合性の確認などはメタ計算である。 -この計算はMetaCodeGearと呼ばれる各CodeGearごと実装されたCodeGearで計算を行う。 +この計算はMetaCodeGearと呼ばれる各CodeGearごと実装されたメタなCodeGearで計算を行う。 特に対象のCodeGearの直前で実行されるMetaCodeGearをStubCodeGearと呼ぶ。 +ユーザーからするとノーマルレベルのCodeGear間の移動に見えるが、実際にはStubCodeGearが挿入される。 MetaCodeGearやMetaDataGearは、プログラマが直接実装せず、 PerlスクリプトによってGearsOSのビルド時に生成される。 ただしPerlスクリプトはすでに書かれていたStubCodeGearは上書きしない。 スクリプトに問題がある場合や、 細かな調整をしたい場合はプログラマが直接実装可能である。 @@ -147,3 +155,8 @@ これはデータ自身がどういう型を持っているかなどの情報である。 ほかに計算を実行するCPU、 GPUの情報や、 計算に必要なすべてのDataGearの管理などの実行環境のメタデータもDataGearの形で表現される。 このメタデータを扱うDataGearをMetaDataGearと呼ぶ。 + + +またCbCはスタックを持たないため、 データを保存したい場合はスタック以外の場所に値を書き込む必要がある。 +このスタック以外の場所はDataGearであり、 メタなデータを扱っているためにMetaDataGearと言える。 +具体的にMetaDataGearがどのように構成されているかは、CbCを扱うプロジェクトによって異なる。 \ No newline at end of file
--- a/paper/chapter/03-gears.tex Wed Feb 03 14:45:20 2021 +0900 +++ b/paper/chapter/03-gears.tex Wed Feb 03 15:44:54 2021 +0900 @@ -2,11 +2,17 @@ GearsOSとはContinuation Based Cを用いて実装しているOSプロジェクトである。\cite{gears} CodeGearとDataGearを基本単位として実行する。 +CodeGearを基本単位としているため、 各CodeGearは割り込みされず実行される必要がある。 +割り込みを完全に制御することは一般的には不可能であるが、 GearsOSのメタ計算部分でこれを保証したい。 +DataGearも基本単位であるため、 各CodeGearがDataGearをどのように扱っているか、書き込みをしたかはGearsOS側で保証するとしている。 + + GearsOSはOSとして実行する側面と、 CbCのシンタックスを拡張した言語フレームワークとしての側面がある。 +GearsOSはノーマルレベルとメタレベルの分離を目指して構築しているOSである。 +すべてをプログラマが純粋なCbCで記述してしまうと、 メタレベルの情報を実装しなければならず、ノーマルレベルとメタレベルの分離をした意味がなくなってしまう。 +GesrsOSではユーザーが書いたノーマルレベルのコードの特定の記述や、シンタックスをもとに、メタレベルの情報を含む等価なCbCへと変換するシステムが含まれている。 現在のGearsOSはUnixシステム上のアプリケーションとして実装されているものと、 xv6の置き換えとして実装されているもの\cite{weko_195888_1}がある。 - - \section{Context} Contextとは従来のOSのプロセスに相当する概念である。 GearsOSでのデータの単位から見ると、 MetaDataGearに相当する。