Mercurial > hg > Papers > 2020 > anatofuz-sigos

comparison paper/anatofuz-sigos.tex @ 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
comparison
equal deleted inserted replaced
42:4c753956a272 43:b0757b4dbbe4
356 APIの内部のCodeGearはあくまでBasic Block単位に基づいているために、 状態遷移図で表現した際に自然言語で表現できないCodeGearも存在してしまう。 356 APIの内部のCodeGearはあくまでBasic Block単位に基づいているために、 状態遷移図で表現した際に自然言語で表現できないCodeGearも存在してしまう。
357 357
358 さらに、 \texttt{for}ループをCodeGearに分割することを考えるとループ中にループのindexを利用している場合は、 そのindexも次の継続に渡さなければならない。 358 さらに、 \texttt{for}ループをCodeGearに分割することを考えるとループ中にループのindexを利用している場合は、 そのindexも次の継続に渡さなければならない。
359 このためindexを使用していないCodeGearでも継続の引数としてindexを受け取り、 実際にindexを利用するCodeGearに伝搬させる必要がある。 359 このためindexを使用していないCodeGearでも継続の引数としてindexを受け取り、 実際にindexを利用するCodeGearに伝搬させる必要がある。
360 これらの問題を解決する為には、 APIを分割したCodeGearそれぞれのDataGearに型を与え、 どの継続でDataGearの意味が変わるかを追求する必要がある。 360 これらの問題を解決する為には、 APIを分割したCodeGearそれぞれのDataGearに型を与え、 どの継続でDataGearの意味が変わるかを追求する必要がある。
361 APIを分割して作成したCodeGearのDataGearは、 現在各APIに対応した一つの巨大な構造体に隠蔽されている。 361 APIを分割して作成したCodeGearのDataGearは、 現在各APIに対応した1つの巨大な構造体に隠蔽されている。
362 巨大な構造体で管理するのではなく、 構造体で次のCodeGearの状態に影響を与える要素を適宜組み合わせたDataGearを作る必要がある。 362 巨大な構造体で管理するのではなく、 構造体で次のCodeGearの状態に影響を与える要素を適宜組み合わせたDataGearを作る必要がある。
363 363
364 364
365 \section{CbCを用いた部分的なxv6の書き換え} 365 \section{CbCを用いた部分的なxv6の書き換え}
366 366
390 390
391 cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size); 391 cbc_init_vmm_dummy(&p->cbc_context, p, p->pgdir, _binary_initcode_start, (int)_binary_initcode_size);
392 392
393 p->sz = PTE_SZ; 393 p->sz = PTE_SZ;
394 memset(p->tf, 0, sizeof(*p->tf)); 394 memset(p->tf, 0, sizeof(*p->tf));
395 \end{lstlisting} 395 // omission
396 }
397 \end{lstlisting}
398
399 Code\ref{src:dumy_function_cbc}中で、 CodeGearへの遷移が行われる\texttt{goto vm->init\_vmm()}の\texttt{vm->void\_ret}は\texttt{init\_vmm}の次の継続のCodeGear名である。
400 この\texttt{vm->void\_ret}は\texttt{return}するのみのCodeGearであり、 void型関数と組み合わせることで呼び出し元へと復帰する事が可能となる。
396 401
397 402
398 \section{xv6の今後の再実装} 403 \section{xv6の今後の再実装}
399 404
400 xv6ではカーネルパニックの発生時や、 inodeのキャッシュなどをグローバル変数として利用している。 405 xv6ではカーネルパニックの発生時や、 inodeのキャッシュなどをグローバル変数として利用している。
401 グローバル変数を使用してしまうと、 CodeGearで定義した状態がDataGear以外のグローバル変数によって変更されてしまう。 406 グローバル変数を使用してしまうと、 CodeGearで定義した状態がDataGear以外のグローバル変数によって変更されてしまう。
402 グローバル変数を極力使わず継続を中心とした実装を行いたい。 407 グローバル変数を極力使わず継続を中心とした実装を行いたい。
403 408
404 contextは現在プロセス構造体に埋め込まれており、 kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。 409 contextは現在プロセス構造体に埋め込まれており、 kernelそのものの状態を制御するためには各contextを管理する機能が必要であると考えられる。
405 410 contextを管理する方法として、 各context間でメッセージなどをやりとりする方法や、 cotnextを主軸にして割り込みなどの処理を再検討するものがある。
411 他にはkernelそのもののcontextを定義し、 kernel全体の状態とプロセスの状態をそれぞれ別のcotnextで処理をするというのも検討している。
412
413 \section{まとめ}
414
415 本稿ではxv6を継続を用いた単位での再実装を検討し、 実際にいくつかの処理を再実装した。
416 現状はまだxv6の完全な再実装や、 実装を利用したxv6の証明は行っていないので今後は証明を行いたい。
417 それに伴って、 xv6自体にモデル検査機能の組み込みなども行っていく。
418 またAgdaなどの定理証明支援系で証明された処理から、 CbCのCodeGearに変換する処理系の実装なども検討する。
406 \nocite{*} 419 \nocite{*}
407 \bibliographystyle{ipsjunsrt} 420 \bibliographystyle{ipsjunsrt}
408 \bibliography{anatofuz-bib} 421 \bibliography{anatofuz-bib}
409 422
410 423