# xv6の構成要素の継続の分析

# 研究目的

• OS自体そのものは高い信頼性が求められるが、 OSを構成するすべての処理をテストするのは困難である。
• テストを利用する以外の手法で信頼性を高めたい。
• OSの状態を状態遷移を基本としたモデルに変換し形式手法を用いて信頼性を高める手法を検討する
• 小さなunixであるxv6 kernelを、状態遷移を基本とした単位でのプログラミングに適したCbCで再実装を行っている
• このためには現状のxv6kernelの処理の状態遷移の分析が必要である。
  • その結果を、 継続ベースでのプログラミングに変換していく必要がある。
• xv6kernelの構成要素の一部に着目し、状態遷移系の分析と状態遷移系を元に継続ベースでxv6の再実装を行う。

# やったこと

• 使っているキーボードが壊れて落ち込む
• sigosのmindmap作成と論文の書き始め
• リモートTA
• 雑誌に投稿するPerlの記事を書く作業
  • なんか出版社の人もコロナ騒ぎで大変らしい
• macOSでのCbCgccのビルド
• 自宅のネットワークが強化された

# Gears関連

• xv6とGearsで共通して使っているGearsToolsをいい感じに統一したい
  • いろいろなPerlスクリプトをcmakeで動かしてたり、手で動かしたりしている
  • ところどころPerlのライブラリとして実装しているので、無理なことはないが…
  • 誰かと一緒にやる or 誰かにやってもらえると良さそう

# sigos

• mindmapはとりあえず書きながら作業しています
• 序章とかは多分書けるので、論文も書きながらネタを考えています
• 文章校正にtexlint使いたいが、 LaTeXだとうまく動かないので一度markdownにするのがいいかもしれない
  • あとでsigos用のテンプレートリポジトリ作っておきたい気もする

# 必要となってきそうな要素

• プロセスの状態を持つcontext

  • 現在の実装ではプロセス構造体にcbc_contextを埋め込んでいる
  • プロセス構造体 -> contextに完全に切り替えるのを考えると、「どこまでがプロセスが持つ情報/状態」かというのが重要そう

• kernelの状態を持つcotnext

  • 今まで実装していた中で必要だったのは、割り込みが来ているかどうかのフラグ、ファイルシステム内のinodeのキャッシュなど
  • inodeのキャッシュそのものをcontext化するのも良さそうだが、特別CodeGearがついてくる必要はなさそう
    • その場合はオブジェクト指向OSっぽい実装になりそうだけど、そういうわけではなさそう

• 論文出すまでにどこまで実装するかみたいなところ

  • ファイルシステムの実装を変えていくのがいいかもしれない

# GCCのビルド

• mac環境だといろいろと大変なところがあるが、最新のGCC9だとわりとスムーズにビルドができるらしい
• CbCGCCも9にアップデート済みだった

# macOSでのビルド

• このサイトの通りにやればだいたいできる
• catalina(high sierraくらい?)からgmpなどのライブラリを個別でビルドしなければGCCのビルドができなかった
  • gcc9からGCCのリポジトリに自動でこのあたりのライブラリをインストールするcontrib/download_prerequisitesが追加されていて便利になっていた

1
2

$contrib/download_prerequisites 
(GCCのトップディレクトリで行わないといけない)

• /usr/include/が抜けた問題があるので、sys_rootを自前で用意する必要がある
  • 一部のincludeファイルにmacOSのパッチを与える必要があるらしい(必要ないかも)

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

$cd sys_root
$ln -s /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/Library .
$ln -s /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/System .
$mkdir usr && cd usr
$ln -s /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/bin .
$ln -s /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/lib .
$ln -s /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/libexec .
$ln -s /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/share .
$cp -r /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include include
$vim include/Availability.h

• あとはConfigureを実行する
  • --with-sysrootを指定しておかないと、/usr/includeが無いエラーが発生する
  • --with-sysrootは絶対パスで与えないといけない

1

../CbC_gcc/configure --prefix=$PWD --disable-nls --disable-bootstrap --enable-checking=tree,rtl,assert,types CFLAGS="-g3 -O0" --enable-languages=c,lto --no-create --no-recursion  --disable-multilib --with-sysroot=/Users/anatofuz/workspace/cr/CbC/latest_gcc/sys_root

• ここで何故かMafikefileでなくconfig.statusなシェルスクリプトが生成される
  • このシェルスクリプトを実行するとMakefileが生成される
  • あとは make -jすれば良い(-jだと一部がうまく動かないので、makeの方が良いかもしれない)

# TODO

• ARM版GCCのビルド
  • linux(dalmore), macOSともに成功していないので…
  • xv6関連で使いたい

# 家のインターネット

• レキオス光レジデンスからレキオス光 スマートウェイに
• あまり人が使っていない説があるが、100Mbosくらい出るようになり安心