%%
%% 研究報告用スイッチ
%% [techrep]
%%
%% 欧文表記無しのスイッチ(etitle,eabstractは任意)
%% [noauthor]
%%

%\documentclass[submit,techrep]{ipsj}
\documentclass[submit,techrep,noauthor]{ipsj}



\usepackage[dvips, dvipdfmx]{graphicx}
\usepackage{latexsym}
\usepackage{listings}
\lstset{
  language=C,
  tabsize=2,
  frame=single,
  basicstyle={\tt\footnotesize}, %
  identifierstyle={\footnotesize}, %
  commentstyle={\footnotesize\itshape}, %
  keywordstyle={\footnotesize\ttfamily}, %
  ndkeywordstyle={\footnotesize\ttfamily}, %
  stringstyle={\footnotesize\ttfamily},
  breaklines=true,
  captionpos=t,
  columns=[l]{fullflexible}, %
  xrightmargin=0zw, %
  xleftmargin=1zw, %
  aboveskip=1zw,
  numberstyle={\scriptsize}, %
  stepnumber=1,
  numbersep=0.5zw, %
  lineskip=-0.5ex
}
\usepackage{caption}


\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
\def\|{\verb|}
%

%\setcounter{巻数}{59}%vol59=2018
%\setcounter{号数}{10}
%\setcounter{page}{1}
\renewcommand{\lstlistingname}{Code}

\begin{document}


\title{GearsOSの分散ファイルシステムの設計}

\etitle{Designing a Distributed File System for GearsOS}

\affiliate{IPSJ}{情報処理学会\\
IPSJ, Chiyoda, Tokyo 101--0062, Japan}


\paffiliate{JU}{琉球大学理工学研究科情報工学専攻\\
Johoshori Uniersity}

\author{一木貴裕}{Ikki Takahiro}{KIE}[ikki-tkhr@cr.ie.u-ryukyu.ac.jp]
\author{河野 真治}{Kono Shinzi}{IE}[kono@ie.u-ryukyu.ac.jp]

\begin{abstract}
本研究室ではgearというプログラミング概念を持つ, 分散フレームワークChristieを開発している. Christieはノード同士がDatagearと呼ばれる変数データを送信しあうことにより, 簡潔に分散プログラムの記述を行うことができる.
このChristieの仕組みを, 同様に本研究室が開発しているGearsOSに組み込み, ファイルシステムを構築したい. GearsOSはノーマルレベルとメタレベルを分けて記述できるContinuation based C(CbC)で構成されており、Christieと近い仕様をもつ. 
\end{abstract}


%
%\begin{jkeyword}
%情報処理学会論文誌ジャーナル，\LaTeX，スタイルファイル，べからず集
%\end{jkeyword}
%
%\begin{eabstract}
%This document is a guide to prepare a draft for submitting to IPSJ
%Journal, and the final camera-ready manuscript of a paper to appear in
%IPSJ Journal, using {\LaTeX} and special style files.  Since this
%document itself is produced with the style files, it will help you to
%refer its source file which is distributed with the style files.
%\end{eabstract}
%
%\begin{ekeyword}
%IPSJ Journal, \LaTeX, style files, ``Dos and Dont's'' list
%\end{ekeyword}

\maketitle

%1
\section{GearsOSのファイルシステムの開発}
当研究室ではOSの信頼性の検証を目的としたOSであるGearsOSを開発している. 
GearsOSはユーザレベルとメタレベルを分離して記述が行える言語であるContinuation based C(以下CbC)で記述されており, Gearというプログラミング概念を持つ.

GearsOSは現在開発途上であるため, 現在は言語フレームワークとしてしか動作しない。OSとして起動するためにこれから実装が必要な機能が多く存在しており, その中の一つとして分散ファイルシステムが挙げられる. 
GearsOSの分散ファイルシステムを構成するために、当研究室が開発している分散フレームワークChristieの仕組みを用いようと考えた. 

ChrsitieはGearsOSのもつGearという概念とよく似た, 別のGearというプログラミング概念を持っており, DataGearと呼ばれる変数データを接続されたノード同士が送信しあうことで分散処理を簡潔に記述することができる. DataGearは指定された型と名前を持つkeyに対応しており, プログラムが必要なkeyにデータが揃ってから初めてプログラムが処理される.
また, ChrisiteはTopologyManagerと呼ばれる機能を持っており, 任意の形でノード同士の配線を行いTopologyを形成する機能を持っている. 

