Mercurial > hg > Papers > 2020 > anatofuz-sigos

--- a/paper/anatofuz-sigos.md	Thu May 07 19:53:29 2020 +0900
+++ b/paper/anatofuz-sigos.md	Thu May 07 20:15:26 2020 +0900
@@ -20,9 +20,9 @@

 ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。
 CbCは基本`goto`で`CodeGaar`というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と
-呼ばれる隠れた状態を持たない。このため、計算のための情報は`CodeGear`の入力にすべてそろっている。そのうちのいくつかはメタ計算、
-つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)である。メタ計算とノーマルレベルの
-区別は入力のどこを扱うかの差に帰着される。
+呼ばれる隠れた状態を持たない。このため、計算のための情報は`CodeGear`の入力にすべてそろっている。
+そのうちのいくつかはメタ計算、つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)である。
+メタ計算とノーマルレベルの区別は入力のどこを扱うかの差に帰着される。
 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
 CbCは`GCC`\cite{gcc}\cite{weko_82695_1}あるいは`LLVM`\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。
@@ -56,6 +56,7 @@
 この例題では特定のシステムコールの場合、 CbCで実装された処理に`goto`文をつかって継続する。
 例題ではCodeGearへのアドレスが配列`cbccodes`に格納されている。
 引数として渡している`cbc_ret`は、 システムコールの返り値の数値をレジスタに代入するCodeGearである。
+実際に`cbc_ret`に継続が行われるのは、 `read`などのシステムコールの一連の処理の継続が終わったタイミングである。

 ``` lab:src:cbc_example, cap:CbCを利用したシステムコールのディスパッチ
 void syscall(void)
@@ -69,7 +70,10 @@
     }
 ```

-![lab:fig:factorial_cbc, cap:CbCを利用したシステムコールディスパッチの状態遷移](fig/cbc_syscall_Trap)
+Code\ref{src:cbc_example}の状態遷移図を図\ref{fig:dispatch}に示す。
+図中の`cbc_read`などは、 `read`システムコールを実装しているCodeGearの集合である。
+
+![lab:fig:dispatch, cap:CbCを利用したシステムコールディスパッチの状態遷移](fig/syscall_dispatch.pdf)

 CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。
 しかしCodeGearを呼び出す直前のスタックは保存されるため、 部分的にCbCを適用する場合はCodeGearを呼び出す`void`型などの関数を経由することで呼び出しが可能となる。
@@ -158,6 +162,8 @@
 システムコールの一連の流れに着目するのではなく、 特定の対象のAPIに着目して継続の分析を検討した。

 xv6のファイルシステムに関する関数などのAPIは主に`fs.c`中に記述されている。
+APIの内部をCodeGearに分割をすると、 APIを呼び出す時点でAPI細部の継続を考慮する必要がある。
+細部の継続を隠蔽するために、 抽象的に複数のCodeGearをまとめる機能であるInterfaceを導入したい。
 Code\ref{src:fs_interface}に示す様に、 `fs.c`中に定義されているAPIを抜き出し、 CbCのInterfaceとして定義した。
 `__code`から始まるCodeGearの名前が、 それぞれ抽象化されたCodeGearの集合の最初の継続となる。

@@ -298,25 +304,18 @@
 グローバル変数を極力使わず継続を中心とした実装を行いたい。

 contextは現在プロセス構造体に埋め込まれており、 kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。
-contextを管理する方法として、 各context間でメッセージなどをやりとりする方法や、 cotnextを主軸にして割り込みなどの処理を再検討するものがある。
-他にはkernelそのもののcontextを定義し、 kernel全体の状態とプロセスの状態をそれぞれ別のcotnextで処理をするというのも検討している。

 現状はxv6の全ての機能をまだCbCを用いて書き換えていない。
 ファイルシステムや仮想メモリにまつわる処理などはAPI単位では書き換えているが、 APIを呼び出す箇所はCの関数上で部分的に呼び出している。
 そのためにOSそのものを状態遷移単位で完全に書き直す必要が存在し、 そのためには全ての処理に対して状態を定義していく必要がある。
-xv6にはアセンブラで記述されている処理も複数存在するため、 CodeGrarの表現においてこのような処理の扱いも決定する必要がある。

 またOS上でDataGearとCodeGearの位置づけを明確に定義する必要も存在する。
-現在は関数を分割した状態としてCodeGearを定義している。
 DataGearの依存関係やCodeGearの並列実行など、 プロセスベースで実装していた処理をCodeGearなどで意味がある形式にする必要がある。

