Mercurial > hg > Papers > 2020 > anatofuz-sigos

changeset 43:b0757b4dbbe4

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 10:37:02 +0900
parents 4c753956a272
children 698ba8f724d3
files paper/anatofuz-sigos.md paper/anatofuz-sigos.pdf paper/anatofuz-sigos.tex
diffstat 3 files changed, 29 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/paper/anatofuz-sigos.md	Wed May 06 19:12:47 2020 +0900
+++ b/paper/anatofuz-sigos.md	Thu May 07 10:37:02 2020 +0900
@@ -252,7 +252,7 @@
 さらに、 `for`ループをCodeGearに分割することを考えるとループ中にループのindexを利用している場合は、 そのindexも次の継続に渡さなければならない。
 このためindexを使用していないCodeGearでも継続の引数としてindexを受け取り、 実際にindexを利用するCodeGearに伝搬させる必要がある。
 これらの問題を解決する為には、 APIを分割したCodeGearそれぞれのDataGearに型を与え、 どの継続でDataGearの意味が変わるかを追求する必要がある。
-APIを分割して作成したCodeGearのDataGearは、 現在各APIに対応した一つの巨大な構造体に隠蔽されている。
+APIを分割して作成したCodeGearのDataGearは、 現在各APIに対応した1つの巨大な構造体に隠蔽されている。
 巨大な構造体で管理するのではなく、 構造体で次のCodeGearの状態に影響を与える要素を適宜組み合わせたDataGearを作る必要がある。
 
 
@@ -286,8 +286,13 @@
 
     p->sz = PTE_SZ;
     memset(p->tf, 0, sizeof(*p->tf));
+// omission
+}
 ```
 
+Code\ref{src:dumy_function_cbc}中で、 CodeGearへの遷移が行われる`goto vm->init_vmm()`の`vm->void_ret`は`init_vmm`の次の継続のCodeGear名である。
+この`vm->void_ret`は`return`するのみのCodeGearであり、 void型関数と組み合わせることで呼び出し元へと復帰する事が可能となる。
+
 
 # xv6の今後の再実装
 
@@ -296,3 +301,12 @@
 グローバル変数を極力使わず継続を中心とした実装を行いたい。
 
 contextは現在プロセス構造体に埋め込まれており、 kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。
+contextを管理する方法として、 各context間でメッセージなどをやりとりする方法や、 cotnextを主軸にして割り込みなどの処理を再検討するものがある。
+他にはkernelそのもののcontextを定義し、 kernel全体の状態とプロセスの状態をそれぞれ別のcotnextで処理をするというのも検討している。
+
+# まとめ
+
+本稿ではxv6を継続を用いた単位での再実装を検討し、 実際にいくつかの処理を再実装した。
+現状はまだxv6の完全な再実装や、 実装を利用したxv6の証明は行っていないので今後は証明を行いたい。
+それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。
+またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。
\ No newline at end of file
Binary file paper/anatofuz-sigos.pdf has changed
--- a/paper/anatofuz-sigos.tex	Wed May 06 19:12:47 2020 +0900
+++ b/paper/anatofuz-sigos.tex	Thu May 07 10:37:02 2020 +0900
@@ -358,7 +358,7 @@
 さらに、 \texttt{for}ループをCodeGearに分割することを考えるとループ中にループのindexを利用している場合は、 そのindexも次の継続に渡さなければならない。
 このためindexを使用していないCodeGearでも継続の引数としてindexを受け取り、 実際にindexを利用するCodeGearに伝搬させる必要がある。
 これらの問題を解決する為には、 APIを分割したCodeGearそれぞれのDataGearに型を与え、 どの継続でDataGearの意味が変わるかを追求する必要がある。
-APIを分割して作成したCodeGearのDataGearは、 現在各APIに対応した一つの巨大な構造体に隠蔽されている。
+APIを分割して作成したCodeGearのDataGearは、 現在各APIに対応した1つの巨大な構造体に隠蔽されている。
 巨大な構造体で管理するのではなく、 構造体で次のCodeGearの状態に影響を与える要素を適宜組み合わせたDataGearを作る必要がある。
 
 
@@ -392,8 +392,13 @@
 
     p->sz = PTE_SZ;
     memset(p->tf, 0, sizeof(*p->tf));
+// omission
+}
 \end{lstlisting}
 
+Code\ref{src:dumy_function_cbc}中で、 CodeGearへの遷移が行われる\texttt{goto vm->init\_vmm()}の\texttt{vm->void\_ret}は\texttt{init\_vmm}の次の継続のCodeGear名である。
+この\texttt{vm->void\_ret}は\texttt{return}するのみのCodeGearであり、 void型関数と組み合わせることで呼び出し元へと復帰する事が可能となる。
+
 
 \section{xv6の今後の再実装}
 
@@ -402,7 +407,15 @@
 グローバル変数を極力使わず継続を中心とした実装を行いたい。
 
 contextは現在プロセス構造体に埋め込まれており、 kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。
+contextを管理する方法として、 各context間でメッセージなどをやりとりする方法や、 cotnextを主軸にして割り込みなどの処理を再検討するものがある。
+他にはkernelそのもののcontextを定義し、 kernel全体の状態とプロセスの状態をそれぞれ別のcotnextで処理をするというのも検討している。
 
+\section{まとめ}
+
+本稿ではxv6を継続を用いた単位での再実装を検討し、 実際にいくつかの処理を再実装した。
+現状はまだxv6の完全な再実装や、 実装を利用したxv6の証明は行っていないので今後は証明を行いたい。
+それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。
+またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。
 \nocite{*}
 \bibliographystyle{ipsjunsrt}
 \bibliography{anatofuz-bib}