# HG changeset patch # User anatofuz # Date 1588815422 -32400 # Node ID b0757b4dbbe4cc8feb924f84a0c9b428e3db6ef0 # Parent 4c753956a272e9495a6cc07d1258a427bb8b02a1 ... diff -r 4c753956a272 -r b0757b4dbbe4 paper/anatofuz-sigos.md --- 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 diff -r 4c753956a272 -r b0757b4dbbe4 paper/anatofuz-sigos.pdf Binary file paper/anatofuz-sigos.pdf has changed diff -r 4c753956a272 -r b0757b4dbbe4 paper/anatofuz-sigos.tex --- 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}