# HG changeset patch # User mir3636 # Date 1549894927 -32400 # Node ID 3179b8daa958b79de3d3c5ea013fe8dacbb40d7c # Parent c276bcc9b245d7fd94152b993b74d7c9f734d644 update diff -r c276bcc9b245 -r 3179b8daa958 paper/evaluation.tex --- a/paper/evaluation.tex Mon Feb 11 19:05:47 2019 +0900 +++ b/paper/evaluation.tex Mon Feb 11 23:22:07 2019 +0900 @@ -1,121 +1,32 @@ -% GPU が遅いのは cpu, GPU 間のデータの通信の分 -% Meta Data で データが GPU にあるのか, CPU にあるのかをわかるようにする -% CPU で必要なったときに初めて取り出す - -\chapter{Gears OS の評価} - -\section{実験環境} -今回 Twice、 BitonicSort をそれぞれ CPU、GPU環境で Gears OS の測定を行う。 - -使用する実験環境を\tabref{powerEdge}、 GPU 環境を\tabref{gtx1070} に示す。 -また、今回は LLVM/Clang で実装した CbC コンパイラを用いて Gears OS をコンパイルする。 +\chapter{評価} -\begin{table}[htbp] - \begin{center} - \begin{tabular}{|l|l|} \hline - Model & Dell PowerEdgeR630 \\ \hline - OS & CentOS 7.4.1708 \\ \hline - Memory & 768GB \\ \hline - CPU & 2 x 18-Core Intel Xeon 2.30GHz \\ \hline - \end{tabular} - \caption{実行環境} - \label{tab:powerEdge} - \end{center} -\end{table} +本研究では、Gears OS のモジュール化、メタレベルの計算の自動生成、 +xv6 の CbC 書き換えの考察と、システムコールの書き換えを行なった。 -\begin{table}[htbp] - \begin{center} - \begin{tabular}{|l||l|} \hline - GPU & GeForce GTX 1070 \\ \hline - Cores & 1920 \\ \hline - Clock Speed & 1683MHz \\ \hline - Memory Size & 8GB GDDR5 \\ \hline - Memory Bandwidth & 256GB/s \\ \hline - \end{tabular} - \caption{GPU 環境} - \label{tab:gtx1070} - \end{center} -\end{table} +これらの実装についての評価を行う。 -\section{Twice} -Twice は与えられた整数配列のすべての要素を2倍にする例題である。 - -Twice の Task は Gears OS のデータ並列で実行される。 -CPU の場合は配列ある程度の範囲に分割してTaskを生成する。 -これは要素毎に Task を生成するとその分の Context を生成するために時間を取ってしまうからである。 - -Twice は並列実行の依存関係もなく、データ並列での実行に適した課題である。 -そのため、 通信時間を考慮しなければ CPU よりコア数が多い GPU が有利となる。 - -要素数$2^{27}$ のデータに対する Twice の実行結果を \tabref{twice}、\figref{twice}に示す。 -CPU 実行の際は $2^{27}$ のデータを 64個のTask に分割して並列実行を行っている。 -GPU では1次元の block 数を $2^{15}$、 block 内の thread 数を $2^{10}$ で kernel の実行を行った。 -ここでの ``GPU`` は CPU、GPU 間のデータの通信時間も含めた時間、 ``GPU(kernel only)`` は kernel のみの実行時間である。 +\section{Gears OS のモジュール化} +Gears OS の モジュール化について評価を行う。 +Gears OS では、ある Data Gear を Code Gear が扱う場合、 +Code Gear に対応する Data Gear を Context が持つ Data Gear のリストから取り出す必要があるが、 +Context に 全ての Code Gear と Data Gear -\begin{table}[htbp] - \begin{center} - \begin{tabular}{|l||l|} \hline - Processor & Time(ms) \\ \hline - 1 CPU & 1181.215 \\ \hline - 2 CPUs & 627.914 \\ \hline - 4 CPUs & 324.059 \\ \hline - 8 CPUs & 159.932 \\ \hline - 16 CPUs & 85.518\\ \hline - 32 CPUs & 43.496 \\ \hline - GPU & 127.018\\ \hline - GPU(kernel only)& 6.018 \\ \hline - \end{tabular} - \caption{$2^{27}$ のデータに対する Twice} - \label{tab:twice} - \end{center} -\end{table} - -\newpage - -\begin{figure}[htbp] - \begin{center} - \includegraphics[scale=0.6]{./fig/twice.pdf} - \end{center} - \caption{$2^{27}$ のデータに対する Twice} - \label{fig:twice} -\end{figure} - -ある程度の台数効果があると考えられる。 - -GPU での実行は kernel のみの実行時間は 32 CPU に比べて 約 7.2 倍の速度向上が見られた。 -しかし、通信時間を含めると 16 CPU より遅い結果となってしまった。 -CPU、GPU の通信時間かオーバーヘッドになっている事がわかる。 +\begin{lstlisting}[frame=lrbt,label=syscall_list,caption={\footnotesize xv6 のシステムコールのリスト}] +__code cg1 (struct Context* context, struct Element* element) { + struct Node* node1 = new Node(); + element->data = (union Data*)node1; + goto meta(context, pushSingleLinkedStack) +} -\section{Go 言語との比較} -Go 言語 は Google社が開発しているプログラミング言語である。 -Go 言語によるTwice の実装例を\coderef{go}に示す。 - -\lstinputlisting[caption=Go 言語での Twice, label=code:go]{./src/go.go} - -Go 言語は並列実行を ``go function(argv)'' のような構文で行う。 -この並列実行を goroutine と呼ぶ。 - -Go 言語は goroutin 間のデータ送受信をチャネルというデータ構造で行う。 -チャネルによるデータの送受信は ``\textless-'' を使って行われる。 -例えばチャネルのデータ構造であるchannel に対して ``channel \textless- data'' とすると、 data を channel に送信を行う。 -``\textless- channel'' とすると、 channel から送信されたデータを1つ取り出す。 -channel にデータが送信されていない場合はchannel にデータが送信されるまで実行をブロックする。 -Go 言語はチャネルにより、データの送受信が簡潔に書ける。 -しかし、チャネルは複数の goroutine で参照できるためデータの送信元が推測しづらい。 +__code pushSingleLinkedStack(struct Context* context, struct SingleLinkedStack* stack, struct Element *element) { + ... +} -Gears OS では goroutine は par goto 文とほぼ同等に扱うことが出来る。 -また、Code Gear は par goto 文で書き出す Output Data Gear を指定して実行するため、Data Gear の書き出し元が推測しやすい。 - -Go 言語での OpenMP と同様に Twice を実装しGears OS と比較を行う。 -こちらも実行環境は \tabref{powerEdge}、 $2^{27}$ のデータに対して行い、Gears OS、Go 言語両方とも配列を64個のTask、 goroutineに分割して並列実行を行った。 +__code pushSingleLinkedStack_stub(struct Context* context){ + SingleLinkedStack* stack = &context->data[SingleLinkedStack]->SingleLinkedStack; + Element *element = &context->data[Element]->element; + goto pushSingleLinkedStack(context, stack, data) +} -\begin{figure}[htbp] - \begin{center} - \includegraphics[scale=0.6]{./fig/vsgo.pdf} - \end{center} - \caption{vs Go} - \label{fig:vsgo} -\end{figure} - -実行結果として Go 言語は 1CPUと32CPU で約4.33 倍の速度向上が見られた。 -こちらも OpenMP と同じく、台数効果自体は Gears OS が高いが、1CPU での実行時間はGo 言語が大幅に速くなっている。 +\end{lstlisting} + diff -r c276bcc9b245 -r 3179b8daa958 paper/fig/state.graffle Binary file paper/fig/state.graffle has changed diff -r c276bcc9b245 -r 3179b8daa958 paper/fig/state.pdf Binary file paper/fig/state.pdf has changed diff -r c276bcc9b245 -r 3179b8daa958 paper/fig/state.xbb --- a/paper/fig/state.xbb Mon Feb 11 19:05:47 2019 +0900 +++ b/paper/fig/state.xbb Mon Feb 11 23:22:07 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/state.pdf %%Creator: extractbb 20160307 -%%BoundingBox: 0 0 1142 382 -%%HiResBoundingBox: 0.000000 0.000000 1142.000000 382.000000 +%%BoundingBox: 0 0 1142 453 +%%HiResBoundingBox: 0.000000 0.000000 1142.000000 453.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Mon Feb 11 15:19:04 2019 +%%CreationDate: Mon Feb 11 20:08:25 2019 diff -r c276bcc9b245 -r 3179b8daa958 paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r c276bcc9b245 -r 3179b8daa958 paper/master_paper.tex --- a/paper/master_paper.tex Mon Feb 11 19:05:47 2019 +0900 +++ b/paper/master_paper.tex Mon Feb 11 23:22:07 2019 +0900 @@ -99,7 +99,7 @@ \input{interface.tex} \input{generate_code.tex} \input{xv6.tex} -%\input{evaluation.tex} +\input{evaluation.tex} \input{conclusion.tex} %謝辞 diff -r c276bcc9b245 -r 3179b8daa958 paper/meta_computation.tex --- a/paper/meta_computation.tex Mon Feb 11 19:05:47 2019 +0900 +++ b/paper/meta_computation.tex Mon Feb 11 23:22:07 2019 +0900 @@ -185,6 +185,8 @@ 実際には \_\_code meta へと継続している。 \_\_code meta では Context の持つ Code Gear のリストから目的の Code Gear へと継続している。（ソースコード \ref{codemeta}） +\newpage + \begin{lstlisting}[frame=lrbt,label=codemeta,caption={\footnotesize code meta}] __code meta(struct Context* context, enum Code next) { diff -r c276bcc9b245 -r 3179b8daa958 paper/src/console.c --- a/paper/src/console.c Mon Feb 11 19:05:47 2019 +0900 +++ b/paper/src/console.c Mon Feb 11 23:22:07 2019 +0900 @@ -1,77 +1,3 @@ -__code cbc_consoleread2 () -{ - struct inode *ip = proc->cbc_arg.cbc_console_arg.ip; - __code(*next)(int ret) = proc->cbc_arg.cbc_console_arg.next; - if (input.r == input.w) { - if (proc->killed) { - release(&input.lock); - ilock(ip); - goto next(-1); - } - goto cbc_sleep(&input.r, &input.lock, cbc_consoleread2); - } - goto cbc_consoleread1(); -} - -__code cbc_consoleread1 () -{ - int cont = 1; - int n = proc->cbc_arg.cbc_console_arg.n; - int target = proc->cbc_arg.cbc_console_arg.target; - char* dst = proc->cbc_arg.cbc_console_arg.dst; - struct inode *ip = proc->cbc_arg.cbc_console_arg.ip; - __code(*next)(int ret) = proc->cbc_arg.cbc_console_arg.next; - - int c = input.buf[input.r++ % INPUT_BUF]; - - if (c == C('D')) { // EOF - if (n < target) { - // Save ^D for next time, to make sure - // caller gets a 0-byte result. - input.r--; - } - cont = 0; - } - - *dst++ = c; - --n; - - if (c == '\n') { - cont = 0; - } - - if (cont == 1) { - if (n > 0) { - proc->cbc_arg.cbc_console_arg.n = n; - proc->cbc_arg.cbc_console_arg.target = target; - proc->cbc_arg.cbc_console_arg.dst = dst; - proc->cbc_arg.cbc_console_arg.ip = ip; - proc->cbc_arg.cbc_console_arg.next = next; - goto cbc_sleep(&input.r, &input.lock, cbc_consoleread2); - } - } - - release(&input.lock); - ilock(ip); - - goto next(target - n); -} - -__code cbc_consoleread (struct inode *ip, char *dst, int n, __code(*next)(int ret)) -{ - uint target; - - iunlock(ip); - - target = n; - acquire(&input.lock); - - if (n > 0) { - goto cbc_consoleread2(); - } - goto cbc_consoleread1(); -} - int consoleread (struct inode *ip, char *dst, int n) { uint target; @@ -119,16 +45,3 @@ return target - n; } -void consoleinit (void) -{ - initlock(&cons.lock, "console"); - initlock(&input.lock, "input"); - - devsw[CONSOLE].write = consolewrite; - devsw[CONSOLE].read = consoleread; - cbc_devsw[CONSOLE].write = cbc_consolewrite; - cbc_devsw[CONSOLE].read = cbc_consoleread; - - cons.locking = 1; -} - diff -r c276bcc9b245 -r 3179b8daa958 paper/xv6.tex --- a/paper/xv6.tex Mon Feb 11 19:05:47 2019 +0900 +++ b/paper/xv6.tex Mon Feb 11 23:22:07 2019 +0900 @@ -16,14 +16,15 @@ xv6 をモジュール化し、CbC で書き換えることができれば、Gears OS の機能を置き換えることもできる。 図 \ref{fig:xv6Interface} は xv6 の構成図となる。 -\begin{figure}[ht] +\begin{figure}[htp] \begin{center} - \includegraphics[width=150mm]{fig/xv6.pdf} + \includegraphics[width=160mm]{fig/xv6.pdf} \end{center} \caption{モジュール化した xv6 の構成} \label{fig:xv6Interface} \end{figure} +\newpage \section{xv6 の構成要素} xv6 はカーネルと呼ばれる形式をとっている。 @@ -107,7 +108,31 @@ GCC 上で実装した CbC コンパイラを ARM 向けに build し xv6-rpi をコンパイルした。 これにより、 xv6-rpi を CbC で書き換えることができるようになった。 -\section{システムコールの書き換え} +\section{Raspberry Pi} +Raspberry Pi は ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである。 +教育用のコンピューターとして開発されたもので、低価格であり、小型であるため使い勝手が良い。 +ストレージにハードディスクや SSD を使用するのではなく、SD カードを用いる。 +HDMI 出力や USB ポートも備えており、開発に最適である。 + +Raspberry Pi には Raspberry Pi 3、Raspberry Pi 2、Raspberry Pi 1、Raspberry Pi Zero といったバージョンが存在する。 + +\section{CbC によるシステムコールの書き換え} +CbC によるシステムコールの書き換えは、従来の xv6 のシステムコールの形から、 +大きく崩すことなく可能である。 +CbC は Code Gear 間の遷移は goto による継続で行われるため、 +状態遷移ベースでのプログラムに適している。 +xv6 を CbC で書き換えることにより、OS のプログラムを状態遷移モデルに落とし込むことができる。 +これにより状態遷移系のモデル検査が可能となる。 +図 \ref{fig:state} は CbC 書き換えによる read システムコールの遷移図である。 + +\begin{figure}[ht] + \begin{center} + \includegraphics[width=150mm]{fig/state.pdf} + \end{center} + \caption{read システムコールの遷移図} + \label{fig:state} +\end{figure} + ソースコード \ref{syscall} は syscall() におけるシステムコールの呼び出しを行うコードである。 システムコールはソースコード \ref{syscall_list} の関数のリストの番号から呼び出される。 CbC でも同様に num で指定された番号の cbccodes のリストの Code Gear へ goto する。 @@ -151,7 +176,7 @@ CbC は C の関数を呼び出すことも出来るため、書き換えたい部分だけを書き換えることができる。 Code Gear であるため、ソースコード \ref{cbc_read} 7、9行目のように関数呼び出しではなく goto による継続となる。 -\begin{lstlisting}[frame=lrbt,label=sys_read,caption={\footnotesize cbc\_read システムコール}] +\begin{lstlisting}[frame=lrbt,label=cbc_read,caption={\footnotesize cbc\_read システムコール}] __code cbc_read(__code (*next)(int ret)){ struct file *f; int n; @@ -178,7 +203,7 @@ return fileread(f, p, n); } \end{lstlisting} - +ソースコード \ref{cbcfileread} は、ソースコード \ref{fileread} を CbC で書き換えたコードである。 継続で Code Gear 間を遷移するため関数呼び出しとは違い元の関数には戻ってこない。 このため、書き換えの際には ソースコード \ref{cbcfileread} のように分割する必要がある。 プロセスの状態を持つ struct proc は大域変数であるため Code Gear を用いるために必要なパラメーターを cbc\_arg として持たせることにした。 @@ -187,37 +212,21 @@ \lstinputlisting[label=cbcfileread, caption=fileread の CbC 書き換えの例]{./src/fileread.cbc} \lstinputlisting[label=fileread, caption=書き換え前の fileread]{./src/fileread.c} +ソースコード \ref{cbcreadi} は、ソースコード \ref{readi} を書き換えたコードである。 CbC では cbc\_devsw を定義しておりソースコード \ref{cbcreadi} 11行目で次の Code Gear へと継続する。 +cbc\_devsw はソースコード \ref{consoleinit}で初期化されており、cbc\_consoleread へと継続する。 \lstinputlisting[label=cbcreadi, caption=readi の CbC 書き換えの例]{./src/readi.cbc} -\lstinputlisting[label=readi, caption=readi の CbC 書き換えの例]{./src/readi.c} +\lstinputlisting[label=readi, caption=書き換え前の readi]{./src/readi.c} +\lstinputlisting[label=consoleinit, caption=consoleinit]{./src/consoleinit.c} -ソースコード \ref{consoleread} 11、50、行目 では sleep へ継続する際、戻るべき継続先を一緒に送ることで、 +ソースコード \ref{cbc_consoleread} の cbc\_consoleread は、ソースコード \ref{consoleread} を書き換えたものである。 +ソースコード \ref{cbc_consoleread} 11、50、行目 では sleep へ継続する際、戻るべき継続先を一緒に送ることで、 sleep から consoleread に戻ってくることができる。 -\lstinputlisting[label=consoleread, caption=consoleread の CbC 書き換えの例]{./src/console.c} - - -xv6 のシステムコールの関数を CbC で書き換え、QEMU 上で動作させることができた。 - -\section{xv6 の CbC 書き換えによる考察} - -CbC は Code Gear 間の遷移は goto による継続で行われるため、 -状態遷移ベースでのプログラムに適している。 -xv6 を CbC で書き換えることにより、OS のプログラムを状態遷移モデルに落とし込むことができる。 -これにより状態遷移系のモデル検査が可能となる。 +\lstinputlisting[label=cbc_consoleread, caption=consoleread の CbC 書き換えの例]{./src/console.cbc} +\lstinputlisting[label=consoleread, caption=書き換え前の consoleread]{./src/console.c} -また、CbC は Agda に変換できるように設計されているため CbC で記述された実行可能なプログラムが、 -そのまま Agda による定理証明ができる。 - -これらのため、CbC で記述された実行可能な OS そのものがモデル検査と定理証明が可能となり、 -OS の信頼性が保証できる。 - -\section{Raspberry Pi} -Raspberry Pi は ARM\cite{arm} プロセッサを搭載したシングルボードコンピュータである。 -教育用のコンピューターとして開発されたもので、低価格であり、小型であるため使い勝手が良い。 -ストレージにハードディスクや SSD を使用するのではなく、SD カードを用いる。 -HDMI 出力や USB ポートも備えており、開発に最適である。 - -Raspberry Pi には Raspberry Pi 3、Raspberry Pi 2、Raspberry Pi 1、Raspberry Pi Zero といったバージョンが存在する。 - +CbC による書き換えにより、状態遷移ベースへと書き換えることができた。 +現在はシステムコールの書き換えのみであるが、カーネル全体を書き換えることで、 +カーネルを状態遷移モデルに落とし込むことができる。