Papers/2020/anatofuz-sigos: paper/anatofuz-sigos.tex comparison

comparison paper/anatofuz-sigos.tex @ 44:698ba8f724d3

update

author	anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date	Thu, 07 May 2020 11:05:55 +0900
parents	b0757b4dbbe4
children	4cecdfd6b237

comparison

equal deleted inserted replaced

-:b0757b4dbbe4
+:698ba8f724d3
 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の完全な再実装や、 実装を利用したxv6の証明は行っていないので今後は証明を行いたい。
+現状はまだxv6の実装を利用した証明は行っていない。
+今後はモデル検査などを行い、 OSの信頼性を向上させていきたい。
 それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。
 またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。
 \nocite{*}
 \bibliographystyle{ipsjunsrt}
 \bibliography{anatofuz-bib}

Mercurial > hg > Papers > 2020 > anatofuz-sigos

comparison paper/anatofuz-sigos.tex @ 44:698ba8f724d3