-またxv6にはユーザーコマンドも存在しているために、 ユーザーコマンド向けのCbCのAPIなども考慮したい。
-
 # まとめ

 本稿ではxv6を継続を用いた単位での書き換えを検討し、 実際にいくつかの処理を書き換えた。
-現状はまだxv6の実装を利用した証明は行っていない。
-今後はモデル検査などを行い、 OSの信頼性を向上させていきたい。
-それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。
+書き換えはシステムコールに着目しCodeGearへ分割する手法と、 BasicBlockごとにCodeGearへ分割する手法で行った。
+現状はまだxv6の実装を利用した証明や、 xv6にモデル検査機能の実装を行いたい。
 またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。
Binary file paper/anatofuz-sigos.pdf has changed
--- a/paper/anatofuz-sigos.tex	Thu May 07 19:53:29 2020 +0900
+++ b/paper/anatofuz-sigos.tex	Thu May 07 20:15:26 2020 +0900
@@ -98,9 +98,9 @@

 ノーマルレベルの計算とメタ計算の両方の実装に適した言語としてContinuation Based C(CbC)がある。
 CbCは基本\texttt{goto}で\texttt{CodeGaar}というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と
-呼ばれる隠れた状態を持たない。このため、計算のための情報は\texttt{CodeGear}の入力にすべてそろっている。そのうちのいくつかはメタ計算、
-つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)である。メタ計算とノーマルレベルの
-区別は入力のどこを扱うかの差に帰着される。
+呼ばれる隠れた状態を持たない。このため、計算のための情報は\texttt{CodeGear}の入力にすべてそろっている。
+そのうちのいくつかはメタ計算、つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(DataGear)である。
+メタ計算とノーマルレベルの区別は入力のどこを扱うかの差に帰着される。
 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
 CbCは\texttt{GCC}\cite{gcc}\cite{weko_82695_1}あるいは\texttt{LLVM}\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。
@@ -140,6 +140,7 @@
 この例題では特定のシステムコールの場合、 CbCで実装された処理に\texttt{goto}文をつかって継続する。
 例題ではCodeGearへのアドレスが配列\texttt{cbccodes}に格納されている。
 引数として渡している\texttt{cbc\_ret}は、 システムコールの返り値の数値をレジスタに代入するCodeGearである。
+実際に\texttt{cbc\_ret}に継続が行われるのは、 \texttt{read}などのシステムコールの一連の処理の継続が終わったタイミングである。

 \begin{lstlisting}[frame=lrbt,label=src:cbc_example,caption={CbCを利用したシステムコールのディスパッチ}]
 void syscall(void)
@@ -153,12 +154,15 @@
     }
 \end{lstlisting}

+Code\ref{src:cbc_example}の状態遷移図を図\ref{fig:dispatch}に示す。
+図中の\texttt{cbc\_read}などは、 \texttt{read}システムコールを実装しているCodeGearの集合である。
+
 \begin{figure}[tb]
     \begin{center}
-        \includegraphics[width=80mm]{fig/cbc_syscall_Trap}
+        \includegraphics[width=80mm]{fig/syscall_dispatch.pdf}
     \end{center}
     \caption{CbCを利用したシステムコールディスパッチの状態遷移}
-    \label{fig:factorial_cbc}
+    \label{fig:dispatch}
 \end{figure}

 CodeGearは関数呼び出し時のスタックを持たない為、一度あるCodeGearに遷移してしまうと元の処理に戻ってくることができない。
@@ -266,6 +270,8 @@
 システムコールの一連の流れに着目するのではなく、 特定の対象のAPIに着目して継続の分析を検討した。

 xv6のファイルシステムに関する関数などのAPIは主に\texttt{fs.c}中に記述されている。
+APIの内部をCodeGearに分割をすると、 APIを呼び出す時点でAPI細部の継続を考慮する必要がある。
+細部の継続を隠蔽するために、 抽象的に複数のCodeGearをまとめる機能であるInterfaceを導入したい。
 Code\ref{src:fs_interface}に示す様に、 \texttt{fs.c}中に定義されているAPIを抜き出し、 CbCのInterfaceとして定義した。
 \texttt{\_\_code}から始まるCodeGearの名前が、 それぞれ抽象化されたCodeGearの集合の最初の継続となる。

@@ -406,26 +412,19 @@
 グローバル変数を極力使わず継続を中心とした実装を行いたい。

 contextは現在プロセス構造体に埋め込まれており、 kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。
