Mercurial > hg > Papers > 2018 > nozomi-master

changeset 100:ebe838b83ada

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Self review
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sun, 12 Feb 2017 11:52:20 +0900
parents a891d7551bbf
children 3ef3933dbd77
files paper/akasha.tex paper/atton-master.pdf paper/cbc-type.tex paper/cbc.tex paper/introduction.tex paper/sources.tex paper/src/AgdaParameterizedModule.agda paper/src/MetaMetaCodeSegment.agda paper/src/MetaMetaDataSegment.agda paper/src/akashaContext.h paper/src/stub.cbc paper/src/type-mds.h paper/summary.tex
diffstat 13 files changed, 58 insertions(+), 37 deletions(-) [+]
line wrap: on
line diff
--- a/paper/akasha.tex	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/akasha.tex	Sun Feb 12 11:52:20 2017 +0900
@@ -7,7 +7,7 @@
 \section{モデル検査}
 モデル検査とは、ソフトウェアの全ての状態において仕様が満たされるかを確認するものである。
 このモデル検査を行なうソフトウェアをモデル検査器と呼ぶ。
-モデルは検査器は、仕様の定義と確認ができる。
+モデルは検査器は、仕様の定義とその検証ができる。
 加えて、仕様を満たさない場合にはソフトウェアがどのような状態であったか反例を返す。
 
 モデル検査器には Spin\cite{spin} やCBMC\cite{cbmc} などが存在する。
@@ -82,8 +82,8 @@
 CAS(Check and Set) とは、アトミックに値を置き換える操作であり、使う際は更新前の値と更新後の値を渡す。
 CAS で渡された更新前の値が、保存している値と同じであれば競合していないために値の更新に成功し、異なる場合は他に書き込みがあったことを示すために値の更新が失敗する操作のことである。
 
-非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとする。
-この際に変更が行なわれていない部分は変更前の木と共有する(図\ref{fig:non-destructive-rbtree})。
+非破壊赤黒木の実装の基本的な戦略は、変更したいノードへのルートノードからの経路を全て複製し、変更後に新たなルートノードとすることである。
+この際に変更されていない部分は変更前の木と共有する(図\ref{fig:non-destructive-rbtree})。
 これは一度構築された木構造は破壊されないという非破壊の性質を用いたメモリ使用量の最適化である。
 
 \begin{figure}[htbp]
@@ -145,7 +145,7 @@
 操作を挿入に限定し、どのような順番で要素を挿入しても木がバランスすることを検証する。
 検証には当研究室で開発しているメタ計算ライブラリ akasha を用いる。
 
-akasha では仕様は常に成り立つべき CbC の条件式として定義される。
+akasha では仕様は常に成り立つべき CbC の条件式として定義する。
 具体的には Meta CodeSegment に定義した assert が仕様に相当する。
 仕様の例として「木をルートから辿った際に最も長い経路は最も短い経路の高々2倍に収まる」という式を定義する(リスト\ref{src:assert})。
 
Binary file paper/atton-master.pdf has changed
--- a/paper/cbc-type.tex	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/cbc-type.tex	Sun Feb 12 11:52:20 2017 +0900
@@ -143,6 +143,27 @@
 
 \lstinputlisting[label=src:agda-mcs, caption=Agda における Meta CodeSegment の定義] {src/MetaCodeSegment.agda.replaced}
 
+メタレベルの定義を部分型で行なって分かったことには以下のようなものがある。
+
+\begin{itemize}
+    \item メタ計算は階層構造化できる
+
+        メタ計算は階層構造を取ることができるため、組み合わせることも可能である。
+
+    \item 継続先が不定の場合は型を一様に扱う必要がある
+
+        メタ計算がノーマルレベルの具体的な型を知ることができるのはコンパイル時のみである。
+        よってメタ計算を定義する時は部分型制約しか記述できない。
+        逆に言えばノーマルレベル計算のみであれば部分型は解決され、レコード型で型付けができる。
+
+    \item \verb/stub/ は部分型付けにおいても必要である
+
+        GearsOS では Meta DataSegment から DataSegment を取り出すための処理として \verb/stub/ が存在していた。
+        これは Meta DataSegment で一様に扱っていた DataSegment に型を戻す処理として、型システムにおいても必要なものである。'
+        また、型システム経由で \verb/stub/ を生成することも可能であると考えられる。
+
+\end{itemize}
+
 % }}}
 
 % {{{ メタレベル計算の実行
@@ -198,7 +219,7 @@
 \section{Agda を用いた Continuation based C の証明}
 \label{section:cbc-proof}
 Agda において CbC の CodeSegment と DataSegment を定義することができた。
-実際の CbC のコードを Agda に変換し、それらの性質を証明していく。
+実際の CbC のコードを Agda で記述し、それらの性質を証明していく。
 
 ここではGearsOS が持つ DataSegment \verb/SingleLinkedStack/ を証明していく。
 この\verb/SingleLinkedStack/はポインタを利用した片方向リストを用いて実装されている。
@@ -448,7 +469,8 @@
 n-push-pop は証明の途中で補題 pop-n-push と push-pop を利用した定理である。
 このように、CbC で記述されたプログラムを Agda 上に記述することで、データ構造の性質を定理として証明することができた。
 これらの証明機構を CbC のコンパイラやランタイム、モデルチェッカなどに組み込むことにより CbC は CbC で記述されたコードを証明することができるようになる。
-なお、本論文で取り扱っている Agda のソースコードは視認性の向上のために暗黙的な引数を省略して記述している。
-動作する完全なコードは付録に付す。
+なお、本論文で取り扱っている Agda のソースコードは可読性の向上のために暗黙的な引数を省略している。
+完全なコードは付録に付す。
 
 % }}}