GearsOSの分散処理の記述方式としてChristieの仕組みを取り入れることにより, 分散ファイルシステムを構成したい. 


\section{UNIXファイルシステムについて} 
UNIXファイルシステムはUNIX系OSを始めとした多くのOSのファイルシステムの大元となっている.

UNIXファイルシステムではファイルに構造を持たず,  カーネルがファイルを単純なバイト配列とみなして処理が行われ, ファイルの実際の取り扱いはプログラムが判断する.
ユーザの視点ではファイルを取り扱う際に, OSレベルの観点からファイルを構成する必要がなく, ファイルの拡張子を任意のアプリケーションに適したものにするだけで良い. 
全てのファイルはi-nodeと呼ばれるユニークな番号をもつデータブロックで表される, ファイルのメタデータは全てi-node内に格納されている. ディレクトリ を格納する i-node はファイルの探索の際などに用いられ, ユーザはstat()と呼ばれるシステムコール により大きさなどのファイルのメタ情報を得ることができる.

また, UNIXはデバイスにまたがる仮想ファイルシステムを搭載している. 
例えばネットワークを経由してファイルシステムにアクセスする際は, 木構造に構成されたディレクトリTree にリモート先のファイルシステムをマウントすることにより参照することができる. 

UNIXbaseのファイルシステムと比較・検討をしながらGearsOSを構成していく. 



\section{Continuation based C}
GearsOSはC言語の下位言語であるContinuation based Cを用いて記述されている. CbCは関数呼び出しでなく, 継続を導入しており, スタック領域を用いずjmp命令でコード間を移動することにより軽量な継続を実現している. CbCではこの継続を用いてfor文などのループの代わりに再起呼び出しを行う. 実際のOSやアプリケーションを記述する際にはGCCまたはLLVM/clangのCbC実装を用いる.

CbCでは関数の代わりにCodeGearという単位でプログラミングを行う. CodeGearは\texttt{\_\_code}で宣言を行い, 各CodeGearはDataGearと呼ばれる変数データを入力として受け取り, その結果を別のDataGearに書き込む. 特に入力のDataGearをInputDataGear, 出力されるDataGearを OutputDataGearと呼ぶ. CodeGearとDataGearの関係図を図\ref{fig:cgdg}に示す. 
CodeGearは関数呼び出しのスタックを持たないため, 一度CodeGearを遷移すると元の処理に戻ってくることができない. 


\begin{figure}[h]
    \begin{center}
        \includegraphics[width=80mm]{images/cgdg.pdf}
    \end{center}
        \caption{CodeGearと入出力の関係図}
    \label{fig:cgdg}
\end{figure}

CbCコードの例をソースコード\ref{src:cbc_example}に示す．%refを使う
この例題では特定のシステムコールの場合, CbC で実装された処理に goto 文をつかって継続する. 
例題では CodeGear へのアドレスが配列 cbccodes に格納されている. 引数として渡している\texttt{cbc\_ret}は, システムコールの返り値の数値をレジスタへ代入する CodeGear である. 実際に\texttt{cbc\_ret} に継続が行われるのは、 read などのシステムコールの一連の処理の継続が終わったタイミングである. 

\begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={CbCを利用したシステムコールのディスパッチ}]
void syscall(void)
{
    int num;
    int ret;

    if((num >= NELEM(syscalls)) && (num <= NELEM(cbccodes)) && cbccodes[num]) {
        proc->cbc_arg.cbc_console_arg.num = num;
        goto (cbccodes[num])(cbc_ret);
    }
\end{lstlisting}

Code\ref{src:cbc_example}の状態遷移図を図\ref{fig:cgdg}に示す。
図中の\texttt{cbc\_read}などは、 \texttt{read}システムコールを実装しているCodeGearの集合である。


\section{CbCを用いたOSの記述}
CodeGearの遷移はノーマルレベルから見ると単純にCodeGearがDataGearをInput, Outputを繰り返し, コードブロックを移動しているように見える.
 CodeGearが別のDataGearに遷移する際のDataGearとの関係性を図\ref{fig:meta-cgdg} に示す. ノーマルレベルではDataGearを受け取ったCodeGearを実行, 実行結果をDataGearに書き込み別のCodeGearに継続していると見える. 

しかし, 実際にはCodeGearから別のCodeGearへの遷移にはデータの整合性の確認などのメタ計算が必要となる. 
コード間の遷移に必要となるメタ計算は,  MetaCodeGearと呼ばれるCodeGearごとに実装されたCodeGearで行う. 
MetaCodeGearで参照されるDataGearをMetaDataGearと呼び, また, CodeGearの直前に実行されるMetaCodeGearをStubCodeGearと呼ぶ.
これらMeta計算部分を含めたCodeGearの遷移とDataGearの関係性を図示すると図\ref{fig:meta-cgdg} の下段の形に表せる. CordGearの実行前後に実行されるMetaCodeGearや入出力のDataGearをMetaDataGearから取り出すなどのメタ計算が加わる.

MetaCodeGearは詳細な処理の変更や, スクリプトに問題がある場合を除き, プログラマが直接実装する必要がなく, GearsOSが持つPerlスクリプトにより, GearsOSがビルドされる際に生成される. 

CodeGearの遷移に重要な役割を持つMetaDataGearとしてcontextが存在する。
contextは遷移先のCodeGearとMetaDataGearの紐付けや, 計算に必要なDataGearの保存や管理を行う.
加えてcontextは処理に必要になるCodeGearの番号とMetaCodeGearの対応表や, DataGearの格納場所を持つ. contextと各データ構造の役割を図\ref{fig:context}に示す.
計算に必要なデータ構造と処理を持つデータ構造であることから, contextは従来のOSのプロセスに相当し, ユーザープログラムごとにcontextが存在している.


\begin{figure}[h]
    \begin{center}
        \includegraphics[width=80mm]{images/meta-cg-dg.pdf}
    \end{center}
        \caption{CodeGearとMetaCodeGearの関係図}
    \label{fig:meta-cgdg}
\end{figure}

\begin{figure}[h]
    \caption{Contextを介したCodeGearの継続}
    \begin{center}
        \includegraphics[width=80mm]{images/Context_ref.pdf}
    \end{center}
    \label{fig:context}
\end{figure}


\section{分散フレームワークChristie}
Christieは当研究室で開発されているjava言語で記述された, 分散フレームワークである.
ChristieはCbCと似ているが異なる仕様を持つGearというプログラミング概念を持つ. 
ChristieのGearとして以下の4つのものが存在する.

\begin{itemize}
\item \|CodeGear|（以下CG）
\item \|DataGear|（以下DG）
\item \|CodeGearManager|（以下CGM）
\item \|DataGearManager|（以下DGM）
\end{itemize}

CodeGearはクラスやスレッドに相当する. 
DataGearは変数データであり, CodeGear内でjavaのアノテーションを用いて記述する.
DataGearはKeyと必ず対応しており, putと言う処理によりCG内の全てのKeyにDataGearが揃った際に初めてCGが動作するという仕組みになっている. 

CodeGearManagerはいわゆるノードに相当し, CodeGear, DataGear, DataGearManagerを管理する.  
複数のCodeGearManager同士が配線され,  DGを送信し合うことで分散処理を実現している. 

DataGearManagerはDGを管理しているもので変数プールに相当し, CGMが利用するCGのkeyとputされたデータの組み合わせを所持している. 
DataGearManagerはLocalとRemoteに区分することができ, LocalDGMはCGM自身が所持するDGのプールであり, Localにputすることにより自身の持つkeyにDGを送ることができる.
対するRemoteDataGearManagerはCGMが配線されている別のCGMが持つDGのプールである. つまり, 任意の接続されたRemoteDGMにDGをputすると, 対応したCGM(ノード)が持つLocalDGMのpoolにDGが送信される. RemoteDGMにDGをputする処理が分散処理の肝となっている. RemoteDataGearManagerを図的に表現したものを図\ref{fig:RDGM}に示す.

\begin{figure}[h]
    \begin{center}
        \includegraphics[width=80mm]{images/Remote_DataGearManager.pdf}
    \end{center}
    \caption{RemoteDataGearと接続ノードの関係図}
    \label{fig:RDGM}
\end{figure}


Christieの要となるDataGearのkeyはjavaのアノテーション機能が使われている. アノテーションには以下の4つが存在する. 
\begin{description}
\item[Take] 先頭のDGを読み込み，そのDGを削除する．DGが複数ある場合，この動作を用いる．
\item[Peek] 先頭のDGを読み込むが，DGが削除されない．そのため，特に操作をしない場合は同じデータを参照し続ける．
\item[TakeFrom(Remote DGM name)] Takeと似ているが，Remote DGM nameを指定することで，その接続先(Remote)のDGMからTake操作を行える．
\item[PeekFrom(Remote DGM name)] Peekと似ているが，Remote DGM nameを指定することで，その接続先(Remote)のDGMからPeek操作を行える．
\end{description}


\subsection{Christieのサンプルコード}
コード\ref{codes: StartHelloWorld}, \ref{codes: StartHelloCG}はChristieで記述したHello Worldのプログラムである. 
ユーザープログラムはStartCodeGearクラスを継承したクラス(コード\ref{codes: StartHelloWorld})から開始する. 
CodeGearManagerはポート番号を指定した上でcreateCGMメソッドを呼び出すことにより生成される. 生成されたCodeGearManagerは CGM名.setup にてCGMに処理させたいスレッド, つまりCodeGearを持たせることができる.  

コード \ref{codes: StartHelloCG}はHeloWorldCodeGearの記述である. 
HelloWorldCodeGearではkey: helloWorldにputされた文字列をprint出力するという単純な処理を記述している. 
 CGM名.getLocalDGM().put("Keyname", 変数データ)にてkeyに変数データを紐付け(putし), CodeGearに設定されている全てのkeyがデータを受け取った際に初めてCodeGearは処理される. HelloWorldCodeGearではString型のhelloWorldというkeyがTake型で設定されている.
 
 
 %以下のHelloWorldプログラムを実行した際の流れを説明する.
 %まずポート10000番のCodeGearManagerを生成し, HelloWorldCodeGearをsetupさせる. 
 %この時点では必要なkey(key名: helloWorld)にデータが揃っていないのでCodeGearは実行されない. cgm.getLocalDGM().put("helloWorld","hello");にてhelloWorldkeyに文字列"hello"をputすると, HelloWorldCodeGearに必要なDataGearが揃い, print表示が行われる. 
%プログラム中ではkey:helloWorldへのputは文字列"hello"と"world"の二回が行われ, print出力結果はhello worldと表示される. 


\begin{lstlisting}[frame=lrbt,label=codes: StartHelloWorld,caption={ChristieにおけるCGMとCGのsetup}]
public class StartHelloWorld extends StartCodeGear {

    public StartHelloWorld(CodeGearManager cgm) {
        super(cgm);
    }

    public static void main(String[] args){
        CodeGearManager cgm = createCGM(10000);
        cgm.setup(new HelloWorldCodeGear());
        cgm.getLocalDGM().put("helloWorld","hello");
        cgm.getLocalDGM().put("helloWorld","world");
    }
}
\end{lstlisting}


\begin{lstlisting}[frame=lrbt,label=codes: StartHelloCG,caption={HelloWorldCodeGear}]
public class HelloWorldCodeGear extends CodeGear {
    @Take
    String helloWorld;

    @Override
    protected void run(CodeGearManager cgm) {
        System.out.print(helloWorld + " ");
        cgm.setup(new HelloWorldCodeGear());
    }
}
\end{lstlisting}


\subsection{TopologyManager}
ChristieにはTopologyを形成するための機能TopologyManagerが備わっている.
Topologyに参加するノードに対して名前を与え, 必要とあればノード間の配線を行う. 

TopologyManagerのTopology形成方法として静的Topologyと動的Topologyがある. 
静的Topologyはプログラマが任意の形のTopologyとノードの配線をdotファイルに記述し, TopologyManagerに参照させることで自由な形のTopologyが形成できる. 
現時点では静的TopologyでのTopology形成はdotファイルに記述した参加ノード数に実際に参加するノードの数が達していない場合, 動作しないという制約が存在している. 
動的Topologyは参加を表明したノードに対し, 自動的にノード同士の配線を行う. 例えばTreeを構成する場合, 参加したノードから順番にrootから近い役割を与える. 


\section{GearOSのファイルアクセス}
Christieの分散ファイルシステムをWordCount例題を通して構築する. 
WordCount例題とは指定したファイルの中身の文字列を読み取り, 文字数と行列数, 加えて文字列を出力すると言う例題である. 
WordCountの例題は大きく分けて, 指定した名前のファイルをFile構造体としてOpenするFileOpenスレッド, ファイル構造体を受け取り文字列(word)を表示し文字数(bytes)と行数(lines)をCountUpするWordCountスレッドの二つのCodeGearで記述することができる.  
図\ref{fig:WCStates}で示したWordCountの遷移図はFileをオープンしたCGとWordCountのCGを巡回することにより, ブロックを処理していく. 

WordCountとファイルの接続はUNIXのシェルのようにプログラムの外で接続される. この接続はTopologyManagerによって接続される. 

ファイルシステム側ではBlockを接続されたCGへgotoで接続すればよい. ここではUNIX上のGearsOSであるのでUNIXのファイルシステムAPIを経由してBlockを投げる. この記述ではファイルの読み込みとWordCountの処理がコードとデータの流れに沿って起こる.   
\begin{figure}[h]
    \begin{center}
        \includegraphics[width=80mm]{images/wordCountStates.pdf}
    \end{center}
    \caption{WordCount with CbC}
    \label{fig:WCStates}
\end{figure}

\section{ChristieAPI}
GearsOS上のファイルは名前のついた大域的な資源であり, 複数のプロセスから競合的にアクセスされる. 
前節のAPIではファイルとWordCountが直接的に結合されているので競合的なアクセスは起きない. 
そこでDataGears Streamに名前をつけてアクセスするAPIを導入する. これはjava versionのChristieのGearsOS版となる. 

図\ref{fig:WCDGMwChristie}はFileと分離されたWordCountの結合を表している. 
File InterfaceはBlockをWordCountに送信するが, 直接的に送るのではなく, WordCountの名前がついたDataGearManagerのploxyに書き込む. FileInterfaceからはRemoteDGMとして見れる.
RemoteDGMに書き込む方法は二通りあり, 一つはgoto文のOutPutに指定する方法がある. 
この方法は従来のAPIをつかった方法とほぼ同じになる. 
もう一つはRemoteDGMへputするAPIを使う. この手法では複数のRemoteDGMに書き込むことができる. 

DGの受け取りはCodeGearの入力で行われる. 入力の接続はTopologyManagerに行われるが, 入力のDGにkeyを設定するmetaCG を使う.
他のCGがputしたDGに対応するCGがそのcontextで実行される. 実行されたCGはDGをDGMに書き込むことで計算が進む. 

同じ名前(key)を持つDGは複数のCGから競合的にアクセスされる. RemoteDGMはLocalDGMのploxyであり, 他の計算ノードにあって良い. 
DGMの同期はGearsOSが管理する. 

FileのeofなどはDGにフラグをつけて関数型プログラミング的に処理される. 

図\ref{fig:WCDGMwChristie}はWordCountをRemoteDGMを用いて構成する際の遷移図である. 
NodeAにて任意のファイルを開きDGMを通して1行ごとに文字列をNodeBに送信(put), NodeBにてWordCountの処理を行い, OutputとしてNodeBからWordCountの処理を送り返す. 
NodeA側から送信するファイルの行がなくなった場合, NodeB側にeofを送信して双方の処理を終了するといった流れになる. 

CbCで記述した場合のWordCountプログラムをコード:\ref{codes: UnixF}, \ref{codes: WCImple} に示す.

\begin{figure}[h]
    \begin{center}
        \includegraphics[width=80mm]{images/wordCountDGM.pdf}
    \end{center}
    \caption{WordCountDGM with Christie}
    \label{fig:WCDGMwChristie}
\end{figure}


\begin{lstlisting}[frame=lrbt,label=codes: UnixF,caption={UnixFileImpl.cbc}]
#include <stdio.h>
#impl UnixFileImpl as "UnixFileImpl.h"

File* createUnixFileImpl(struct Context* context) {
    File *file = new File();
    file->FileImpl = (union Data*)new FileImpl();
    return file;
}

readBlock*(UnixFileImpl* file) {
   Block *block = new Block();
   int len = read(fd, BUFSIZE, block->data);
   block->eof &= ~BLOCK_FLAG_EOF;
   if (len <=0 ) {
       block->eof |= BLOCK_FLAG_EOF;
       close(file->fd);
   } 
   return block ;
}

__code unixOpen(UnixFileImpl* file,Key *key, __code next(Block *block,...));
   file->fd = open(key->path,unix_mode(key->modde));
   if (fd < 0) {
       goto error("can't open");
   }
   goto next(readBlock(file), ...);
}

