# 研究目的

アプリケーションの信頼性を保証するために、アプリケーションが動作するOSの信頼性を高める必要がある。

本研究室では、信頼性に重きを置いたGearsOSを開発している。
信頼性とは

- どのユーザーがどのようなファイル操作をしたかわかること
- logが残ること
- item 操作の辻褄があっていること

を指す。

GearsOSはノーマルレベル、メタレベルの処理を切り分けることができるCbC(Continuation Based C)で記述されている。

GearsOSにはAgdaで記述された、GearsAgdaがある。
GearsAgdaはOSの信頼性を検証するために作成された。
しかしながら、Agdaはcontinuationでなく、速度も遅い。
よって、信頼性が検証されたGearsAgdaをCbCに変換する必要がある。

また、GearsOSには現在未実装の機能があり、その一つにファイルシステムが挙げられる。信頼性を確保するため、ファイルシステムは

- ファイルシステム全体のトランザクション化
- ファイルシステム全体のバックアップ\&ロギング

を取り入れたい。

本卒業研究では、GearsAgdaのCbCへの変換後、ファイルシステムの実装を目指す。

# シス管

- 土日はnal研のブログサルベージをzoom繋ぎながらやっていた
- 新しく入ってきた人たちがpsonoにユーザー登録できなくて不便なので、この後なおしたい
- 少しずつタスク割り振りもできるようにしていきたい
- シス管ミーティングは毎週月金(14:40~)

# その他

- LANケーブル自作むずい
    - try: 3, failed: 3
- raspberry pi
    - 家にあるipod touch 繋いでなんかできるかな
        - カメラで動作検出
        - ディスプレイとして
- 研究室にあるLogitecのUSB LANアダプターはドライバーがなんかうまく動かない
    - 多分自分の環境が悪い
- 有線接続に切り替えたい
    - wifi接続めちゃくちゃ切れる
    - 自分の席はそもそも電波が届き切ってなさそう
- AtcoderのC問題がなかなか突破できない
    - まだ10回やってないからこれからに期待