+
--- a/paper/cbc.tex	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/cbc.tex	Sun Feb 12 11:52:20 2017 +0900
@@ -1,7 +1,7 @@
 \chapter{Continuation based C}
 \label{chapter:cbc}
 
-Continuation based C (CbC)は当研究室で開発しているプログラミング言語であり、OSや組み込みソフトウェアの開発を主な対象としている。
+Continuation based C (CbC)は当研究室で開発しているプログラミング言語であり、OSや組み込みソフトウェアを主な対象としている。
 CbC は C言語の下位の言語であり、構文はほぼC言語と同じものを持つが、よりアセンブラに近い形でプログラムを記述する。
 CbC は CodeSegment と呼ばれる単位で処理を定義し、それらを組み合わせることにでプログラム全体を構成する。
 データの単位は DataSegment と呼ばれる単位で定義し、それら CodeSegment によって変更していくことでプログラムの実行となる。
@@ -55,7 +55,7 @@
 Scheme などの call/cc といった継続はトップレベルから現在までの位置を環境として保持する。
 通常環境とは関数の呼び出しスタックの状態である。
 CbC の軽量継続は呼び出し元の情報を持たないため、スタックを破棄しながら処理を続けていく。
-よって、リスト\ref{src:goto} のプログラムでは cs0  から cs1 へと継続した後にcs0 へ戻ることはできない。
+よって、リスト\ref{src:goto} のプログラムでは cs0  から cs1 へと継続した後には cs0 へ戻らずに処理を続ける。
 
 もう少し複雑な CbC のソースコードをリスト\ref{src:factrial}に、実行される流れを図\ref{fig:factrial}に示す。
 このソースコードは整数の階乗を求めるプログラムである。
@@ -82,7 +82,8 @@
 プログラムを動作させるためにメタ計算部分は必須であり、しばしば本来の処理よりも複雑度が高い。
 
 CodeSegment を用いたプログラミングスタイルでは計算とメタ計算を分離して記述する。
-分離した計算は階層構造を持ち、本来行ないたい処理をノーマルレベルとし、メタ計算はメタレベルとしてノーマルレベルよりも上の存在に位置する。
+なお、分離した計算は階層構造を持つ。
+本来行ないたい処理はノーマルレベルであり、メタ計算はメタレベルとして上位に位置する。
 複雑なメタ計算部分をライブラリやOS側が提供することで、ユーザはノーマルレベルの計算の記述に集中することができる。
 また、ノーマルレベルのプログラムに必要なメタ計算を追加することで、並列処理やネットワーク処理などを含むプログラムに拡張できる。
 さらに、ノーマルレベルからはメタレベルは隠蔽されているため、メタ計算の実装を切り替えることも可能である。
@@ -106,9 +107,9 @@
 \section{Continuation based C におけるメタ計算の例: GearsOS}
 CbC を用いてメタ計算を実現した例として、GearsOS\cite{weko_142109_1}が存在する。
 GearsOS は並列に、信頼性高く動作することを目標としたOS であり、 マルチコアCPUやGPU環境での動作を対象としている。
-現在OSの設計と並列処理部分の実装が行なわれている。
+現在はOSの設計と並列処理部分の実装が行なわれている。
 GearsOS におけるメタ計算はMonad\cite{Moggi:1991:NCM:116981.116984}を用いている~\cite{kkb-master}。