__code unixAck(UnixFileImpl* file,Ack *ack, __code next(Block *block,...));
   if (!ack->isOk) {
      close(file->fd);
      goto next(...);
   }
   goto next(readBlock(file), ...);   // file is automaticaly put into local dataGearManger/input
}
\end{lstlisting}


\begin{lstlisting}[frame=lrbt,label=codes: WCImple,caption={WcImpl.cbc}]
#include "../../../context.h"
#include <stdio.h>
#impl "Wc.h" as "WcImpl.h"
#interface "WcResult.h"

Wc* createWcImpl(struct Context* context) {
    Wc *wc = new Wc();
    wc->wc = (union Data*)new WcImpl();
    wc->bytes = 0;
    wc->words = 0;
    wc->lines = 0;
    return wc;
}

__code take(Impl* wc, Block *block,__code next(Ack *ack, ...),__code finish(StdData *result,...) {
    if (isEof(block->eof )) {
        result.buffer = new Buffer(1);
        result.buffer->data = new Byte(BUSIZE);
        result.size = 1;
        result.buffer->size = 
            snprintf(result.buffer[0]->data, "%d %d %d\n",wc->bytes,wc->words,wc->lines);
        goto finish(resut);
    }
    for(size_t i = 0 ; i<block->size; i++) {
        if (block->data[i] == '\n') wc->lines++;
        if (block->data[i] == ' ') {
            wc->words++;
            while(block->data[i] == ' ') {
               if(i>=block->size) 
                    goto next(ack,take);
               i++;
               wc->bytes++;
            }
        }
        wc->bytes++;
    }
    goto next(ack,take);
}
\end{lstlisting}




\section{FileSystem Implementation}
GearsOS独自のファイルシステムは単なるDGのリストとなる. 要求されたDGをリストから参照してgotoまたはputで送信する. acknowledgeを待って順次送信すれば良い. この場合ではDGはメモリ上にのみ存在する.

持続的なファイルシステムの場合はリストまたはB-TreeをSSDやMVMEなどの持続性のあるデバイスに格納する. 
これらのデバイスは単なるメモリとして扱ってよく, メモリ上のデータ構造と同様に構築する. 

メモリ領域の管理はメタ計算として実装される. メタレベルでGCやDataGear Poolを用いて不要になったメモリの回収を行う. 

このようにDGM自体がファイルの概念に対応する. DGMに格納されているDGには型があり, 正しく接続するには型変換を提供する必要がある. UNIX的にstd Dataのようなものを提供しても良い. 
DGMのデータ構造は複数のものが可能になり, Red-Black-Treeあるいは単方向リストあるいは双方向リストを使うことができる. 
物理デバイス上の重複管理や変更履歴管理もDGMが行う. しかし, ノーマルレベル的には単なるDGのリストとして扱う. つまり検証上は単なるリストとなる. 
図\ref{fig:fileImpletation}はファイルを別ノードにて参照する際の遷移図である.
WordCountと同様な1行ごとの文字列に加え, 読み込みモード, ファイルのパスなどをputする. 送信の制御としてAckもデータとして送信している.  
図\ref{fig:filePersist}はデバイス上に保存されたDGMをLocalDGMとして呼び出し, 操作を行う際の遷移図となる.



\begin{figure}[h]
    \begin{center}
        \includegraphics[width=80mm]{images/fileImplementation.pdf}
    \end{center}
    \caption{file Implementation}
    \label{fig:fileImpletation}
\end{figure}

\begin{figure}[h]
    \begin{center}
        \includegraphics[width=80mm]{images/filePersistency.pdf}
    \end{center}
    \caption{file Persistency}
    \label{fig:filePersist}
\end{figure}

\section{競合的アクセスを含む分散計算の検証}
ChristieAPIは競合的なアクセスを含むので逐次型プログラミングのように検証することができない. TopologyManagerは名前付きDataGearManagerを相互に接続するが, これも動的に変更される. 
これ全体をモデル検査することを考える. 
可能な接続パターンと可能なDGMの内容のパターンを網羅すれば良い. 
一般的にはこれは無限あるいは膨大となるが, 抽象化を導入することにより, より様々なレベルでの検証が可能になることが期待される. 

接続とDGMの内容のパターンが確定すれば, その範囲でプログラムは関数型プログラミングとして振る舞う. 
この場合の検証はHoare Logicなどで証明的に行うことができる. 証明が複雑な場合でも, DGのパターンをメタ計算で調べるなどの手法を用いることができる. 

\section{比較とまとめ}
GearsOSにおけるファイルシステムAPIの設計に対して議論を行った. 
APIは二種類あり, アプリケーションで閉じた決定的な実行を行う直接接続されたものと, もう一つはDataGearManagerに名前をつけて競合的アクセスを許す形でゆるく接続されるものである. 

DataGearManagerはファイルとして見ることもできるし, 分散環境での通信として見ることもできる. 
ファイルシステムの同期, 例えばDataGearの待ち合わせはSynclonised Queue的に行われる. 
Peekを用いるとブロックしない形でRead Onlyアクセスすることが可能になる. 
いずれの場合もアクセスはDataGear単位であり, 不完全な状態なデータになることはない. 

UNIX FileSystemはAPI的にはFile StreamとSocket StreamはRead-Writeでアクセスする.
しかし, その設定はプログラム内部で煩雑な処理が必要となる. 
GearsOSではこの部分はTopologyManagerに押し付けられている. 
UNIXではStreamに型がないので不完全なデータが生じてしまう. 
UNIXファイルシステムにはfsckと呼ばれる修復機能があるが, メモリに対する修復機能は存在しない. 
GearsOS側ではそれらはDGMのメタな機能として実装することが可能である. 
例えばメモリの一部不良などに対応するDGMを作るといったことが可能になると思われる.

DGMの名前とその中のDataGear Streamに対応するkeyでアクセスする対象が決まる. これがUNIXでいうi-node番号に相当する. Human Readableな名前空間はそれらに対して自由に構築して良い. 
UNIXのファイルシステムと異なり, i-nodeの構成と名前空間の構成は独立で良い.
例えばscrap boxのようなTag baseでのアクセスが考えられる. 


\begin{thebibliography}{10}
%かずきさんのAlice　徳森さんのCbC
\bibitem{latex}照屋 のぞみ，河野真治 : \textbf{分散フレームワークChristieの設計}．琉球大学理工学研究科修士論文 2018.
\bibitem{latex}赤嶺 一樹，河野真治 : \textbf{分散ネットワークフレームワークAlice の 提案と実装}．琉球大学理工学研究科修士論文 2012.
\bibitem{aka}赤堀 貴一，河野真治 : \textbf{Christieによるブロックチェーンの実装}．琉球大学工学部情報工学科卒業論文 2019.
\bibitem{latex}徳森 海斗，河野真治 : \textbf{LLVM Clang 上の Continuation based C コンパイラ の改良}．琉球大学理工学研究科修士論文 2016.
\bibitem{latex}清水 隆博，河野真治 : \textbf{xv6 の構成要素の継続の分析}．OS研究会2019.
\bibitem{latex}清水 隆博，河野真治 : \textbf{GearsOSのメタ計算}．琉球大学理工学研究科修士論文 2020.
\bibitem{latex}宮城 光輝，河野真治 : \textbf{継続を基本とした言語による OS のモジュール化}．琉球大学理工学研究科修士論文 2018.
\end{thebibliography}




\end{document}