# HG changeset patch # User ryokka # Date 1580838511 -32400 # Node ID d30593612a38cb08f71affdc52a94554dc9d774c # Parent 196ba119ca8932c0c4c52bdaf5782d6b21735512 modify diff -r 196ba119ca89 -r d30593612a38 paper/agda.tex --- a/paper/agda.tex Mon Feb 03 21:47:43 2020 +0900 +++ b/paper/agda.tex Wed Feb 05 02:48:31 2020 +0900 @@ -1,16 +1,17 @@ \chapter{Agda} \label{c:agda} -Adga \cite{agda} とは定理証明支援器であり、関数型言語である。 -Agda は依存型という型システムを持っており、型を第一級オブジェクトとして扱うことができる。 -また、型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応ため +Agda \cite{agda} とは定理証明支援器であり、関数型言語である。 +Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱うことが可能である。 +また、型システムは Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda では記述したプログラムを証明することができる。 -本章では Agda で証明をするために必要な要素について説明を行う。 -また、定理証明支援器としての Agda について解説する。 +本章では Agda で証明をするために必要な要素を示し。 +また、Agda での証明について説明する。 \section{Agda の文法} + Agdaはインデントが意味を持ち、スペースの有無もチェックされる。 -コメントは \verb/\-\- comment/ や \verb/{\-\- comment \-\-}/ のように記述される。 +コメントは \verb/-- comment/ や \verb/{-- comment --}/ のように記述される。 Agda のプログラムは全てモジュール内部に記述されるため、各ファイルのトップレベルにモ ジュールを定義する必要がある。トップレベルのモジュールはファイル名と同一である。 diff -r 196ba119ca89 -r d30593612a38 paper/cbc.tex --- a/paper/cbc.tex Mon Feb 03 21:47:43 2020 +0900 +++ b/paper/cbc.tex Wed Feb 05 02:48:31 2020 +0900 @@ -1,14 +1,14 @@ \chapter{Continuation based C} \label{c:cbc} -Continuation based C\cite{cbc} (以下 CbC) は CodeGear を処理の単位、 DataGear をデータの単位として記述するプログラミング言語である。 CbC は C 言語とほぼ同じ構文を持つが、よりアセンブラに近いプログラムを記述することになる。 -CbC でのプログラミングは DataGear を CodeGear で変更し、その変更を次の CodeGear に渡して処理を実行する。 -現在 CbC の処理系には llvm/clang による実装 \cite{llvm} とgcc \cite{gcc} による実装が存在する。 +Continuation based C\cite{kaito-lola} (以下 CbC) は CodeGear を処理の単位、 DataGear をデータの単位として記述するプログラミング言語である。 CbC は C 言語とほぼ同じ構文を持つが、よりアセンブラに近い記述になる。 +CbC のプログラミングでは DataGear を CodeGear で変更し、その変更を次の CodeGear に渡して処理を行う。 +現在 CbC の処理系には llvm/clang による実装 \cite{utah-master} と gcc \cite{weko_82695_1} による実装が存在する。 -本章は CbC についての説明を行う。 +本章は CbC の概要についての説明する。 -\section{Code GearとData Gear} -当研究室では検証しやすいプログラムの単位として DataGear と CodeGear という +\section{Code Gear と Data Gear} +CbC では検証しやすいプログラムの単位として DataGear と CodeGear という 単位を用いるプログラミングスタイルを提案している。 DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。 @@ -27,37 +27,32 @@ \begin{figure}[htpb] \begin{center} - \scalebox{0.55}{\includegraphics{fig/csds.pdf}} + \scalebox{0.50}{\includegraphics{fig/cgdg.pdf}} \end{center} \caption{CodeGear と DataGear} \label{fig:csds} \end{figure} -\section{メタ計算} +\section{Meta CodeGear、 Meta DataGear} +プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、資源管理等を記述しなければならない処理が存在する。 +これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。 -%% プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、CPUがGPUの資源管理等を記述しなければならない処理が存在する。 -%% これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。 -メタ計算(自己反映計算)\cite{weko_5056_1} とはプログラムを記述する際に通常の処理 -と分離し、他に記述しなければならない処理である。例えば、プログラム実行時のメモリ管 -理やスレッド管理、資源管理等の計算がこれに当たる。 +メタ計算は OS の機能を通して処理することが多く、信頼性の高い記述が求められる。 +そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している。 -メタ計算は関数型言語では Monad\cite{moggi-monad} を用いて表現される\cite{kkb-sigos}。 -Monad は Haskell では実行時の環境を記述する構文として使われる。 +Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。 -従来の OS では、メタ計算はシステムコールやライブラリーコールの単位で行われる。 -実行時にメタ計算の変更を行う場合には OS 内部のパラメータの変更を使用し、実行されるユーザープログラム自体への変更は限定的である。 -しかし、メタ計算は性能測定あるいはプログラム検証、さらに並列分散計算のチューニングなど細かい処理が必要で実際のシステムコール単位では不十分である。 -例えば、モデル検査ではアセンブラあるいは バイトコード、インタプリタレベルでのメタ計算が必要になる。 -しかし、バイトコードレベルでは粒度が細かすぎて扱いが困難になっている。具体的にはメタ計算の実行時間が大きくなってしまう。 +例えば、 CbC では CodeGear を実行する際、ノーマルレベルの計算からは見えないが必要な DataGear を Context と呼ばれる Meta DataGear を通して取得することになる。これはユーザーが直接データを扱える状態では信頼性が高いとは言えないと考えるからである。 +そのために、 Meta CodeGear を用いて Context から必要な DataGear を取り出し、 CodeGear に接続する stub CodeGear という Meta CodeGear が定義されている。 + +Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。 +例えば stub CodeGear では Context と呼ばれる接続可能な CodeGear、 DataGear のリストや、DataGear のメモリ空間等を持った Meta DataGear を扱っている。 -\section{Context} -CbC では、接続可能な全ての CodeGear、 DataGear のリスト、Temporal DataGear のためのメモリ空間などを -Context として保持している。 -CbC で必要な CodeGear 、 DataGear を参照する際は Context を通してアクセスする必要がある。 - -\section{Meta Gears} -Meta Gear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。 -例えば、 CodeGear を実行する際、必要な DataGear を Context を通して取得する必要があるが、ユーザーが Context から直接データを扱える状態は信頼性が高いとは言えない。 -そのために、 CbC では Meta CodeGear を用いて Context から必要な DataGear を取り出し、 CodeGear に接続する stub CodeGear という Meta CodeGear を定義している。 -% Meta DataGear は? +\begin{figure}[htpb] + \begin{center} + \scalebox{0.55}{\includegraphics{fig/meta_cg_dg.pdf}} + \end{center} + \caption{メタ計算を可視化した CodeGear と DataGear} + \label{fig:meta-cgdg} +\end{figure} diff -r 196ba119ca89 -r d30593612a38 paper/cbc_agda.tex --- a/paper/cbc_agda.tex Mon Feb 03 21:47:43 2020 +0900 +++ b/paper/cbc_agda.tex Wed Feb 05 02:48:31 2020 +0900 @@ -1,52 +1,53 @@ \chapter{Continuation based C と Agda} \label{c:cbc_agda} -現在 Agda は CbC の上位言語として使用されており、 -Agda で記述された CbC のプログラムはメタ計算を含む形で記述される。 -しかし、 - +現在 CbC では検証用の上位言語として Agda を利用しており、 +Agda では CbC のプログラムをメタ計算を含む形で記述することができる。 -本章では当研究室で推奨している単位を用いての検証を行うため、 -Agda 上で DataGear、 CodeGear の表現を示す。 -また、Gear の単位と Hoare Logic を対応させ、 -CbC 上での Hoare Logic について示す。 +先行研究\ref{atton-master} では CbC と Agda を対応させるための型付けが行われているが、 +ここでは、その型付けは使わず、前段階である Agda での記述のみで説明を行う。 - +本章では当研究室で推奨している単位での検証を行うために、 +Agda で DataGear、 CodeGear を表現し、 +これらの単位を用いた検証を行う事ができることを示す。 \section{DataGear、 CodeGear と Agdaの対応} -DataGear は Agda で使うことのできるすべてのデータに対応する。 -また、Agda での記述はメタ計算として扱われるので Context を通してデータを -扱う必要はない。 +Agda での DataGear は Agda で使うことのできるすべてのデータに対応する。 +また、Agda での記述はメタ計算として扱われるので、 +Context を通すことなくそのまま扱う。 CodeGear は DataGear を受け取って処理を行い DataGear を返す。 また、CodeGear 間の移動は継続を用いて行われる。 継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻らず、 -次の CodeGear へ継続を行う。 +次の CodeGear へ継続を行うものであった。 -これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当するため、 +これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当し、 継続渡し(Continuation Passing Style) で書かれた Agda の関数と対応する。 継続は不定の型 (\verb/t/) を返す関数で表される。 -CodeGear は次に実行する関数の型を引数として受け取り不定の型\verb/t/を返す関数として記述され、 +継続先は次に実行する関数の型を引数として受け取り不定の型\verb/t/を返す関数として記述され、 CodeGear 自体も同じ型 \verb/t/ を返す関数となる。 コード \ref{agda-while} は Agda で記述した CodeGear の例である。 \lstinputlisting[caption= whileTest の型, label=agda-while]{src/while-test.agda.replaced} -%% Agda のとこで Level の話を…！ -ここでは \verb/c10/ と名付けた自然数を受け取った後、 -\verb/Env/ を受け取って不定の型\verb/t/を返す関数を受け取り、 -\verb/t/を返す CodeGear を定義している。 + +型では \verb/c10/ と名付けた自然数を受け取った後、 +\verb/Env/ を受け取り不定の型\verb/t/を返す関数を受け取り、 +最終的に \verb/t/を返す CodeGear を定義しており、 + +実装では、自然数 \verb/c10/ と継続先の関数 \verb/next/ を受け取り、\verb/next/ に値を代入した Env を引数として渡している。 +\section{Meta Gears の表現} +通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う CodeGear である。 +検証での Meta DataGear は、 DataGear が持つ同値関係や、大小関係などの関係を表す DataGear がそれに当たると考えている。 +Agda 上では Meta DataGear を持つことで性質を持ったデータ構造を作ることができる。 -\section{Meta CodeGear の表現と Meta DataGear} +% \lstinputlisting[label=src:agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda.replaced} + Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear である。 Agda での Meta CodeGear は通常の CodeGear を引数に取りそれらの関係などの上位概念を返す CodeGear である。 これは(図を入れる)のような Code Gear となる。 % \lstinputlisting[label=src:agda-mcg, caption= Agda における Meta CodeGear 型の定義] {src/MetaCodeGear.agda.replaced} -Meta DataGear については不確かであるが、 DataGear が持つ同値関係や、大小関係などの関係を表す DataGear がそれに当たると考えている。 -Agda 上では Meta DataGear を持つことで性質を持ったデータ構造を作ることができる。 - -% \lstinputlisting[label=src:agda-cs, caption= Agda における CodeGear 型の定義] {src/CodeSegment.agda.replaced} \section{CbC 上での HoareLogic の実現} CbC 上の Hoare Logic は引数として事前条件、次の CodeGear に渡す値に事後条件を含めることで記述する。 diff -r 196ba119ca89 -r d30593612a38 paper/fig/cgdg.pdf Binary file paper/fig/cgdg.pdf has changed diff -r 196ba119ca89 -r d30593612a38 paper/fig/cgdg.xbb --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/fig/cgdg.xbb Wed Feb 05 02:48:31 2020 +0900 @@ -0,0 +1,8 @@ +%%Title: fig/cgdg.pdf +%%Creator: extractbb 20190225 +%%BoundingBox: 0 0 535 427 +%%HiResBoundingBox: 0.000000 0.000000 535.000000 427.000000 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Wed Feb 5 01:55:59 2020 + diff -r 196ba119ca89 -r d30593612a38 paper/fig/meta-cg-dg.pdf Binary file paper/fig/meta-cg-dg.pdf has changed diff -r 196ba119ca89 -r d30593612a38 paper/fig/meta-cg-dg.xbb --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/fig/meta-cg-dg.xbb Wed Feb 05 02:48:31 2020 +0900 @@ -0,0 +1,8 @@ +%%Title: fig/meta-cg-dg.pdf +%%Creator: extractbb 20190225 +%%BoundingBox: 0 0 608 202 +%%HiResBoundingBox: 0.000000 0.000000 608.000000 202.000000 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Wed Feb 5 02:00:05 2020 + diff -r 196ba119ca89 -r d30593612a38 paper/history.bib --- a/paper/history.bib Mon Feb 03 21:47:43 2020 +0900 +++ b/paper/history.bib Wed Feb 05 02:48:31 2020 +0900 @@ -1,8 +1,8 @@ -@techreport{weko_189373_1, - author = "外間,政尊 and 河野,真治", - title = "GearsOSのAgdaによる記述と検証", - year = "2018", - institution = "琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科", - number = "5", - month = "may" -} \ No newline at end of file +@Comment @techreport{weko_189373_1, +@Comment author = "外間,政尊 and 河野,真治", +@Comment title = "GearsOSのAgdaによる記述と検証", +@Comment year = "2018", +@Comment institution = "琉球大学大学院理工学研究科情報工学専攻, 琉球大学工学部情報工学科", +@Comment number = "5", +@Comment month = "may" +@Comment } \ No newline at end of file diff -r 196ba119ca89 -r d30593612a38 paper/history.tex --- a/paper/history.tex Mon Feb 03 21:47:43 2020 +0900 +++ b/paper/history.tex Wed Feb 05 02:48:31 2020 +0900 @@ -6,7 +6,7 @@ \begin{enumerate} \item 外間政尊, 河野真治. GearsOSのAgdaによる記述と検証. 研究報告システムソフトウェアとオペレーティング・システム（OS), May, 2018 \item 外間政尊, 河野真治. GearsOSのHoare Logicをベースにした検証手法. 電子情報通信学会 ソフトウェアサイエンス研究会 (SIGSS) 1月, Jan, 2019 - \item 外間政尊, 河野真治. 継続を基本とする言語CbCでのHoareLogicによる健全性の考察. 電子情報通信学会 ソフトウェアサイエンス研究会 (SIGSS) 3月, Jan, 2020 + \item 外間政尊, 河野真治. 継続を基本とする言語CbCでのHoareLogicによる健全性の考察. 電子情報通信学会 ソフトウェアサイエンス研究会 (SIGSS) 3月, Mar, 2020 %% \item 宮城光希, 河野真治. Code Gear と Data Gear を持つ Gears OS の設計. 第59回プログラミング・シンポジウム, Jan, 2018 \end{enumerate} diff -r 196ba119ca89 -r d30593612a38 paper/introduction.tex --- a/paper/introduction.tex Mon Feb 03 21:47:43 2020 +0900 +++ b/paper/introduction.tex Wed Feb 05 02:48:31 2020 +0900 @@ -7,7 +7,7 @@ 証明支援向けのプログラミング言語としては Agda\cite{agda}、 Coq\cite{coq} などが存在しているが、これらの言語自体は実行速度が期待できるものではない。 -そこで、当研究室では検証と実装が同一の言語で行う Continuation based C\cite{cbc} という言語を開発している。 +そこで、当研究室では検証と実装が同一の言語で行う Continuation based C\cite{kaito-lola} という言語を開発している。 Continuation based C(CbC) では、処理の単位を CodeGear、 データの単位を DataGear としている。 CodeGear は値を入力として受け取り出力を行う処理の単位であり、 CodeGear の出力を 次の GodeGear に接続してプログラミングを行う。 CodeGear の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行うことができる。 このメタ計算部分で assertion などの検証を行うことで、 CodeGear の処理に手を加えることなく検証を行う。 diff -r 196ba119ca89 -r d30593612a38 paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r 196ba119ca89 -r d30593612a38 paper/reference.bib --- a/paper/reference.bib Mon Feb 03 21:47:43 2020 +0900 +++ b/paper/reference.bib Wed Feb 05 02:48:31 2020 +0900 @@ -166,4 +166,45 @@ title = {whileTestPrim.agda - 並列信頼研 mercurial repository}, howpublished = {\url{http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestPrim.agda}}, note = {Accessed: 2018/12/17(Mon)} +} + +@mastersthesis{utah-master, + author = "徳森海斗", + title = "LLVM Clang 上の Continuation based C コンパイラ の改良", + school = "琉球大学 大学院理工学研究科 情報工学専攻", + year = "2016" +} + +@mastersthesis{parusu-master, + author = "伊波立樹", + title = "Gears OS の並列処理", + school = "琉球大学 大学院理工学研究科 情報工学専攻", + year = "2017" +} + +@mastersthesis{mitsuki-master, + author = "宮城光希", + title = "継続を基本とした言語による OS のモジュール化", + school = "琉球大学 大学院理工学研究科 情報工学専攻", + year = "2018" +} + +@inproceedings{weko_82695_1, + author = "大城,信康 and 河野,真治", + title = "Continuation based C の GCC4.6 上の実装について", + booktitle = "第53回プログラミング・シンポジウム予稿集", + year = "2012", + volume = "2012", + number = "", + pages = "69--78", + month = "jan" +} + +@article{kaito-lola, + author = "Kaito, Tokumori and Shinji, Kono", + title = "Implementing Continuation based language in LLVM and Clang", + journal = "LOLA 2015, Kyoto", + month = "July", + year = 2015 + } \ No newline at end of file