-現在実装済みのメタ計算はメモリの管理、並列に書き込むことが可能な Synchronized Queue、データの保存用の非破壊赤黒木がある。
+実装済みのメタ計算はメモリの管理、並列に書き込むことが可能な Synchronized Queue、データの保存用の非破壊赤黒木がある。
 
 GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。
 マルチコアCPU環境では CodeGear と CodeSegment は同一だが、GPU 環境では CodeGear には OpenCL~\cite{opencl}/CUDA~\cite{cuda} における kernel も含まれる。
@@ -163,8 +164,7 @@
         CodeGear の名前と CodeGear の関数ポインタの対応は enum と関数ポインタによって実現されている。
         CodeGear の名前は enum (リスト\ref{src:context} 5-9行) で定義され、コンパイル後には整数へと変換される。
         プログラム全体で利用する CodeGear は code フィールドに格納されており、enum を用いてアクセスする。
-        この対応表を動的に変更することにより、実行時に比較ルーチンなどを変更することが可能になる。
-
+        この対応表を動的に変更することで、実行時に比較ルーチンなどを変更することが可能になる。
 
     \item CodeGear が参照する DataGear へのポインタ
 
@@ -194,9 +194,6 @@
 
 stub は Context が持つ DataGear のポインタ data に対して enum を用いてアクセスしている。
 なお、現在はメタレベルの計算とノーマルレベルの分離はコンパイラ側がサポートしていないため、引数に Meta DataGear である Context が渡されているが、本来はノーマルレベルではアクセスできない。
-% また、stub は全ての CodeGear に対してユーザが1つずつ定義する必要があるため、 CodeGear の定義が煩雑になっている。
-% レベルの分離と stub の自動生成を行なうスクリプトも存在しているが、コンパイラ側のサポートはまだ行なわれていない。
-% 型情報を用いたコンパイル時 stub 生成や、軽量継続時の型チェックを行なうために本研究では CbC の型システムを定義する。
 
 また、GearsOS におけるメタ計算として CodeGear のモデル検査がある。
 通常レベルの CodeGear を変更することなく、その仕様を検証するものである。
--- a/paper/introduction.tex	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/introduction.tex	Sun Feb 12 11:52:20 2017 +0900
@@ -6,8 +6,8 @@
 
 ソフトウェアの検証手法にはモデル検査と定理証明がある。
 
-モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が常に真となることを確認する。
-モデル検査器には Promela と呼ばれる言語でモデルを記述する Spin\cite{spin} や、モデルを状態遷移系で記述する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。
+モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が常に真となることを確認することである。
+モデル検査器には、 Promela と呼ばれる言語でモデルを記述する Spin\cite{spin} や、モデルを状態遷移系で記述する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。
 定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明する。
 定理証明を行なうことができる言語には、依存型で証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。
 
@@ -25,13 +25,14 @@
 本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。
 モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。
 CbC で記述された GearsOS の非破壊赤黒木に対して、メタ計算ライブラリ akasha を用いて仕様を検査する。
-また、定理証明的な検証として、 CbC のプログラムが証明支援系言語 Agda 上に証明可能な形で定義できることを示す。
-Agda 上で CbC のプログラムを記述するために、CbC の型システムを部分型を利用して定義する。
+また、定理証明的な検証として、 CbC のプログラムを証明支援系言語 Agda 上で証明する。
+Agda で CbC の項を表現するために部分型を用いてCbCを型付けし、Agdaでの定義からCbCの形式的な定義を得る。
+そして、Agda 上で Single Linked Stack の性質の証明を行なう。
 
 
 \section{本論文の構成}
 本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。
-CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、GearsOS の解説を行なう。
+CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算の例として GearsOS の解説を行なう。
 第\ref{chapter:akasha}章にて GearsOS 上の非破壊赤黒木の検証をメタ計算ライブラリ akasha にて行なう。
 次に第\ref{chapter:type}章で型システムについて取り上げる。
 型システムの定義と CbC の型システムの定義に必要な単純型、レコード型、部分型について述べる。
--- a/paper/sources.tex	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/sources.tex	Sun Feb 12 11:52:20 2017 +0900
@@ -9,7 +9,7 @@
 
 \section{ノーマルレベル計算の実行}
 \ref{section:normal-level-exec}節で取り上げたソースコードをリスト~\ref{src:normal-level-exec}に示す。
-CbC のコードにより近づけるようにA gda 上の \verb/Data.Nat/ を \verb/Int/ という名前に変更している。
+CbC のコードにより近づけるよう Agda 上の \verb/Data.Nat/ を \verb/Int/ という名前に変更している。
 
 \lstinputlisting[label=src:normal-level-exec, caption=ノーマルレベル計算例の完全なソースコード(atton-master-sample.agda)] {src/atton-master-sample.agda.replaced}
 
