Mercurial > hg > Papers > 2020 > anatofuz-sigos

changeset 50:5f09000649ef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 07 May 2020 19:53:29 +0900
parents 72805ecaa331
children 305181ddeb7d
files paper/anatofuz-sigos.md paper/anatofuz-sigos.pdf paper/anatofuz-sigos.tex
diffstat 3 files changed, 18 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/paper/anatofuz-sigos.md	Thu May 07 19:10:57 2020 +0900
+++ b/paper/anatofuz-sigos.md	Thu May 07 19:53:29 2020 +0900
@@ -28,8 +28,8 @@
 CbCは`GCC`\cite{gcc}\cite{weko_82695_1}あるいは`LLVM`\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。
 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
 
-現在小さなunixであるxv6 kernelをCbCを用いて再実装している。
-再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
+現在小さなunixであるxv6 kernelをCbCを用いて書き換えている。
+書き換えの為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。
 
 
@@ -128,7 +128,7 @@
 
 
 # xv6のシステムコールの継続の分析と書き換え
-xv6の処理を継続を中心とした記述で再実装を行う。
+xv6の処理を継続を中心とした記述で書き換えを行う。
 この際に、 xv6のどの処理に着目するかによって継続の実装が異なっていくことが実装につれてわかった。
 
 まずxv6の`read` システムコールに着目し、 システムコール内部でどのような状態を遷移するかを分析した。 \cite{weko_195888_1}
@@ -136,7 +136,7 @@
 
 ![lab:fig:cbc_readsyscall, cap:readシステムコールの状態遷移](fig/readsyscall.pdf)
 
-CbCで再実装した`read`システムコールは、 xv6の`read`システムコールのディスパッチ部分から、 `cbc_read`CodeGearに`goto`文で軽量継続される。
+CbCで書き換えた`read`システムコールは、 xv6の`read`システムコールのディスパッチ部分から、 `cbc_read`CodeGearに`goto`文で軽量継続される。
 継続後はreadする対象によって`cbc_readi`や、 `cbc_consoleread`などに状態が変化していく。
 各CodeGearの遷移時にはDataGearがやり取りされる。
 DataGearはxv6のプロセス構造体に埋め込まれたcontextを経由してCodeGearに渡される。
@@ -150,7 +150,7 @@
 
 この事からGearsOSでは、 各CodeGearのモジュール化の仕組みであるInterface機能を導入している。
 Interfaceの導入によってCodeGearを定義することで状態数を増やしても、 抽象化されたAPIを利用することで細部の状態まで意識する必要が無くなった。
-xv6の処理をCbCで再実装する際には、 対象の継続のAPIをまず決定しモジュール化を図る必要がある。
+xv6の処理をCbCで書き換える際には、 対象の継続のAPIをまず決定しモジュール化を図る必要がある。
 
 # xv6のシステムコール以外の継続の分析
 xv6はシステムコール以外に、 ファイルシステムの操作やページテーブルの管理などの処理も存在している。
@@ -291,7 +291,7 @@
 この`vm->void_ret`は`return`するのみのCodeGearであり、 void型関数と組み合わせることで呼び出し元へと復帰する事が可能となる。
 
 
-# xv6の今後の再実装
+# xv6の今後の書き換え
 
 xv6ではカーネルパニックの発生時や、 inodeのキャッシュなどをグローバル変数として利用している。
 グローバル変数を使用してしまうと、 CodeGearで定義した状態がDataGear以外のグローバル変数によって変更されてしまう。
@@ -301,8 +301,8 @@
 contextを管理する方法として、 各context間でメッセージなどをやりとりする方法や、 cotnextを主軸にして割り込みなどの処理を再検討するものがある。
 他にはkernelそのもののcontextを定義し、 kernel全体の状態とプロセスの状態をそれぞれ別のcotnextで処理をするというのも検討している。
 
-現状はxv6の全ての機能をまだCbCを用いて再実装をしていない。
-ファイルシステムや仮想メモリにまつわる処理などはAPI単位では再実装しているが、 APIを呼び出す箇所はCの関数上で部分的に呼び出している。
+現状はxv6の全ての機能をまだCbCを用いて書き換えていない。
+ファイルシステムや仮想メモリにまつわる処理などはAPI単位では書き換えているが、 APIを呼び出す箇所はCの関数上で部分的に呼び出している。
 そのためにOSそのものを状態遷移単位で完全に書き直す必要が存在し、 そのためには全ての処理に対して状態を定義していく必要がある。
 xv6にはアセンブラで記述されている処理も複数存在するため、 CodeGrarの表現においてこのような処理の扱いも決定する必要がある。
 
@@ -314,7 +314,7 @@
 
 # まとめ
 
-本稿ではxv6を継続を用いた単位での再実装を検討し、 実際にいくつかの処理を再実装した。
+本稿ではxv6を継続を用いた単位での書き換えを検討し、 実際にいくつかの処理を書き換えた。
 現状はまだxv6の実装を利用した証明は行っていない。
 今後はモデル検査などを行い、 OSの信頼性を向上させていきたい。
 それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。