-contextを管理する方法として、 各context間でメッセージなどをやりとりする方法や、 cotnextを主軸にして割り込みなどの処理を再検討するものがある。
-他にはkernelそのもののcontextを定義し、 kernel全体の状態とプロセスの状態をそれぞれ別のcotnextで処理をするというのも検討している。

 現状はxv6の全ての機能をまだCbCを用いて書き換えていない。
 ファイルシステムや仮想メモリにまつわる処理などはAPI単位では書き換えているが、 APIを呼び出す箇所はCの関数上で部分的に呼び出している。
 そのためにOSそのものを状態遷移単位で完全に書き直す必要が存在し、 そのためには全ての処理に対して状態を定義していく必要がある。
-xv6にはアセンブラで記述されている処理も複数存在するため、 CodeGrarの表現においてこのような処理の扱いも決定する必要がある。

 またOS上でDataGearとCodeGearの位置づけを明確に定義する必要も存在する。
-現在は関数を分割した状態としてCodeGearを定義している。
 DataGearの依存関係やCodeGearの並列実行など、 プロセスベースで実装していた処理をCodeGearなどで意味がある形式にする必要がある。

-またxv6にはユーザーコマンドも存在しているために、 ユーザーコマンド向けのCbCのAPIなども考慮したい。
-
 \section{まとめ}

 本稿ではxv6を継続を用いた単位での書き換えを検討し、 実際にいくつかの処理を書き換えた。
-現状はまだxv6の実装を利用した証明は行っていない。
-今後はモデル検査などを行い、 OSの信頼性を向上させていきたい。
-それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。
+書き換えはシステムコールに着目しCodeGearへ分割する手法と、 BasicBlockごとにCodeGearへ分割する手法で行った。
+現状はまだxv6の実装を利用した証明や、 xv6にモデル検査機能の実装を行いたい。
 またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/fig/syscall_dispatch.drawio	Thu May 07 20:15:26 2020 +0900
@@ -0,0 +1,1 @@
+<mxfile host="app.diagrams.net" modified="2020-05-07T11:06:29.868Z" agent="5.0 (Macintosh)" etag="PMsrwCwIZCRMYiVRvmiZ" version="13.0.8" type="device"><diagram id="SqVz1idNpBTpqpkpe1dT" name="Page-1">7Vhdb9owFP01PHYicULgkY+WVVqlSUjb3iovNolXE2eOacJ+/W4a54uYARsImPqEc2xf2+fcHF/SQ9NVNpc4Dp8Eobxn90nWQ7OebVv9vgU/ObIpENdzCiCQjOhBNbBgv2g5U6NrRmjSGqiE4IrFbdAXUUR91cKwlCJtD1sK3l41xgHtAAsf8y76lREVFujQ9mr8I2VBWK5sDUZFzwqXg/VJkhATkTYgdN9DUymEKlqrbEp5Tl7JSzHvYUdvtTFJI3XIhB/OZj5//hSQx8WD+/T4Mgy+fLuztBqvmK/1ifVu1aakAMIA2/AwSUOm6CLGft6TguCAhWrF4cmCJk7iQoIlyyisOkmUFC8VbwgQvRqVimY7z2FV7EBaUbGiSm5giJ7gDDWhOqOqVElrfSyksbCpTQlinRNBFbumDRqauWNYRLfHIro+Fu3bY3HUZhFdnkTr9kh09pPomEh0zkaigcMBh2UnSwFnapI5+LkWZcdd8nZ9jWEA6sdZ3QmtIP9NNgncLLwMBnsr4hW9HZ2uQh2vLY5lG9SxTOpY51LHZBPHqWO7JnX87/5zKoHyQ/W5svcIbZmRc3EzMl2Lp1JKUkz+E6Gu4O49oAyE+jXOm0tOs3FeWQMZNCK6OfM5ThLmt/ls0+dU9FHSqbr3ktcgxzVwU2KScqzYazu8iS+9wmfB3lJRa1OV66Xfec4Htx0kEWvpUz2vWXBvhULu3lAKy4CqTijgFG8aw+J8QPKHTQ92rbRrb/ZwzwxoFLuoc6rS4u/TzP13QzBerIFQ4lAzgPdWmbJ0KriQgEQiyp1iyTjfgjBnQZSnOqQqBXySuwCDG32sO1aMEL7LZqRYRyQ3lVn/NDayrbrd79qIqW6yz2Uiw3cT0WFGJzMRb78fnchEBuhYExnsNLizmsjo3UROZyLbql/cRMpa6ExFo7rRmtHb/h9m0OlkNSM81t8li9e2/rqL7n8D</diagram></mxfile>
\ No newline at end of file
Binary file paper/fig/syscall_dispatch.pdf has changed