# HG changeset patch # User mir3636 # Date 1549270957 -32400 # Node ID 5927917e18320c88c77a47e1843cc177524e1dae # Parent d61a7ff51f6f3f99b801b7e8981821170043f5fe update diff -r d61a7ff51f6f -r 5927917e1832 paper/conclusion.tex --- a/paper/conclusion.tex Mon Feb 04 17:31:31 2019 +0900 +++ b/paper/conclusion.tex Mon Feb 04 18:02:37 2019 +0900 @@ -28,5 +28,5 @@ Go、との比較から、 Gears OS が1CPU での動作が遅いということがわかった。 Gears OS は par goto 文を使用することで Context を生成し、並列処理を行う。 しかし、Context はメモリ空間の確保や使用する全ての Code/Data Gear を設定する必要があり、生成にある程度の時間がかかってしまう。 -そこで、 par goto のコンパイルタイミングで実行する Code Gear のフローをモデル検査で解析し、処理が軽い場合はContext を生成せずに、関数呼び出しを行う等の最適化を行なうといったチュ>ーニングが必要である。 +そこで、 par goto のコンパイルタイミングで実行する Code Gear のフローをモデル検査で解析し、処理が軽い場合はContext を生成せずに、関数呼び出しを行う等の最適化を行なうといったチューニングが必要である。 diff -r d61a7ff51f6f -r 5927917e1832 paper/fig/Context_ref.graffle Binary file paper/fig/Context_ref.graffle has changed diff -r d61a7ff51f6f -r 5927917e1832 paper/fig/Context_ref.pdf Binary file paper/fig/Context_ref.pdf has changed diff -r d61a7ff51f6f -r 5927917e1832 paper/fig/Context_ref.xbb --- a/paper/fig/Context_ref.xbb Mon Feb 04 17:31:31 2019 +0900 +++ b/paper/fig/Context_ref.xbb Mon Feb 04 18:02:37 2019 +0900 @@ -1,8 +1,8 @@ -%%Title: ./fig/Context_ref.pdf -%%Creator: extractbb 20140317 -%%BoundingBox: 0 0 2000 2000 -%%HiResBoundingBox: 0.000000 0.000000 2000.001000 2000.001000 +%%Title: fig/Context_ref.pdf +%%Creator: extractbb 20160307 +%%BoundingBox: 0 0 766 305 +%%HiResBoundingBox: 0.000000 0.000000 766.000000 305.000000 %%PDFVersion: 1.3 %%Pages: 1 -%%CreationDate: Mon Feb 4 17:30:31 2019 +%%CreationDate: Mon Feb 4 17:33:10 2019 diff -r d61a7ff51f6f -r 5927917e1832 paper/gearsOS.tex --- a/paper/gearsOS.tex Mon Feb 04 17:31:31 2019 +0900 +++ b/paper/gearsOS.tex Mon Feb 04 18:02:37 2019 +0900 @@ -1,4 +1,6 @@ \chapter{Gears OS の構成} +Gears OS は Code Gear、 Data Gear の単位を用いて開発されており、CbC で記述されている。 + Gears OS は以下の要素で構成される。 diff -r d61a7ff51f6f -r 5927917e1832 paper/introduction.tex --- a/paper/introduction.tex Mon Feb 04 17:31:31 2019 +0900 +++ b/paper/introduction.tex Mon Feb 04 18:02:37 2019 +0900 @@ -1,5 +1,27 @@ +\chapter{オペレーティングシステム} + +コンピュータには CPU、ディスプレイ、キーボードやマウス、ハードディスクなど様々な機器が接続されている。 +プログラムの処理を行うとき、これらの様々なデバイスのアクセスや資源管理は複雑で容易ではない。 +異なるハードウェアを扱う際にはそれぞれに対応したプログラミングを行う必要がある。 +OS とはこれらのデバイスの抽象化や資源管理を行う。 + +ユーザーは OS のおかげで異なるハードウェアの違いを意識することなくプログラミングをすることができる。 +例えば同じプログラムで、異なる入力デバイスによる操作や、ディスプレイでの表示などは、 +デバイスへのアクセスなどの複雑な処理を OS が隠すことによってユーザーが意識せずにプログラミングを行える。 + +CPU、メモリ、ディスク、などの本来ユーザーが意識しなければならない資源も、OS が資源管理を行うことで意識することなくプログ +ラミングすることができる。 + +1950年代におけるコンピューターがプログラムを実行する際には専門のオペレータが存在し、オペレーターがジョブの管理、コンパイ +ラの選択などを行なっていた。 +しかし後に、ジョブの自動実行、やコンパイラのロードを行うプログラムができた。これが OS の祖先である。 +コンピュータには科学技術用のコンピューターと商用のコンピューターが開発されていたが、後に汎用コンピューターである System/360 が開発される。 +System/360 の OS/360 は強力なソフトウェア互換を持っていた。 +ソフトウェア互換により全てのソフトウェアが全てのマシンで動作するようになった。 +この頃の OS には、スプーリングやタイムシェアリングといった機能も導入されるようになった。 +その後、UNIX が開発され後に様々なバージョンが開発され、System V、BSD といった派生 OS なども開発され、現在に至る。 + \chapter{OS の拡張性と信頼性の両立} - さまざまなコンピュータの信頼性の基本はメモリなどの資源管理を行う OS である。 OS の信頼性を保証する事自体が難しいが、 時代とともに進歩するハードウェア、サービスに対応して OS 自体が拡張される必要がある。 @@ -35,11 +57,28 @@ これを用いて、Code Gear と Data Gear、さらにそのメタ構造を導入する。 これらを用いて、検証された Gears OS を構築したい。 図\ref{fig:MetaGear}。 -検証には定理証明支援系である Agda を用いる。 + +本論文では、Gears OS の要素である Code Gear、Data Gear、そして、Meta Code Gear 、Meta Data Gear の構成を示す。これらは、CbC に変換されて実行される。 +Gears OS は、Task Scheduler を CPU や GPU 毎に持ち、一つの Task に対応する Context という Meta Data Gear を使用しながら計算を実行する。 + +Meta Gear を入れかえることにより、ノーマルレベルの Gear をモデル検査することができるようにしたい。 +ノーマルレベルでの Code Gear と Data Gear は継続を基本とした関数型プログラミング的な記述に対応する。 +この記述を定理証明支援系である Agda を用いて直接に証明できるようにしたい。 Gears OS の記述はそのまま Agda に落ちる。 -CbC で記述することによって検証された OS を実装することができる。 +Code Gear、Data Gear を用いた言語である CbC で記述することによって検証された OS を実装することができる。 + +従来の研究でメタ計算を用いる場合は、関数型言語では Monad を用いる\cite{Moggi:1989:CLM:77350.77353}。これは Hakell では実行時の環境を記述する構文として使われている。 +OS の研究では、メタ計算の記述に型つきアセンブラ(Typed Assembler)を用いることがある\cite{Yang:2010:SLI:1806596.1806610}。Python や Haskell による記述をノーマルレベルとして +採用した OS の検証の研究もある\cite{Klein:2009:SFV:1629575.1629596,Chen:2015:UCH:2815400.2815402}。 +SMIT などのモデル検査を OS の検証に用いた例もある\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}。 -また、Gears の記述をモジュール化するために Interface を導入した。 +本研究で用いる Meta Gear は制限された Monad に相当し、型つきアセンブラよりは大きな表現単位を提供する。 +Haskell などの関数型プログラミング言語では実行環境が複雑であり、実行時の資源使用を明確にすることができない。 +CbC はスタック上に隠された環境を持たないので、メタレベルで使用する資源を明確にできるという利点がある。 +ただし、Gear のプログラミングスタイルは、従来の関数呼出を中心としたものとはかなり異なる。 + + +また、本研究では Gears の記述をモジュール化するために Interface を導入した。 さらに並列処理の記述用にpar goto 構文を導入する。 これらの機能は Agda 上で継続を用いた関数型プログラムに対応するようになっている。 \begin{figure}[ht] diff -r d61a7ff51f6f -r 5927917e1832 paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r d61a7ff51f6f -r 5927917e1832 paper/meta_computation.tex --- a/paper/meta_computation.tex Mon Feb 04 17:31:31 2019 +0900 +++ b/paper/meta_computation.tex Mon Feb 04 18:02:37 2019 +0900 @@ -1,6 +1,20 @@ \chapter{Gears におけるメタ計算} -Gears OS ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を用いる。 +プログラムを記述する際、ノーマルレベルの処理の他に、メモリ管理、スレッド管理、CPU や GPU の資源管理等、記述しなければならない処理が存在する。 +これらの計算をメタ計算と呼ぶ。 + +従来の OS では、メタ計算はシステムコールやライブラリーコールの単位で行われる。 +実行時にメタ計算の変更を行う場合には、OS 内部のパラメータの変更を使用し、 +実行されるユーザープログラム自体への変更は限定的である。 +しかし、メタ計算は性能測定あるいはプログラム検証、さらに並列分散計算のチューニングなど細かい処理が必要で +実際のシステムコール単位では不十分である。 +例えば、モデル検査ではアセンブラあるいはバイトコード、インタプリタレベルでのメタ計算が必要になる。 +しかし、バイトコードレベルでは粒度が細かすぎて扱いが困難になっている。 +具体的にはメタ計算の実行時間が大きくなってしまう。 + +メタ計算を通常の計算から切り離して記述するためには処理を細かく分割する必要がある。しかし、関数やクラスなどの単位は容易に分割できない。 +そこで当研究室ではメタ計算を柔軟に記述するためのプログラミング言語の単位として Code Gear、Data Gear という単位を提案している。 プログラムの処理の単位を Code Gear、データの単位を Data Gear と呼ぶ。 +これによりシステムコードよりも細かくバイトコードよりも大きなメタ計算の単位を提供できる。 Code Gear、Data Gear にはそれぞれメタレベルの単位である Meta Code Gear、Meta Data Gear が存在し、 これらを用いてメタ計算を実現する。 @@ -29,6 +43,7 @@ \section{Code Gear} Code Gear は CbC における最も基本的な処理単位である。 +関数に比べて細かく分割されているのでメタ計算をより柔軟に記述できる。 ソースコード \ref{code_simple} はCbC における Code Gear の一例である。 \begin{lstlisting}[frame=lrbt,label=code_simple,caption={\footnotesize code segment の軽量継続}] @@ -51,6 +66,8 @@ cs1 へ継続した後は cs0 へ戻ることはない。 軽量継続により、並列化、ループ制御、関数コールとスタックの操作を意識した最適化がソースコードレベルで行えるようにする。 +CbC は軽量継続による遷移を行うので、継続前の Code Gear に戻ることはなく、状態遷移ベースのプログラミングに適している。 + \section{Data Gear} Data Gear は Gears OS におけるデータの単位である。 Gears OS では Code Gear は Input Data Gear、Output Data Gear を引数に持ち、 @@ -97,6 +114,11 @@ \section{Meta Code Gear、Meta Data Gear} Gears OS ではメタ計算 を Meta Code Gear、Meta Data Gear で表現する。 +CbC での記述はメタ計算を含まないノーマルレベルでの記述と、 Code Gear、Data Gear の記述を含むメタレベルの記述の2種類がある。 +メタレベルでもさらに、メタ計算を用いることが可能になっている。 +この2つのレベルはプログラミング言語レベルでの変換として実現される。 +メタレベルでの変換系は本論文では、Perl による変換スクリプトにより実装されている。 + Meta Code Gear は通常の Code Gear の直前、直後に遷移され、メタ計算を実行する。 Code Gear はノーマルレベルでは図 \ref{fig:normal_Code_Gear} のように見える。 メタレベルでは Code Gear は図 \ref{fig:meta_Code_Gear} のように継続を行なっている。 @@ -156,7 +178,6 @@ これにより Interface 間の呼び出しを C++ のメソッド呼び出しのように記述することができる。 Interface の実装は、Context 内に格納されているので、オブジェクトごとに実装を変える多様性を実現できている。 - Context を複製して複数の CPU に割り当てることにより並列実行を可能になる。 これによりメタ計算として並列処理を記述したことになる。 Gears のスレッド生成は Agda の関数型プログラミングに対応して行われるのが望ましい。