--- a/paper/src/AgdaParameterizedModule.agda	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/src/AgdaParameterizedModule.agda	Sun Feb 12 11:52:20 2017 +0900
@@ -1,6 +1,7 @@
 module Sort (A : Set) (_<_ : A -> A -> Bool) where
-  sort : List A -> List A
-  sort = ...
+sort : List A -> List A
+sort = -- 実装は省略 ...
 
+-- Parameterized Module により N.sort や B.sort が可能
 open import Sort Nat  Nat._<_  as N
 open import Sort Bool Bool._<_ as B
--- a/paper/src/MetaMetaCodeSegment.agda	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/src/MetaMetaCodeSegment.agda	Sun Feb 12 11:52:20 2017 +0900
@@ -1,4 +1,3 @@
-...
 -- meta level
 liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
 liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c)))
--- a/paper/src/MetaMetaDataSegment.agda	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/src/MetaMetaDataSegment.agda	Sun Feb 12 11:52:20 2017 +0900
@@ -1,6 +1,7 @@
-...
-open import subtype Context as N
+-- 上で各 DataSegement の定義を行なっているとする
+open import subtype Context as N    -- Meta Datasegment を定義
 
+-- Meta DataSegment を持つ Meta Meta DataSegment を定義できる
 record Meta : Set where
   field
     context : Context
@@ -8,4 +9,4 @@
     next    : N.CodeSegment Context Context
 
 open import subtype Meta as M
-...
+-- 以下よりメタメタレベルのプログラムを記述できる
--- a/paper/src/akashaContext.h	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/src/akashaContext.h	Sun Feb 12 11:52:20 2017 +0900
@@ -1,7 +1,7 @@
 // Data Segment
 union Data {
-    struct Tree { /* ... */ } tree;
-    struct Node { /* ... */ } node;
+    struct Tree { /* ... 赤黒木の定義と同様 */ } tree;
+    struct Node { /* ... 赤黒木の定義と同様 */ } node;
 
     /* for verification */
     struct IterElem {
--- a/paper/src/stub.cbc	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/src/stub.cbc	Sun Feb 12 11:52:20 2017 +0900
@@ -3,7 +3,7 @@
            struct Node* root,
            struct Allocate* allocate)
 {
-    /* ... */
+    /* 実装コードは省略 */
 }
 
 __code put_stub(struct Context* context)
--- a/paper/src/type-mds.h	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/src/type-mds.h	Sun Feb 12 11:52:20 2017 +0900
@@ -2,7 +2,7 @@
     struct Tree { /* ... */ } tree;
     struct Node { /* ... */ } node;
 
-    struct IterElem { /* ..  */ } iterElem;
+    struct IterElem { /* ... */ } iterElem;
     struct Iterator { /* ... */ } iterator;
     struct AkashaInfo { /* ... */} akashaInfo;
     struct AkashaNode { /* ... */} akashaNode;
@@ -10,6 +10,6 @@
 
 
 struct Context { /* meta data segment as subtype */
-    /* ... */
-    struct Data **data;
+    /* ... fields for meta computations ... */
+    struct Data **data; /* data segments */
 };
--- a/paper/summary.tex	Sun Feb 12 11:13:08 2017 +0900
+++ b/paper/summary.tex	Sun Feb 12 11:52:20 2017 +0900
@@ -8,7 +8,7 @@
 
 二つめは定理証明的なアプローチである。
 akasha を用いた検証では挿入回数は有限の数に限定されていた。
-データ構造とそれにまつわる処理を直接証明することにより、任意の回数操作を行なっても性質を保証する。
+プログラムを直接証明することにより、任意の回数の操作においても性質を保証する。
 部分型を利用して CbC の型システムの定義を行ない、依存型を持つ言語 Agda 上で記述することで CbC の形式的な定義とした。
 Agda 上で記述された CbC プログラムの性質を証明することで、 CbC が部分型できちんと型付けできること、依存型をCbCコンパイラに組み込むことでCbC 自身を証明できることが分かった。
 
@@ -30,4 +30,4 @@
 
 また、型システムの拡張としては総称型などを CbC に適用することも挙げられる。
 多相型は \verb/Java/ におけるジェネリクスや \verb/C++/ におけるテンプレートに相当し、ユーザが定義できるデータ構造の表現能力が向上する。
-他にも、CbC における型推論や推論器のコンパイラへの実装などが挙げられる。
+他にも、CbC の型推論や推論器の実装などが挙げられる。