--- a/paper/abstract.tex	Sat Jan 06 19:07:03 2018 +0900
+++ b/paper/abstract.tex	Thu Jan 25 18:15:48 2018 +0900
@@ -1,33 +1,27 @@
 \begin{abstract}
-高い信頼性を持つソフトウェアを提供することは重要である。
-それには、ソフトウェアが期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。
-特に実際に動作するソフトウェアを検証や証明できるとなお良い。
-本論文では 検証や証明に直接使用することができる言語として Continuation based C(CbC) 言語を用いる。
+スマートフォンやタブレット端末の普及率が増加している。
+それに伴いインターネット利用者数も増加しており、ネットワーク上のサービスには
+、信頼性とスケーラビリティーが要求される。
+ここでいう信頼性とは、定められた環境下で安定して仕様に従った動作を行うことを
+指す。
+またスケーラビリティーとは、スケーラビリティとは、分散ソフトウェアに対して単純にノードを追加するだけで性能を線形的に上昇させることができる性質である。
+しかし、これらをもつ分散プログラムをユーザーが一から記述することは容易ではない。
 
-CbC上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法を提案し、メタ計算ライブラリ akasha として実装した。
-akasha では赤黒木の仕様を、限定的な木の大きさの範囲内で検証した。
+これらの問題の解決のために、当研究室ではデータをData Segment、タスクをCode Segmentという単位で記述するプログラミング手法を導入した分散フレームワークAlice の開発を実現した。
+Data Segmentは整数や文字列や構造体などの基本的なデータの集まりである。
+Code Segmentは入力となるData Segmentが全て揃ったら処理を開始し計算結果のData Segmentを出力するタスクである。
 
-木の大きさを制限せず実装が仕様を満たすことを示すには証明が必要である。
-プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。
-本論文では依存型を持つ証明支援系 Agda を用いて証明を行なう。
-部分型を用いてCbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。
-これらの形式的定義を Agda によって記述し、Single Linked Stackの満たす性質を証明した。
+Aliceが実用的な分散アプリケーションを記述でき、仕様の変更を抑えた信頼性の高い拡
+張を可能にするということは、水族館の例題やTreeVNCの例題から確認された。
+しかし、AliceではAPI設計が直感的でなく、型の整合性がとれない問題があった。また、AliceにNAT越えの機能を実装しようとした際、Data Segment Managerが1つしか持てない
+たために拡張が困難であることが分かった。
+
+本研究では、Aliceから得られた知見をもとに、分散フレームワークChristieの設計を行った。
+
+
 
 \end{abstract}
 
 \begin{abstract_eng}
-Proving highly reliable software is important.
-One way is checking if the specification is satisfied or not, the other way is to prove the implementation satisfies the specification directly.
-If we can check or prove actual implementations, it it much better.
-In this paper, we use Continuation base C programming language (CbC) which can be used in both model checking and proof.
-
-We propose model checking method by enumerating bounded computational state in CbC code as a meta computation.
-Akasha meta computation library makes it possible to check red-black tree algorithm within a bounded tree size.
-
-To assure the property for arbitrary size of trees, we need proof method.
-Proofs in a program are known to correspond $\lambda$ calculus, which is a Curry-Howward Isomorphism.
-We use dependently typed Agda proof assistance system.
-Formal definitions of CbC are similarly defined by subtyped CbC terms using Agda.
-We prove properties of Single Linked Stack using proposed formal definitions.
 \end{abstract_eng}
 

Binary file paper/nozomi-master.pdf has changed

--- a/paper/nozomi-master.tex	Sat Jan 06 19:07:03 2018 +0900
+++ b/paper/nozomi-master.tex	Thu Jan 25 18:15:48 2018 +0900
@@ -15,8 +15,8 @@
 
 %\input{dummy.tex} %% font
 
-\jtitle{並列分散フレームワークChristieの設計}
-%\etitle{}
+\jtitle{分散フレームワークChristieの設計}
+\etitle{Design of Distributed framework Christie}
 \year{2018年 3月}
 \eyear{March 2018}
 \author{照屋 のぞみ}
