Mercurial > hg > Papers > 2018 > nozomi-master
changeset 174:f0e9cc7d13f9
minor change
| author | Nozomi Teruya <e125769@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 05 Feb 2018 16:38:28 +0900 |
| parents | 52a43c1336d9 |
| children | 7e7fe5e28ba4 |
| files | paper/introduction.tex paper/master_paper.sty paper/nozomi-master.pdf paper/nozomi-master.tex paper/reference.bib |
| diffstat | 5 files changed, 78 insertions(+), 114 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/introduction.tex Mon Feb 05 14:59:41 2018 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -\chapter{CbC とメタ計算としての検証手法} -ソフトウェアの規模が大きくなるにつれてバグは発生しやすくなる。 -バグとはソフトウェアが期待される動作以外の動作をすることである。 -ここで期待された動作は仕様と呼ばれ、自然言語や論理によって記述される。 -検証とは定められた環境下においてソフトウェアが仕様を満たすことを保証することである。 - -ソフトウェアの検証手法にはモデル検査と定理証明がある。 - -モデル検査とはソフトウェアの全ての状態を数え上げ、その状態について仕様が常に真となることを確認することである。 -モデル検査器には、 Promela と呼ばれる言語でモデルを記述する Spin\cite{spin} や、モデルを状態遷移系で記述する NuSMV\cite{nusmv}、C言語/C++ を記号実行する CBMC\cite{cbmc} などが存在する。 -定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明する。 -定理証明を行なうことができる言語には、依存型で証明を行なう Agda\cite{agda} や Coq\cite{coq} 、 ATS2\cite{ats2} などが存在する。 - -モデル検査器や証明でソフトウェアを検証する際、検証を行なう言語と実装に使われる言語が異なるという問題がある。 -言語が異なれば二重で同じソフトウェアを記述する必要がある上、検証に用いるソースコードは状態遷移系でプログラムを記述するなど実装コードに比べて記述が困難である。 -検証されたコードから実行可能なコードを生成可能な検証系もあるが、生成されたコードは検証のコードとは別の言語であったり、既存の実装に対する検証は行なえないなどの問題がある。 -そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{utah-master} 言語を開発している。 - -Continuation based C (CbC)はC言語と似た構文を持つ言語である。 -CbC では処理の単位は関数ではなく CodeSegment という単位で行なわれる。 -CodeSegment は値を入力として受け取り出力を行なう処理単位であり、CodeSegment を接続していくことによりソフトウェアを構築していく。 -CodeSegment の接続処理はメタ計算として定義されており、実装や環境によって切り替えを行なうことができる。 -検証を行なうメタ計算を定義することにより、CodeSegment の定義を検証用に変更せずソフトウェアの検証を行なう。 - -本論文では CbC のメタ計算として検証手法の提案と CbC の型システムの定義を行なう。 -モデル検査的な検証として、状態の数え上げを行なう有限のモデル検査と仕様の定義を CbC 自身で行なう。 -CbC で記述された GearsOS の非破壊赤黒木に対して、メタ計算ライブラリ akasha~\cite{atton-ipsjpro} を用いて仕様を検査する。 -また、定理証明的な検証として、 CbC のプログラムを証明支援系言語 Agda 上で証明する。 -Agda で CbC の項を表現するために部分型を用いてCbCを型付けし、Agdaでの定義からCbCの形式的な定義を得る。 -そして、Agda 上で Single Linked Stack の性質の証明を行なう。 - - -\section{本論文の構成} -本論文ではまず第\ref{chapter:cbc}章で Continuation based C の解説を行なう。 -CbC を記述するプログラミングスタイルである CodeSegment と DataSegment の解説、メタ計算の例として GearsOS の解説を行なう。 -第\ref{chapter:akasha}章にて GearsOS 上の非破壊赤黒木の検証をメタ計算ライブラリ akasha にて行なう。 -次に第\ref{chapter:type}章で型システムについて取り上げる。 -型システムの定義と CbC の型システムの定義に必要な単純型、レコード型、部分型について述べる。 -第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。 -Agda の構文や使い方、Curry-Howard Isomorphism や Natural Deduction といった証明に関する解説も行なう。 -第\ref{chapter:cbc-type}章では、部分型を用いて CbC のプログラムを Agda で記述し、証明を行なう。 -CodeSegment や DataSegment の Agda 上での定義や、メタ計算はどのように定義されるかを解説する。
--- a/paper/master_paper.sty Mon Feb 05 14:59:41 2018 +0900 +++ b/paper/master_paper.sty Mon Feb 05 16:38:28 2018 +0900 @@ -197,10 +197,10 @@ (主 査) 和田 知久 \vskip 2 em \underline{ 印}\\ - (副 査) 岡崎 威生 + (副 査) 長田 智和 \vskip 2 em \underline{ 印}\\ - (副 査) 名嘉村 盛和 + (副 査) 玉城 史郎 \vskip 2 em \underline{ 印}\\ (副 査) 河野 真治
--- a/paper/nozomi-master.tex Mon Feb 05 14:59:41 2018 +0900 +++ b/paper/nozomi-master.tex Mon Feb 05 16:38:28 2018 +0900 @@ -115,7 +115,7 @@ しかし、これらをもつ分散プログラムをユーザーが一から記述することは容易ではない。 なぜなら、並列で動く分散した資源を意識しながら記述するのは容易ではなく、また、どのように分散したノードの選択を行えば良いのか明確ではないからである。 -分散プログラムには以下の３つの要素がある。 +分散プログラムには以下の３つの要素がある\cite{Framework}。 \begin{itemize} \item {ノード内の計算} \end{itemize} @@ -155,23 +155,17 @@ Data Segmentは対になるkeyが存在し、Data Segment Managerというノードごとに存在する独自のデータベースによって管理されている。 各ノードにはラベル付きのプロキシであるRemote Data Segment Managerを立て、ラベルとkeyを指定してデータをtake/putするプロトコルとなっている。 -%Topologymanagerもここにかく？ - \newpage -%問題といったら参考文献が必要,わかりづらいとハッキリ書かない -記述の面において、Akkaではメッセージが集中した場合にそれを処理するパターンマッチが増えてしまう問題や、複数のインプットを待ち合わせる際に記述が煩雑になる問題があった。 -しかしAliceはインプットを明確に記述でき、複数のインプットを持てる。 +記述の面において、Akkaでは基本的にメッセージをFIFO的に処理するため、複数のインプットを待ち合わせる場合は、待ち合わせの処理をプログラマが各必要があった。 +しかしAliceは複数のインプットを1箇所に記述するるため、そのような煩雑さがない。 プロトコルの設計方針において、AkkaやHazelcastは分散通信の複雜さを抽象度を高めることで隠す方針であるため、ロケーション透過性が高く、プログラマからは処理の流れを把握しにくくなっていた。 -一方でAliceは分散計算のチューニングをメタ計算として行う。これによりメタ計算から分離された処理の流れを明確にすることができる。 - -Alice の分散ノード間の通信はラベルを用いてリモートノードを選択することによって指定する。 -Akkaでは送り先をドメインで指定しているのと同様である。Alice ではラベルはToplogy managerによって自動的に指定される。 +一方でAliceでは明示的に分散性を意識する代わりに、計算を通常計算とそれを支えるメタ計算として分離することで記述の複雑さを回避している。 +これにより処理の流れを明確にし、分散計算のチューニングをしやすくしている。 -% このように、Aliceのプロトコルの特徴は分散処理の見通しの良さといえる。Alice は Java 上に実装されており、Javaのオブジェクト生成や -% 継承により記述されている -%しかし、現状のAliceのAPIシンタックスは直感的でなく、プログラマが処理の順番やデータの型を考慮して書く必要があった。 -%これではバグを引き起こす可能性が高いため、信頼性を上げるにはよりユーザーフレンドリーなシンタックスで再設計すべきだと考えた。 +また、Aliceの分散ノード間の通信はラベルを用いてリモートノードを選択することによって指定する。 +これはAkkaで送り先をドメインで指定しているのと同様である。 +Aliceではラベルの命名をToplogy Managerによって自動的に指定することもできる。 \section{トポロジーの構成} @@ -255,9 +249,9 @@ \section{DataSegmentManager} -DS Manager（以下DSM）にはLocal DSMとRemote DSMが存在する。Local DSMは各ノード固有のデータベースである。 +DS Manager(以下DSM)にはLocal DSMとRemote DSMが存在する。Local DSMは各ノード固有のデータベースである。 -Remote DSMは他ノードのLocal DSMに対応するproxyであり、接続しているノードの数だけ存在する（図 \ref{fig:Remote DSM} ）。 +Remote DSMは他ノードのLocal DSMに対応するproxyであり、接続しているノードの数だけ存在する(図 \ref{fig:Remote DSM} )。 他ノードのLocal DSMに書き込みたい場合はRemote DSMに対して書き込めば良い。 \newpage @@ -311,7 +305,7 @@ \begin{itemize} \item {\ttfamily void take(String managerKey, String key)} \end{itemize} -takeはDSを読み込むためのAPIである。読み込まれたDSは削除される。要求したDSが存在しなければ、CSの待ち合わせ （Blocking）が起こる。putやupdateによりDSに更新があった場合、takeが直ちに実行される。 +takeはDSを読み込むためのAPIである。読み込まれたDSは削除される。要求したDSが存在しなければ、CSの待ち合わせ (Blocking)が起こる。putやupdateによりDSに更新があった場合、takeが直ちに実行される。 \begin{itemize} \item {\ttfamily void peek(String managerKey, String key)} @@ -323,8 +317,7 @@ \newpage \section{CodeSegmentの記述方法} -CSをユーザーが記述する際にはCodeSegmentクラスを継承して記述する(ソースコード \ref{src:StartCodeSegmen -t} , \ref{src:CodeSegment})。 +CSをユーザーが記述する際にはCodeSegmentクラスを継承して記述する(ソースコード \ref{src:StartCodeSegment} , \ref{src:CodeSegment})。 継承することによりCode Segmentで使用するData Segment APIを利用する事ができる。 @@ -339,7 +332,7 @@ \newpage -ソースコード \ref{src:StartCodeSegment} は、5行目で次に実行させたいCS（ソースコード \ref{src:CodeSegment} ）を作成している。 +ソースコード \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}を実行することができる。 @@ -413,6 +406,7 @@ Meta ComputationもCS/DSで作られており、プログラマ側から見えないこれらのCS/DSはMeta CS/Meta DSと呼ばれる。 現在Aliceには、データの圧縮機能、トポロジーの構成・管理機能、ノードの生存確認機能、ノードの切断・再接続時の処理管理機能などのMeta Computationが用意されている。 +これらの有用性は水族館の例題\cite{Aquarium}やTreeVNCの例題\cite{TreeVNC}\cite{AliceVNC}によって示された。 \newpage @@ -420,7 +414,7 @@ リモートノードに大きなデータを送るために、データを圧縮したい場合がある。 そこで、Aliceは圧縮をサポートしている。 しかし、単に圧縮のメソッドを用意したわけではない。 -圧縮データの展開と、圧縮したまま別ノードへの転送を同時に実現したい場合があるため、Meta CSを介すことでDSに圧縮と非圧縮のデータを同時に持てるようにしている（図\ref{fig:compress}）。 +圧縮データの展開と、圧縮したまま別ノードへの転送を同時に実現したい場合があるため、Meta CSを介すことでDSに圧縮と非圧縮のデータを同時に持てるようにしている(図\ref{fig:compress})。 \begin{figure}[h] \begin{center} @@ -434,7 +428,7 @@ \begin{enumerate} \item 一般的なJavaのクラスオブジェクト - \item MessagePack for Java\cite{}でシリアライズ化されたバイナリオブジェクト + \item MessagePack for Java\cite{MessagePack}でシリアライズ化されたバイナリオブジェクト \item 2を圧縮したバイナリオブジェクト \end{enumerate} @@ -446,7 +440,7 @@ \newpage データの圧縮を指定するには、putするDSMの名前の前に"compressed"をつけるだけでよい。 -\ref{src:before},\ref{src:after}は通常のDSと圧縮のDSを扱う際の記述の例である。 +ソースコード\ref{src:before},\ref{src:after}は通常のDSと圧縮のDSを扱う際の記述の例である。 \lstinputlisting[label=src:before, caption=通常のDSを扱うCSの例]{source/beforeCompress.java} \lstinputlisting[label=src:after,caption=圧縮したDSを扱うCSの例]{source/afterCompress.java} @@ -458,15 +452,14 @@ \subsection{TopologyManager} Aliceでは、ノード間の接続管理やトポロジーの構成管理を、Topology ManagerとTopology NodeというMeta Computationが提供している。 プログラマはトポロジーファイルを用意し、Topology Managerに読み込ませるだけでトポロジーを構成することができる。 -トポロジーファイルはDOT Language\cite{}という言語で記述される。 -DOT Languageとは、プレーンテキストを用いてデータ構造としてのグラフを表現するためのデータ記述言語の一 -つである。 +トポロジーファイルはDOT Language\cite{dot}という言語で記述される。 +DOT Languageとは、プレーンテキストを用いてデータ構造としてのグラフを表現するためのデータ記述言語の一つである。 ソースコード\ref{src:topologyfile}は3台のノードでリングトポロジーを組むときのトポロジーファイルの例である。 \lstinputlisting[label=src:topologyfile, caption=トポロジーファイルの例]{source/TopologyFile.dot} DOT Languageファイルはdotコマンドを用いてグラフの画像ファイルを生成することができる。そのため、記述したトポロジーが正しいか可視化することが可能である。 -Topology Managerはトポロジーファイルを読み込み、参加を表明したクライアント（以下、Topology Node）に接続するべきクライアントのIPアドレスやポート番号、接続名を送る（図\ref{fig:topologymanager}）。 +Topology Managerはトポロジーファイルを読み込み、参加を表明したクライアント(以下、Topology Node)に接続するべきクライアントのIPアドレスやポート番号、接続名を送る（図\ref{fig:topologymanager}）。 \newpage @@ -499,7 +492,7 @@ 2.4で示したように、InputDSを記述するには、一度フィールドでReceiverをcreateして、その後Reveiverに対してsetKeyで待ち合わせるkeyを指定しなければならない。 このようにインプットの処理が分離されてしまっていては、記述が煩雑な上にコードを読んだ際にどのkeyに対して待ち合わせを行っているのか直感的に分からない。 -さらに、setKeyは明確な記述場所が決まっていないため、そのDSを待ち合わせているCS以外からも呼び出せてしまう\ref{src:StartSetKey}。 +さらに、setKeyは明確な記述場所が決まっていないため、そのDSを待ち合わせているCS以外からも呼び出せてしまう(ソースコード\ref{src:StartSetKey)})。 \lstinputlisting[label=src:StartSetKey, caption=setKeyを外部から呼び出す例]{source/StartSetKey.java} \lstinputlisting[label=src:SetKey]{source/SetKey.java} @@ -519,7 +512,10 @@ \lstinputlisting[label=src:NullPointerException,caption=NullPointerExceptionになる可能性がある]{source/ShowDataFailed.java} -ソースコード\ref{src:NullPointerException}は、for文でsetKeyとids.createをcntの回数呼び、動的にDSの取得数を決めようとしている。しかし、setKeyが最初に呼ばれた際に、DSの取得に成功すると実行可能と判断されてしまう。runの中でinfoの配列の要素だけ中身を表示させようとしてるが、2回目のasClassでNullPointExceptionを引き起こす。 +ソースコード\ref{src:NullPointerException}は、for文でsetKeyとids.createをcntの回数呼び、動的にDSの取得数を決めようとしている。 +しかし、setKeyが最初に呼ばれた際に、DSの取得に成功すると実行可能と判断されてしまう。 +runの中でinfoの配列の要素だけ中身を表示させようとしてるが、2回目のasClassでNullPointExceptionを引き起こす。 +この問題もインプットAPIの記述の分離により引き起こされるエラーである。 \newpage @@ -576,7 +572,7 @@ より気軽にテストができるよう、同一プログラム内でLocalDSMを複数立ち上げられるようにすべきだと考えた。 \subsection{TopologyManagerの拡張が困難} -Aliceではより自由度の高い通信を行うために、TopologyManagerに幾つかの機能を追加すること考えていた。 +Aliceではより自由度の高い通信を行うために、TopologyManagerに幾つかの機能を追加すること考えていた\cite{OverNAT}。 その一つがNAT越えの機能である。NAT越えは分散アプリケーション構築における課題の1つでもあるが、プログラマにとってその実装は容易ではない。Topology ManagerにNATを越えたノード間通信機能をつけることにより、ネットワークを気にせずに通信が行えるようにしたい。 @@ -607,7 +603,7 @@ 今までのAliceでは、1つのノードに対してTopology Managerは１つと決められていた。 Topology Managerと各ノードのやり取りをするのは、ノードごとに実行されるTopology NodeというMeta Computationである。 -Topology Managerは接続されたnodeの情報（nodeNameとIPアドレスのHashMap）を"nodeTable"というKeyに対応するDSとして保存している。 +Topology Managerは接続されたnodeの情報(nodeNameとIPアドレスのHashMap)を"nodeTable"というKeyに対応するDSとして保存している。 そしてTopology NodeはTopology Managerから割り当てられたnodeNameを"hostname"というKeyに保存する。 つまり、接続するTopology Managerが増えればTopoloyNodeに割り当てられるnodeNameも増えるため、今までのように"hostname"という1つのKeyだけでは対応できない。 １つのノードに複数のTopologyManagerを対応させるには、TopologyNodeが複数のnodeNameを持つ必要がある。 @@ -662,17 +658,17 @@ ChristieはAliceと同じくJavaで書かれている。 -しかし将来的に当研究室が開発するGearsOSに取り入れたいため、GearsOSを構成する言語であるContinuation based C(CbC)に互換可能な設計を目指す。 +しかし将来的に当研究室が開発するGearsOS\cite{GearsOS}に取り入れたいため、GearsOSを構成する言語であるContinuation based C(CbC)に互換可能な設計を目指す。 GearsOSではCodeSegment/DataSegmentと同様の概念としてCodeGear/DataGearという名称を用いているため、Christieでもそれに倣いCodeGear/DataGear(以下、CG/DG)と呼ぶこととする。 \newpage -DGはAliceと同様にDataGearManager（以下DGM）が管理する。 -DGMはLocalとRemoteがあり、全てのDGMはCodeGearManager（以下CGM）で管理される。 +DGはAliceと同様にDataGearManager(以下DGM)が管理する。 +DGMはLocalとRemoteがあり、全てのDGMはCodeGearManager(以下CGM)で管理される。 GearsOSではContextという全てのCG/DGを一括管理するプロセスがあり、AliceのCGMもこのContextに相当する。 -全てのCGMはThreadPoolと他のCGM全てのリストを共有しているため、全てのCG/DGにアクセス可能である（図\ref{fig:christieClass}）。 +全てのCGMはThreadPoolと他のCGM全てのリストを共有しているため、全てのCG/DGにアクセス可能である(図\ref{fig:christieClass})。 \begin{figure}[h] \begin{center} @@ -706,7 +702,7 @@ 先頭に@をつけることで記述でき、オリジナルのアノテーションを定義することもできる。 AliceではInputの受け皿であるReceiverを作り後からkeyをセットしていたが、 -ChristieではInputのためのDGを作り、その上にアノテーションでKeyを指定する（\ref{src:take}）。 +ChristieではInputのためのDGを作り、その上にアノテーションでKeyを指定する(ソースコード\ref{src:take})。 \lstinputlisting[label=src:take, caption=Takeの例]{source/christie/InputDG.java} @@ -719,23 +715,23 @@ また、アノテーションの指定はRUNTIMEではできないため、動的なkeyの指定も防ぐことができる。 このように、アノテーションを用いたことで、Aliceの記述の分離問題が解決された。 -\ref{src:take}の2行目にあるように、InputDGを宣言する際には必ず型の指定が必要となる。 +ソースコード\ref{src:take}の2行目にあるように、InputDGを宣言する際には必ず型の指定が必要となる。 DataGearは様々な型のデータを扱うためにJavaの総称型で受け取るようにしており、\textless \textgreater 内に指定した型でデータの型を限定できる。 このように記述することで、Christieでは他の部分を辿らなくてもCGを見るだけでインプットされるデータの型が分かるように可読性を向上させた。 また、取得してきたDGが指定と違う型であった場合はエラーとなるため、型の整合性を保ちながら信頼性の高いプログラミングが可能となった。 また、Aliceではkeyと変数名の不一致から可読性が低くなっていた。 しかしChristieではkeyと変数名が一致しないとエラーとなるため、自然と読みやすいコードが書けるようになっている。 -この部分に関しては、JavaのメタプログラミングAPIであるjavassist\cite{}を用いてアノテーションから変数の自動生成も試みたが、javassistでは変数生成の前に他のどのクラスも生成してはならないという制限があったため、Christieでは実現できなかった。 +この部分に関しては、JavaのメタプログラミングAPIであるJavassist\cite{javassist}を用いてアノテーションから変数の自動生成も試みたが、Javassistでは変数生成の前に他のどのクラスも生成してはならないという制限があったため、Christieでは実現できなかった。 -リモートノードに対してTake/Peekする際は、RemoteTake/RemotePeekのアノテーションを用いる(\ref{src:remotetake})。 +リモートノードに対してTake/Peekする際は、RemoteTake/RemotePeekのアノテーションを用いる(ソースコード\ref{src:remotetake})。 そのため待ち合わせ先がLocalかRemoteかはアノテーションの違いからひと目でわかるようになった。 \lstinputlisting[label=src:remotetake, caption=RemoteTakeの例]{source/christie/RemoteInputDG.java} -なお、圧縮のMeta ComputationはAliceと同様で、指定する際にDGM名の前にcompressedをつける（\ref{src:compresslocal}）。 +なお、圧縮のMeta ComputationはAliceと同様で、指定する際にDGM名の前にcompressedをつける(ソースコード\ref{src:compresslocal})。 \lstinputlisting[label=src:compresslocal, caption=Localへの圧縮の指定の例]{source/christie/CompressLocal.java} @@ -756,7 +752,7 @@ \newpage -flipも同様にDGMに直接DGを渡す(\ref{src:flip})。 +flipも同様にDGMに直接DGを渡す(ソースコード\ref{src:flip})。 \lstinputlisting[label=src:flip, caption=Remoteへflipする例]{source/christie/Flip.java} @@ -771,7 +767,7 @@ \lstinputlisting[label=src:getdata, caption=getDataの例]{source/christie/GetData.java} Aliceと違う点は、プログラマが型を指定しなくて良い点である。 -4.2.1で示したように、InputDGを生成する際には型を指定する。 +4.3で示したように、InputDGを生成する際には型を指定する。 この型は内部で保存され、リモートノードと通信する際も保たれる。 このようにgetDataするだけでプログラマが指定しなくとも正しい型で取得できるため、プログラマの負担を減らし信頼性を保証することができる。 @@ -795,7 +791,7 @@ CGMを生成した際にLocalDGMやリモートと通信を行うためのDaemonも作られる。 CGに対してアノテーションから待ち合わせを実行する処理はsetupメソッドが行う。 -そのためソースコード\ref{src:StartCodeGear}の13行目、\ref{src:TestCodeGear}の10行目のように、newしたCGをCGMのsetupメソッドに渡す必要がある。 +そのためソースコード\ref{src:StartCodeGear}の13行目、ソースコード\ref{src:TestCodeGear}の10行目のように、newしたCGをCGMのsetupメソッドに渡す必要がある。 AliceではnewすればCGが待ちに入ったが、Christieでは一度CGをnewしないとアノテーションから待ち合わせを行う処理ができないため、newの後にsetupを行う。 そのため、CGの生成には必ずCGMが必要になる。 runでCGMを受け渡すのはこのためである。 @@ -807,7 +803,7 @@ \section{DataGearManagerの複数立ち上げ} AliceではLocalDGMがstaticで書かれていたため複数のLocalDGMを立ち上げることができなかった。 しかしChristieではCGMを２つ生成すればLocalDGMも２つ作られる。 -複数のLocalDGM同士のやりとりも、Remoteへの接続と同じようにRemoteDGMをproxyとして立ち上げアクセスする（図\ref{fig:remoteDGM}）。 +複数のLocalDGM同士のやりとりも、Remoteへの接続と同じようにRemoteDGMをproxyとして立ち上げアクセスする(図\ref{fig:remoteDGM})。 \begin{figure}[h] \begin{center} @@ -819,7 +815,7 @@ \newpage -ソースコード\ref{multilocal}は、LocalDSMを2つ立ち上げ、お互いをリモートに見立てて通信する例である。 +ソースコード\ref{src:multilocal}は、LocalDSMを2つ立ち上げ、お互いをリモートに見立てて通信する例である。 11行目にあるように、RemoteDGMを立ち上げるにはCGMが持つcreateRemoteDGMメソッドを用いる。 引数にはRemoteDGM名と接続するリモートノードのIPアドレス、ポート番号を渡している。 @@ -853,7 +849,7 @@ プログラマはmainでCGMとStartCGを生成する。 CGMと同時にLocalDGMは作られる。 CGが生成され、setupメソッドが呼ばれるとアノテーションからTAKEコマンドが作られ実行される。 -CGは生成したインプットコマンドの総数を初期値としたカウンタを持っており、コマンドが解決される（InputDGが揃う）たびにカウンタは減っていき、0になるとrun内の処理がThreadPoolへ送られる。 +CGは生成したインプットコマンドの総数を初期値としたカウンタを持っており、コマンドが解決される(InputDGが揃う)たびにカウンタは減っていき、0になるとrun内の処理がThreadPoolへ送られる。 \newpage @@ -866,6 +862,7 @@ \includegraphics[width=160mm]{images/RemotePutSequence.pdf} \end{center} \caption{RemoteDGMにPutしたときのフロー} +\label{fig:remotePutSequence} \end{figure} LocalまたはリモードノードからPUTコマンドが実行された際、もしwaitListにPutしたDGを待っているコマンドがあれば実行される。 @@ -894,15 +891,16 @@ \chapter{再設計への考察} InputDGの指定において、CGにDGを宣言するというのは、DGをそのままflipできるようにするためであった。 逆に言えばそれ以外でDataGear型でプログラマが利用することは少ない。 -そのため、DGをアノテーションから生成し完全にメタレイヤーに移すことで、DGの宣言のないより分かりやすい記述が可能だと考える。 -flipする場合は、keyを指定するだけにしたほうが良い。 +そのため、DGを宣言せずにアノテーションから生成し完全にメタレイヤーに移すことで、より分かりやすい記述が可能だと考える。 +flipする場合は、keyを指定するだけで良い。 + また、put/flipする際にDGM名を直接指定する書き方も、まだひと目でアウトプットしている部分が分かるようなシンタックスではないため、改善の余地がある。 DGMは一種のデータベースであると述べたが、現状のDGMはデータベースに必要なトランザクションを持っていない。 当研究室で開発しているJungleデータベースはトランザクションを持っており、更にマージ可能な差分管理システムを持っている。 -そのためJungleデータベースとの統合することで、DGMへの操作を信頼性高くできるようにしたほうが望ましい。 +そのためJungleデータベースとの統合することで、DGMへの操作を信頼性高くすることが望ましい。 -現在はノードごとにDGMとDGのkeyが与えられているが、URLのような大域で使えるkeyを用意することで +また、現在はノードごとにDGMとDGのkeyが与えられているが、将来的にはURLのような大域で使えるkeyを用意することでより手軽なRemoteDGMへのアクセスを提供できると考えられる。 \chapter{結論} \section{まとめ} @@ -927,7 +925,7 @@ \subsection*{GearsOSへの移行} GearsOSはまだ開発途中であったため、本論文の作成時点ではChristieのような分散機能を実装することが叶わなかった。 -GearsOSではモデル検査機構akasha\cite{}があるため、待ちに入っているkeyのputし忘れなどをコンパイルの段階で見つけることができる。 +GearsOSではモデル検査機構akasya\cite{akasya}があるため、待ちに入っているkeyのputし忘れなどをコンパイルの段階で見つけることができる。 GearsOS上で分散プログラミングができればより信頼性の高いプログラミングが期待できるため、将来的にはChristieをGearsOSの分散機構として取り込みたい。 GearsOSにChristieを移行するには、GearsOSにJavaのアノテーションに相当するMeta Computationを実装する必要がある。 @@ -954,7 +952,7 @@ \lstinputlisting[label=src:takeAno, caption=Takeアノテーションの使用例]{source/christie/InputDG.java} \lstinputlisting[label=src:remotetakeAno, caption=RemoteTakeアノテーションの使用例]{source/christie/RemoteInputDG.java} -アノテーションを使う際、()内に記述する値が\ref{src:take}のvalueや\ref{src:remotetake}のdsmNameといったキーに保存される。 +アノテーションを使う際、()内に記述する値がソースコード\ref{src:take}のvalueやソースコード\ref{src:remotetake}のdsmNameといったキーに保存される。 通常キーに対して値を入れる場合は、ソースコード\ref{src:remotetakeAno}のようにkey=の形で記述しなければならないが、Takeのようにキーが1つの場合、キー名をvalueにすることでその記述を省略することができる。 setupメソッド内では生成されたフィールドに対してアノテーションを含めた情報を処理している。 @@ -964,7 +962,7 @@ \lstinputlisting[label=src:setup, caption=reflectionAPIでフィールドの情報を取得]{source/christie/Setup.java} -フィールドから取得したDGとアノテーションから取得したkeyからインプットコマンド（TAKE/PEEK）を生成し、DGMへ送って実行する。 +フィールドから取得したDGとアノテーションから取得したkeyからインプットコマンド(TAKE/PEEK)を生成し、DGMへ送って実行する。 \chapter{謝辞}
--- a/paper/reference.bib Mon Feb 05 14:59:41 2018 +0900 +++ b/paper/reference.bib Mon Feb 05 16:38:28 2018 +0900 @@ -1,5 +1,5 @@ @article{Alice1, - author = {赤嶺一樹, 河野真治}, + author = "赤嶺一樹 and 河野真治", title = {Data segment apiを用いた分散フレームワークの設計}, journal = {日本ソフトウェア科学会第28回大会}, month = Sep, @@ -7,7 +7,7 @@ } @article{Alice2, - author = {杉本優, 河野真治}, + author = "杉本優 and 河野真治", title = {分散フレームワークAliceのDataSegmentの更新に関する改良}, journal = {情報処理学会システムソフトウェアとオペレーティング・システム 研究会(OS)}, month = May, @@ -15,14 +15,14 @@ } @mastersthesis{Aquarium, - author = "杉本 優", + author = "杉本優", title = "分散フレームワークAlice上のMeta Computationと応用", school = "琉球大学 大学院理工学研究科 情報工学専攻", year = "2015" } @mastersthesis{TreeVNC, - author = "谷成 雄", + author = "谷成雄", title = "授業やゼミ向けの画面共有システムTreeVNCの設計と実装", school = "琉球大学 大学院理工学研究科 情報工学専攻", year = "2014" @@ -30,7 +30,7 @@ @article{AliceVNC, - author = {照屋のぞみ, 河野真治}, + author = "照屋のぞみ and 河野真治", title = {分散フレームワークAliceのPC画面配信システムへの応用}, journal = {第57回プログラミング・シンポジウム}, month = Jan, @@ -38,15 +38,23 @@ } @article{OverNAT, - author = {照屋のぞみ, 河野真治}, + author = "照屋のぞみ and 河野真治", title = {分散システム向けのTopology Managerの改良}, journal = {情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS)}, month = May, year = {2016}, } +@article{Framework, + author = "安村恭一 and 河野真治", + title = {動的ルーティングによりタプル配信を行なう分散タプルスペース Federated Linda}, + journal = {日本ソフトウェア科学会第22回大会論文集}, + month = Sep, + year = {2005}, +} + @article{Jungle, - author = {大城信康, 杉本優, 河野真治}, + author = "大城信康 and 杉本優 and 河野真治 and 永山辰巳", title = {Data Segmentの分散データベースへの応用}, journal = {日本ソフトウェア科学会第30回大会論文集}, month = Sep, @@ -70,32 +78,32 @@ @misc{Akka, - title = {}, - howpublished = {\url{}}, + title = {Akka Documentation}, + howpublished = {\url{https://akka.io/docs/}}, note = {Accessed: 2018/02/3(Sat)} } @misc{Hazelcast, - title = {}, - howpublished = {\url{}}, + title = {Hazelcast Documentation}, + howpublished = {\url{https://hazelcast.org/documentation/}}, note = {Accessed: 2018/02/3(Sat)} } @misc{MessagePack, - title = {}, - howpublished = {\url{}}, + title = {MessagePack Documentation}, + howpublished = {\url{http://msgpack.org/}}, note = {Accessed: 2018/02/3(Sat)} } @misc{dot, - title = {}, - howpublished = {\url{}}, + title = {Dot Language Documentation}, + howpublished = {\url{http://www.graphviz.org/}}, note = {Accessed: 2018/02/3(Sat)} } @misc{javassist, - title = {}, - howpublished = {\url{}}, + title = {Javassist Documentation}, + howpublished = {\url{http://jboss-javassist.github.io/javassist/}}, note = {Accessed: 2018/02/3(Sat)} }