# HG changeset patch # User mir3636 # Date 1547955414 -32400 # Node ID a70aef153f8d0e646cbe1862dc5d9a2c22d75115 # Parent c1783d29c14a79c1fed59000008f90710d0cdb65 update diff -r c1783d29c14a -r a70aef153f8d paper/abstract.tex --- a/paper/abstract.tex Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/abstract.tex Sun Jan 20 12:36:54 2019 +0900 @@ -1,25 +1,32 @@ %OS研究会のまま、要相談 +%これ俺のも par goto 書くの？ \chapter*{要旨} 現代の OS では拡張性と信頼性を両立させることが要求されている。 信頼性をノーマルレベルの計算に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を設計中である。 -Gears OS は Continuation based C によってアプリケーションと OS そのものを記述する。 +Gears OS は Continuation based C (CbC) によってアプリケーションと OS そのものを記述する。 +OS の下ではプログラムの記述は通常の処理の他に、メモリ管理、スレッドの待ち合わせやネットワークの管理、 +エラーハンドリング等の記述しなければならない処理が存在する。 +これらの計算をメタ計算と呼ぶ。 +メタ計算を通常の計算から切り離して記述するために、Code Gear、Data Gear という単位を提案している。 CbC はこの Code Gear と Data Gear の単位でプログラムを記述する。 システムやアプリケーションを記述するためにCode Gear と Data Gear を柔軟に再利用する必要がある。 このときに機能を接続するAPIと実装の分離が可能であることが望ましい。 - Gears OS の信頼性を保証するために、形式化されたモジュールシステムを提供する必要がある。 本論文では、Interface を用いたモジュールシステムの説明とその応用としての並列 API について考察する。 並列APIは継続を基本とした関数型プログラミングと両立する必要がある。 ここでは、CbC の goto 文を拡張したpar goto 文を導入する。 -par goto では並列実行のための実行 Context を生成し、TaskScheduler に登録する。 +par goto では並列実行のための実行 Context を生成し、TaskManager に登録する。 Gears OS での同期機構はData Gear の待ち合わせとして定義する。 メタレベルではこれらの同期機能はCASとそれを用いて実装した Synchronized Queue になる。 これらの Queue も Interface を用いてモジュール化されている。 モジュール化の詳細と、有効性について考察する。 +また、本研究ではハードウェア上でメタレベルの処理、および並列実行を可能とするために、 +Raspberry Pi 上での Gears OS の実装についての考察も行う。 + \chapter*{Abstract} %英語論文 diff -r c1783d29c14a -r a70aef153f8d paper/fig/IO_DataGear.graffle Binary file paper/fig/IO_DataGear.graffle has changed diff -r c1783d29c14a -r a70aef153f8d paper/fig/IO_DataGear.pdf Binary file paper/fig/IO_DataGear.pdf has changed diff -r c1783d29c14a -r a70aef153f8d paper/fig/IO_DataGear.xbb --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/fig/IO_DataGear.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -0,0 +1,8 @@ +%%Title: fig/IO_DataGear.pdf +%%Creator: extractbb 20160307 +%%BoundingBox: 0 0 794 277 +%%HiResBoundingBox: 0.000000 0.000000 794.000000 277.000000 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Fri Jan 18 21:35:54 2019 + diff -r c1783d29c14a -r a70aef153f8d paper/fig/bitonicNetwork.xbb --- a/paper/fig/bitonicNetwork.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/bitonicNetwork.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/bitonicNetwork.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 591 422 %%HiResBoundingBox: 0.000000 0.000000 591.000000 422.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Sat Feb 3 19:57:43 2018 +%%CreationDate: Tue Jan 15 17:52:10 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/bitonicSort.xbb --- a/paper/fig/bitonicSort.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/bitonicSort.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/bitonicSort.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 600 480 %%HiResBoundingBox: 0.000000 0.000000 600.000000 480.000000 %%PDFVersion: 1.5 %%Pages: 1 -%%CreationDate: Sat Feb 3 22:27:55 2018 +%%CreationDate: Tue Jan 15 17:52:10 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/codesegment.pdf Binary file paper/fig/codesegment.pdf has changed diff -r c1783d29c14a -r a70aef153f8d paper/fig/codesegment.xbb --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/fig/codesegment.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -0,0 +1,8 @@ +%%Title: fig/codesegment.pdf +%%Creator: extractbb 20160307 +%%BoundingBox: 0 0 393 201 +%%HiResBoundingBox: 0.000000 0.000000 393.000000 201.000000 +%%PDFVersion: 1.3 +%%Pages: 1 +%%CreationDate: Thu Jan 17 21:34:49 2019 + diff -r c1783d29c14a -r a70aef153f8d paper/fig/cudaArchitecture.xbb --- a/paper/fig/cudaArchitecture.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/cudaArchitecture.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/cudaArchitecture.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 446 488 %%HiResBoundingBox: 0.000000 0.000000 446.000000 488.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Thu Feb 1 07:03:30 2018 +%%CreationDate: Tue Jan 15 17:52:10 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/cudaDataArchitecture.xbb --- a/paper/fig/cudaDataArchitecture.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/cudaDataArchitecture.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/cudaDataArchitecture.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 448 598 %%HiResBoundingBox: 0.000000 0.000000 448.000000 598.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Tue Feb 13 04:47:33 2018 +%%CreationDate: Tue Jan 15 17:52:09 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/meta_cg_dg.xbb --- a/paper/fig/meta_cg_dg.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/meta_cg_dg.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/meta_cg_dg.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 608 202 %%HiResBoundingBox: 0.000000 0.000000 608.000000 202.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Tue Feb 13 00:36:02 2018 +%%CreationDate: Tue Jan 15 17:52:10 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/putSynchronizedQueue1.xbb --- a/paper/fig/putSynchronizedQueue1.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/putSynchronizedQueue1.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/putSynchronizedQueue1.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 746 301 %%HiResBoundingBox: 0.000000 0.000000 746.000000 301.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Jan 24 02:45:08 2018 +%%CreationDate: Tue Jan 15 17:52:10 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/putSynchronizedQueue2.xbb --- a/paper/fig/putSynchronizedQueue2.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/putSynchronizedQueue2.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/putSynchronizedQueue2.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 825 391 %%HiResBoundingBox: 0.000000 0.000000 825.000000 391.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Mon Jan 29 20:29:39 2018 +%%CreationDate: Tue Jan 15 17:52:09 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/sendTask.xbb --- a/paper/fig/sendTask.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/sendTask.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/sendTask.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 722 374 %%HiResBoundingBox: 0.000000 0.000000 722.000000 374.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Tue Feb 13 05:26:03 2018 +%%CreationDate: Tue Jan 15 17:52:10 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/takeSynchronizedQueue1.xbb --- a/paper/fig/takeSynchronizedQueue1.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/takeSynchronizedQueue1.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/takeSynchronizedQueue1.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 571 202 %%HiResBoundingBox: 0.000000 0.000000 571.000000 202.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Jan 24 02:45:08 2018 +%%CreationDate: Tue Jan 15 17:52:10 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/takeSynchronizedQueue2.xbb --- a/paper/fig/takeSynchronizedQueue2.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/takeSynchronizedQueue2.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/takeSynchronizedQueue2.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 561 202 %%HiResBoundingBox: 0.000000 0.000000 561.000000 202.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Wed Jan 24 02:45:08 2018 +%%CreationDate: Tue Jan 15 17:52:09 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/twice.xbb --- a/paper/fig/twice.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/twice.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/twice.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 600 480 %%HiResBoundingBox: 0.000000 0.000000 600.000000 480.000000 %%PDFVersion: 1.5 %%Pages: 1 -%%CreationDate: Tue Feb 6 04:08:41 2018 +%%CreationDate: Tue Jan 15 17:52:10 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/vsgo.xbb --- a/paper/fig/vsgo.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/vsgo.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/vsgo.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 600 480 %%HiResBoundingBox: 0.000000 0.000000 600.000000 480.000000 %%PDFVersion: 1.5 %%Pages: 1 -%%CreationDate: Wed Feb 28 23:36:32 2018 +%%CreationDate: Tue Jan 15 17:52:10 2019 diff -r c1783d29c14a -r a70aef153f8d paper/fig/vsopenmp.xbb --- a/paper/fig/vsopenmp.xbb Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/fig/vsopenmp.xbb Sun Jan 20 12:36:54 2019 +0900 @@ -1,8 +1,8 @@ %%Title: fig/vsopenmp.pdf -%%Creator: extractbb 20170318 +%%Creator: extractbb 20160307 %%BoundingBox: 0 0 600 480 %%HiResBoundingBox: 0.000000 0.000000 600.000000 480.000000 %%PDFVersion: 1.5 %%Pages: 1 -%%CreationDate: Wed Feb 28 23:36:32 2018 +%%CreationDate: Tue Jan 15 17:52:09 2019 diff -r c1783d29c14a -r a70aef153f8d paper/introduction.tex --- a/paper/introduction.tex Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/introduction.tex Sun Jan 20 12:36:54 2019 +0900 @@ -1,10 +1,13 @@ \chapter{OS の拡張性と信頼性の両立} -さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。OS の信頼性を保証する事自体が難しいが、時代とともに進歩する -ハードウェア、サービスに対応して OS 自体が拡張される必要がある。 -OS は非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分であり、テストしきれない部分が残ってしまう。 +さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。 +OS の信頼性を保証する事自体が難しいが、 +時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。 +OS は非決定的な実行を持ち、その信頼性を保証するには、従来のテストとデバッグでは不十分であり、 +テストしきれない部分が残ってしまう。 これに対処するためには、証明を用いる方法とプログラムの可能な実行をすべて数え上げるモデル検査を用いる方法がある。 -モデル検査は無限の状態ではなくても巨大な状態を調べることになり、状態を有限に制限したり状態を抽象化したりする方法が用いられている。 +モデル検査は無限の状態ではなくても巨大な状態を調べることになり、 +状態を有限に制限したり状態を抽象化したりする方法が用いられている。 (図\ref{fig:verification}) \begin{figure}[ht] \begin{center} @@ -15,12 +18,14 @@ \end{figure} 証明やモデル検査を用いて OS を検証する方法はさまざまなものが検討されている。 +%さまざまなものって何？ 検証は一度ですむものではなく、アプリケーションやサービス、デバイスが新しくなることに検証をやり直す必要がある。 つまり信頼性と拡張性を両立させることが重要である。 コンピュータの計算はプログラミング言語で記述されるが、その言語の実行は操作的意味論の定義などで規定される。 +%操作的意味論って何？ プログラミング言語で記述される部分をノーマルレベルの計算と呼ぶ。 -コードが実行される時には、処理系の詳細や使用する資源、あるいは、コードの仕様や型などの言語以外の部分が服属する。 +実際にコードが実行される時には、処理系の詳細や使用する資源、あるいは、コードの仕様や型などの言語以外の部分が服属する。 これをメタレベルの計算という。 この二つのレベルを同じ言語で記述できるようにして、ノーマルレベルの計算の信頼性をメタレベルから保証できるようにしたい。 ノーマルレベルでの正当性を保証しつつ、新しく付け加えられたデバイスやプログラムを含む正当性を検証したい。 @@ -29,19 +34,21 @@ CbC は関数呼出時の暗黙の環境(Environment)を使わずに、コードの単位を行き来できる引数付き goto 文(parametarized goto)を持つ C と互換性のある言語である。 これを用いて、Code Gear と Data Gear、さらにそのメタ構造を導入する。 これらを用いて、検証された Gears OS を構築したい。 -図\ref{fig:MetaGear}。 +%図\ref{fig:MetaGear}。 検証には定理証明支援系である Agda を用いる。 -Gears の記述をモジュール化するために Interface を導入した。 +Gears OS の記述はそのまま Agda に落ちる。 +CbC で記述することによって検証された OS を実装することができる。 + +また、Gears の記述をモジュール化するために Interface を導入した。 さらに並列処理の記述用にpar goto 構文を導入する。 これらの機能は Agda 上で継続を用いた関数型プログラムに対応するようになっている。 -\begin{figure}[ht] - \begin{center} - \includegraphics[width=70mm]{./fig/MetaGear.pdf} - \end{center} - \caption{Gearsのメタ計算} - \label{fig:MetaGear} -\end{figure} +%\begin{figure}[ht] +% \begin{center} +% \includegraphics[width=70mm]{./fig/MetaGear.pdf} +% \end{center} +% \caption{Gearsのメタ計算} +% \label{fig:MetaGear} +%\end{figure} -本論文では Interface と par goto の実装の詳細を記述し評価を行った。 -マルチ CPU と GPU 上での par goto 文の実行を確認した。 - +本論文では Interface と par goto の実装を行なった。 +%実際の修正は考えてない diff -r c1783d29c14a -r a70aef153f8d paper/master_paper.tex --- a/paper/master_paper.tex Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/master_paper.tex Sun Jan 20 12:36:54 2019 +0900 @@ -100,7 +100,7 @@ \input{generate_code.tex} \input{parallelism_gears.tex} %\input{gpu.tex} -\input{evaluation.tex} +%\input{evaluation.tex} \input{conclusion.tex} %謝辞 diff -r c1783d29c14a -r a70aef153f8d paper/meta_computation.tex --- a/paper/meta_computation.tex Fri Jan 04 20:17:57 2019 +0900 +++ b/paper/meta_computation.tex Sun Jan 20 12:36:54 2019 +0900 @@ -1,17 +1,92 @@ \chapter{Gears におけるメタ計算} Gears OS ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を用いる。 -Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、これらを用いてメタ計算を実現する。(図\ref{fig:metaCS}) +プログラムの処理の単位を Code Gear、データの単位を Data Gear と呼ぶ。 +Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、 +これらを用いてメタ計算を実現する。 +Gears OS は処理やデータの構造が Code Gear、Data Gear に閉じているため、 +これにより実行時間、メモリ使用量などを予測可能なものにすることが可能になる。 + +\section{Continuation based C} +CbC は処理を Code Gear とした単位を用いて記述するプログラミング言語である。 +Code Gear 間では軽量継続 (goto文) による遷移を行うので、継続前の Code Gear に戻ることはなく、状態遷移ベースのプログラミングに適している。 +図\ref{fig:cs}は Code Gear 間の処理の流れを表している。 + +\begin{figure}[htpb] + \begin{center} + \scalebox{0.7}{\includegraphics{fig/codesegment.pdf}} + \end{center} + \caption{goto による code gear 間の継続} + \label{fig:cs} +\end{figure} + + +CbC は LLVM\cite{llvm} と GCC\cite{gcc} 上で実装されている。 +Gears OS はこの CbC を用いて記述されている。 + +\section{Code Gear} + +Code Gear は CbC における最も基本的な処理単位である。 +リスト \ref{code_simple} はCbC における Code Gear の一例である。 + +\begin{lstlisting}[frame=lrbt,label=code_simple,caption={\footnotesize code segment の軽量継続}] +__code cs0(int a, int b){ + goto cs1(a+b); +} + +__code cs1(int c){ + goto cs2(c); +} +\end{lstlisting} + +Code Gear は\_\_code Code Gear 名 (引数) の形で記述される。 +Code Gear は戻り値を持たないので、関数とは異なり return 文は存在しない。 +次の Code Gear への遷移は goto Code Gear 名 (引数) で次の Code Gear への遷移を記述する。 +リスト \ref{code_simple} での goto cs1(a+b); がこれにあたる。 +この goto の行き先を継続と呼び、このときの a+b が次の Code Gear への出力となる。 +Scheme の継続と異なり CbC には呼び出し元の環境がないので、この継続は単なる行き先である。 +したがってこれを軽量継続と呼ぶこともある。 +cs1 へ継続した後は cs0 へ戻ることはない。 +軽量継続により、並列化、ループ制御、関数コールとスタックの操作を意識した最適化がソースコードレベルで行えるようにする。 + +\section{Data Gear} +Data Gear は Gears におけるデータの単位である。 +Gears OS では Code Gear は Input Data Gear、Output Data Gear を引数に持ち、 +任意の Input Data Gear を参照し、Output Data Gear を書き出す。\ref{fig:IODataGear} +Code Gear はこのとき渡された引数の Data Gear 以外を参照することはない。 +この Data Gear の対応から依存関係の解決を行う。 \begin{figure}[ht] \begin{center} - \includegraphics[width=70mm]{./fig/metaCS.pdf} + \includegraphics[width=70mm]{fig/IO_DataGear.pdf} + \end{center} + \caption{CodeGear と DataGear} + \label{fig:IODataGear} +\end{figure} + +\section{Meta Code Gear、Meta Data Gear} +Gears OS ではメタ計算 を Meta Code Gear、Meta Data Gear で表現する。 +Meta Code Gear は通常の Code Gear の直後に遷移され、メタ計算を実行する。 +これを図示したものが図\ref{fig:metaCS}である。 + +\begin{figure}[ht] + \begin{center} + \includegraphics[width=70mm]{fig/metaCS.pdf} \end{center} \caption{Gears でのメタ計算} \label{fig:metaCS} \end{figure} -CbC は軽量継続 (goto文) による遷移を行うので、継続前の Code Gear に戻ることはなく、状態遷移ベースのプログラミングに適している。 -CbC は LLVM\cite{llvm} と GCC\cite{gcc} 上で実装されている。 +Gears OS では Context と呼ばれる、使用されるすべての Code Gear、Data Gear を持つ Meta Data Gear を持っている。 +Gears OS は必要な Code Gear、Data Gear を参照したい場合、この Context を通す必要がある。 +しかし Context を通常の計算から直接扱うのはセキュリティ上好ましくない。 +そこで Context から必要なデータを取り出して Code Gear に接続する Meta Code Gear を定義し、 +これを介して間接的に必要な Data Gear にアクセスする。 +この Meta Code Gear を stub Code Gear と呼ぶ。 +stub Code Gear は Code Gear 毎に生成され、次の Code Gear へと継続する前に挿入される。 +goto による継続を行うと、実際には次の Code Gear の stub Code Gear を呼び出す。 + + + メタレベルの記述は Perl スクリプトによって生成される stub と goto meta によって Code Gear で記述される。 Code Gear と Data Gear は Interface と呼ばれるまとまりとして記述される。