@@ -36,6 +36,7 @@
 
 \newcommand\figref[1]{図 \ref{fig:#1}}
 \newcommand\tabref[1]{表 \ref{tab:#1}}
+\newcommand{\tblcaption}[1]{\def\@captype{table}\caption{#1}}
 
 \lstset{
   frame=single,
@@ -77,7 +78,7 @@
 \makecommission
 
 %要旨
-%\input{abstract.tex}
+\input{abstract.tex}
 
 %目次
 \tableofcontents
@@ -120,25 +121,204 @@
 
 \chapter{分散フレームワークAliceの概要}
 \section{CodeSegmentとDataSegment}
+AliceではCode Segment（以下CS）とData Segment（以下DS）の依存関係を記述することでプログラミングを行う。
+
+CSは実行に必要なDSが全て揃うと実行される。CSを実行するために必要な入力されるDSのことをInputDS、CSが計算を行った後に出力されるDSのことをOutput DSと呼ぶ。
+
+データの依存関係にないCSは並列実行が可能である（図 \ref{fig:CS} ）。
+CSの実行においてDSが他のCSから変更を受けることはない。そのためAliceではデータが他から変更され整合性がとれなくなることはない。
+
+\begin{figure}[htbp]
+    \begin{center}
+        \includegraphics{images/dsandcs2.pdf}
+    \end{center}
+    \caption{CodeSegmentの依存関係 }
+    \label{fig:CS}
+\end{figure}
+
+AliceはJavaで実装されており、DSはJava Objectに相当する。
+CSはRunnableなObject(void run()を持つObject)に相当する。
+プログラマがCSを記述する際は、CodeSegmentクラスを継承する。
+
+DSは数値や文字列などの基本的なデータの集まりを指し、Aliceが内部にもつデータベースによって管理されている。このデータベースをAliceではDS Managerと呼ぶ。
+
+CSは複数のDS Managerを持っている。DSには対になるString型のkeyが存在し、それぞれのManagerにkeyを指定してDSにアクセスする。
+一つのkeyに対して複数のDSをputするとFIFO的に処理される。なのでData Segment Managerは通常のデータベースとは異なる。
+
+
+
 \section{DataSegmentManager}
+DS Manager（以下DSM）にはLocal DSMとRemote DSMが存在する。Local DSMは各ノード固有のデータベースである。
+
+Remote DSMは他ノードのLocal DSMに対応するproxyであり、接続しているノードの数だけ存在する（図 \ref{fig:Remote DSM} ）。
+他ノードのLocal DSMに書き込みたい場合はRemote DSMに対して書き込めば良い。
+
+Remote DSMを立ち上げるには、DataSegmentクラスが提供するconnectメソッドを用いる。
+接続したいノードのipアドレスとport番号、そして任意のManager名を指定することで立ちあげられる。
+その後はManager名を指定してData Segment APIを用いてDSのやり取りを行うため、プログラマはManager名さえ
+意識すればLocalへの操作もRemoteへの操作も同じ様に扱える。
+
+\begin{figure}[h]
+    \begin{center}
+        \includegraphics[width=150mm]{images/remote_datasegment.pdf}
+    \end{center}
+    \caption{Remote DSMは他のノードのLocal DSMのproxy }
+    \label{fig:Remote DSM}
+\end{figure}
+
+
 \section{Data Segment API}
+DSの保存・取得にはAliceが提供するAPIを用いる。
+
+putとupdate、flipはOutput DS APIと呼ばれ、DSをDSMに保存する際に用いる。
+
+peekとtakeはInput DS APIと呼ばれ、DSをDSMから取得する際に使用する。
+
+\begin{itemize}
+\item {\ttfamily void put(String managerKey, String key, Object val)}
+\end{itemize}
+DSをDSMに追加するためのAPIである。第一引数はLocal DSMかRemote DSMかといったManager名を指定する。そし
+て第二引数で指定されたkeyに対応するDSとして第三引数の値を追加する。
+
+\begin{itemize}
+\item {\ttfamily void update(String managerKey, String key,  Object val)}
+\end{itemize}
+updateもDSをDSMに追加するためのAPIである。putとの違いは、queueの先頭のDSを削除してからDSを追加するこ
+とである。そのためAPI実行前後でqueueの中にあるDSの個数は変わらない。
+
+\begin{itemize}
+\item{\ttfamily void flip(String managerKey, String key,  Receiver val)}
+\end{itemize}
+flipはDSの転送用のAPIである。取得したDSに対して何もせずに別のKeyに対し保存を行いたい場合、一旦値を取
+り出すのは無駄である。flipはDSを受け取った形式のまま転送するため無駄なコピーなくDSの保存ができる。
+
+\begin{itemize}
+\item {\ttfamily void take(String managerKey, String key)}
+\end{itemize}
+takeはDSを読み込むためのAPIである。読み込まれたDSは削除される。要求したDSが存在しなければ、CSの待ち合わせ （Blocking）が起こる。putやupdateによりDSに更新があった場合、takeが直ちに実行される。
+
+\begin{itemize}
+\item {\ttfamily void peek(String managerKey, String key)}
+\end{itemize}
+peekもDSを読み込むAPIである。takeとの違いは読み込まれたDSが削除されないことである。
+
+
+
 \section{CodeSegmentの記述方法}
+CSをユーザーが記述する際にはCodeSegmentクラスを継承して記述する(ソースコード \ref{src:StartCodeSegmen
+t} , \ref{src:CodeSegment})。
+
+継承することによりCode Segmentで使用するData Segment APIを利用する事ができる。
+
+Alice には、Start CS (ソースコード \ref{src:StartCodeSegment} )というC の main に相当するような最初に
+実行される CS がある。
+Start CSはどのDSにも依存しない。つまりInput DSを持たない。
+このCSをmainメソッド内でnewし、executeメソッドを呼ぶことで実行を開始させることができる。
+
+%\begin{table}[html]
+%    \lstinputlisting[label=src:StartCodeSegment, caption=StartCodeSegmentの例]{source/StartCodeSegment.java}
+%    \lstinputlisting[label=src:CodeSegment, caption=CodeSegmentの例]{source/TestCodeSegment.java}
+%\end{table}
+
+\newpage
+
+ソースコード \ref{src:StartCodeSegment} は、5行目で次に実行させたいCS（ソースコード \ref{src:CodeSegment} ）を作成している。
+8行目でOutput DS APIを通してLocal DSMに対してDSをputしている。
+Output DS APIはCSの{\tt ods}というフィールドを用いてアクセスする。
+{\tt ods}は{\tt put}と{\tt update}と{\tt flip}を実行することができる。
+TestCodeSegmentはこの"cnt"というkeyに対して依存関係があり、8行目でputが行われるとTestCodeSegmentは実
+行される。
+
+
+CSのInput DSは、CSの作成時に指定する必要がある。指定はCommandType(PEEKかTAKE)、DSM名、そしてkey よっ
+て行われる。
+Input DS API はCSの{\tt ids}というフィールドを用いてアクセスする。
+Output DSは、{\tt ods}が提供するput/update/flipメソッドをそのまま呼べばよかったが、Input DSの場合{\tt ids}にpeek/takeメソッドはなく、create/setKeyメソッド内でCommandTypeを指定して実行する。
+
+ソースコード\ref{src:CodeSegment}は、0から9までインクリメントする例題である。
+2行目では、Input DS APIがもつcreateメソッドでInput DSを格納する受け皿(Receiver)を作っている。
+引数には{\tt PEEK}または{\tt TAKE}を指定する。
+\begin{itemize}
+\item {\ttfamily Receiver create(CommandType type)}
+\end{itemize}
+
+4行目から6行目はコンストラクタである。コンストラクタはオブジェクト指向のプログラミング言語で新たなオ
+ブジェクトを生成する際に呼び出されて内容の初期化を行う関数である。
+
+% TestCodeSegmentのコンストラクタが呼ばれた際には、
+% \begin{enumerate}
+% \item CSが持つフィールド変数 {\tt Receiver input}に{\tt ids.create(CommandType.TAKE)}が行われ、{\tt input}が初期化される。
+% \item 5行目にあるTestCodeSegmentのコンストラクタのTAKEが実行される。
+% \end{enumerate}
+
+5行目は、2行目のcreateで作られたReceiverが提供するsetKeyメソッドを用いてLocal DSMからDSを取得している。
+\begin{itemize}
+\item \verb+void setKey(String managerKey, String key)+
+\end{itemize}
+setKeyメソッドはpeek/takeの実行を行う。どのDSMのどのkeyに対してpeekまたはtakeコマンドを実行させるかを指定できる。コマンドの結果がレスポンスとして届き次第CSは実行される。
+
+実行されるrunメソッドの内容は
+\begin{enumerate}
+\item 10行目で取得されたDSをInteger型に変換してcountに代入する。
+\item 12行目でcountをインクリメントする。
+\item 16行目で次に実行されるCSが作られる。（この時点で次のCSはInput DSの待ち状態に入る）
+\item 17行目でcountをLocal DSMにputする。Input DSが揃い待ち状態が解決されたため、次のCSが実行される。
+\item 13行目が終了条件であり、countの値が10になれば終了する。
+ \end{enumerate}
+となっている。
+
+
 \section{TopologyManager}
+Aliceでは、ノード間の接続管理やトポロジーの構成管理を、Topology ManagerというMeta Computationが提供している。
+プログラマはトポロジーファイルを用意し、Topology Managerに読み込ませるだけでトポロジーを構成すること
+ができる。
+トポロジーファイルはDOT Language\cite{dot}という言語で記述される。
+DOT Languageとは、プレーンテキストを用いてデータ構造としてのグラフを表現するためのデータ記述言語の一
+つである。
+ソースコード\ref{src:topologyfile}は3台のノードでリングトポロジーを組むときのトポロジーファイルの例である。
+
+%\begin{table}[html]
+%    \lstinputlisting[label=src:topologyfile, caption=トポロジーファイルの例]{source/TopologyFile.dot}
+%\end{table}
+DOT Languageファイルはdotコマンドを用いてグラフの画像ファイルを生成することができる。そのため、記述したトポロジーが正しいか可視化することが可能である。
+
+\newpage
+
+Topology Managerはトポロジーファイルを読み込み、参加を表明したクライアント（以下、Topology Node）に接続するべきクライアントのIPアドレスやポート番号、接続名を送る（図\ref{fig:topologymanager}）。
+また、トポロジーファイルでlavelとして指定した名前はRemote DSMの名前としてTopology Nodeに渡される。
+そのため、Topology NodeはTopology ManagerのIPアドレスさえ知っていれば自分の接続すべきノードのデータを受け取り、ノード間での正しい接続を実現できる。
+\begin{figure}[h]
+\begin{center}
+\includegraphics{images/topologymanager.pdf}
+\end{center}
+\caption{Topology Managerが記述に従いトポロジーを構成}
+\label{fig:topologymanager}
+\end{figure}
+
+また、実際の分散アプリケーションでは参加するノードの数が予め決まっているとは限らない。
+そのためTopology Managerは動的トポロジーにも対応している。
+トポロジーの種類を選択してTopology Managerを立ち上げれば、あとは新しいTopology Nodeが参加表明するたびに、Topology ManagerからTopology Nodeに対して接続すべきTopology Nodeの情報がput
+され接続処理が順次行われる。
+そしてTopology Managerが持つトポロジー情報が更新される。
+現在Topology Managerでは動的なトポロジータイプとして二分木に対応している。
+
 
 \chapter{Aliceの問題点}
 \section{直感的でないAPI}
 \section{型がわからない}
 \section{DataSegmentManagerを複数持てない}
 \subsection{TopologyManagerのNAT超え機能}
+\subsection{Jungleのテスト}
 
 \chapter{分散フレームワークChristieの設計}
+\section{Christieの基本設計}
 \section{APIの改善}
+\section{DataGearManagerの複数立ち上げ}
 
 \chapter{Christieの評価}
 \section{Akka}
 \section{Corba}
 \section{Erlang}
-\section{Spark}
 \section{Hazelcast}
 
 \chapter{まとめ}