Binary file paper/anatofuz-sigos.pdf has changed
--- a/paper/anatofuz-sigos.tex	Thu May 07 19:10:57 2020 +0900
+++ b/paper/anatofuz-sigos.tex	Thu May 07 19:53:29 2020 +0900
@@ -106,8 +106,8 @@
 CbCは\texttt{GCC}\cite{gcc}\cite{weko_82695_1}あるいは\texttt{LLVM}\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。
 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
 
-現在小さなunixであるxv6 kernelをCbCを用いて再実装している。
-再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
+現在小さなunixであるxv6 kernelをCbCを用いて書き換えている。
+書き換えの為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。
 
 
@@ -230,7 +230,7 @@
 
 
 \section{xv6のシステムコールの継続の分析と書き換え}
-xv6の処理を継続を中心とした記述で再実装を行う。
+xv6の処理を継続を中心とした記述で書き換えを行う。
 この際に、 xv6のどの処理に着目するかによって継続の実装が異なっていくことが実装につれてわかった。
 
 まずxv6の\texttt{read} システムコールに着目し、 システムコール内部でどのような状態を遷移するかを分析した。 \cite{weko_195888_1}
@@ -244,7 +244,7 @@
     \label{fig:cbc_readsyscall}
 \end{figure}
 
-CbCで再実装した\texttt{read}システムコールは、 xv6の\texttt{read}システムコールのディスパッチ部分から、 \texttt{cbc\_read}CodeGearに\texttt{goto}文で軽量継続される。
+CbCで書き換えた\texttt{read}システムコールは、 xv6の\texttt{read}システムコールのディスパッチ部分から、 \texttt{cbc\_read}CodeGearに\texttt{goto}文で軽量継続される。
 継続後はreadする対象によって\texttt{cbc\_readi}や、 \texttt{cbc\_consoleread}などに状態が変化していく。
 各CodeGearの遷移時にはDataGearがやり取りされる。
 DataGearはxv6のプロセス構造体に埋め込まれたcontextを経由してCodeGearに渡される。
@@ -258,7 +258,7 @@
 
 この事からGearsOSでは、 各CodeGearのモジュール化の仕組みであるInterface機能を導入している。
 Interfaceの導入によってCodeGearを定義することで状態数を増やしても、 抽象化されたAPIを利用することで細部の状態まで意識する必要が無くなった。
-xv6の処理をCbCで再実装する際には、 対象の継続のAPIをまず決定しモジュール化を図る必要がある。
+xv6の処理をCbCで書き換える際には、 対象の継続のAPIをまず決定しモジュール化を図る必要がある。
 
 \section{xv6のシステムコール以外の継続の分析}
 xv6はシステムコール以外に、 ファイルシステムの操作やページテーブルの管理などの処理も存在している。
@@ -399,7 +399,7 @@
 この\texttt{vm->void\_ret}は\texttt{return}するのみのCodeGearであり、 void型関数と組み合わせることで呼び出し元へと復帰する事が可能となる。
 
 
-\section{xv6の今後の再実装}
+\section{xv6の今後の書き換え}
 
 xv6ではカーネルパニックの発生時や、 inodeのキャッシュなどをグローバル変数として利用している。
 グローバル変数を使用してしまうと、 CodeGearで定義した状態がDataGear以外のグローバル変数によって変更されてしまう。
@@ -409,8 +409,8 @@
 contextを管理する方法として、 各context間でメッセージなどをやりとりする方法や、 cotnextを主軸にして割り込みなどの処理を再検討するものがある。
 他にはkernelそのもののcontextを定義し、 kernel全体の状態とプロセスの状態をそれぞれ別のcotnextで処理をするというのも検討している。
 
-現状はxv6の全ての機能をまだCbCを用いて再実装をしていない。
-ファイルシステムや仮想メモリにまつわる処理などはAPI単位では再実装しているが、 APIを呼び出す箇所はCの関数上で部分的に呼び出している。
+現状はxv6の全ての機能をまだCbCを用いて書き換えていない。
+ファイルシステムや仮想メモリにまつわる処理などはAPI単位では書き換えているが、 APIを呼び出す箇所はCの関数上で部分的に呼び出している。
 そのためにOSそのものを状態遷移単位で完全に書き直す必要が存在し、 そのためには全ての処理に対して状態を定義していく必要がある。
 xv6にはアセンブラで記述されている処理も複数存在するため、 CodeGrarの表現においてこのような処理の扱いも決定する必要がある。
 
@@ -422,7 +422,7 @@
 
 \section{まとめ}
 
-本稿ではxv6を継続を用いた単位での再実装を検討し、 実際にいくつかの処理を再実装した。
+本稿ではxv6を継続を用いた単位での書き換えを検討し、 実際にいくつかの処理を書き換えた。
 現状はまだxv6の実装を利用した証明は行っていない。
 今後はモデル検査などを行い、 OSの信頼性を向上させていきたい。
 それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。