Mercurial > hg > Papers > 2020 > anatofuz-sigos

changeset 44:698ba8f724d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
update
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 07 May 2020 11:05:55 +0900
parents b0757b4dbbe4
children 4cecdfd6b237
files paper/anatofuz-sigos.md paper/anatofuz-sigos.pdf paper/anatofuz-sigos.tex
diffstat 3 files changed, 30 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/paper/anatofuz-sigos.md	Thu May 07 10:37:02 2020 +0900
+++ b/paper/anatofuz-sigos.md	Thu May 07 11:05:55 2020 +0900
@@ -304,9 +304,22 @@
 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の完全な再実装や、 実装を利用したxv6の証明は行っていないので今後は証明を行いたい。
+現状はまだxv6の実装を利用した証明は行っていない。
+今後はモデル検査などを行い、 OSの信頼性を向上させていきたい。
 それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。
-またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。
\ No newline at end of file
+またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。
+
Binary file paper/anatofuz-sigos.pdf has changed
--- a/paper/anatofuz-sigos.tex	Thu May 07 10:37:02 2020 +0900
+++ b/paper/anatofuz-sigos.tex	Thu May 07 11:05:55 2020 +0900
@@ -410,12 +410,26 @@
 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の完全な再実装や、 実装を利用したxv6の証明は行っていないので今後は証明を行いたい。
+現状はまだxv6の実装を利用した証明は行っていない。
+今後はモデル検査などを行い、 OSの信頼性を向上させていきたい。
 それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。
 またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。
+
+
 \nocite{*}
 \bibliographystyle{ipsjunsrt}
 \bibliography{anatofuz-bib}