view user/itsuki/2021/6-15.md @ 72:1986100619b2

backup 2021-06-16
author autobackup
date Wed, 16 Jun 2021 00:10:04 +0900
parents
children
line wrap: on
line source

# 進捗報告 
## 研究目的
- 当研究室ではOSの信頼性の検証に重きを置いた、GearsOSを開発している。
    - GearsOSはノーマルレベルとメタレベルを分離して記述が行えるCの拡張言語CbC(Continuation based C)で構成されている。
- GearsOSは現在開発途上であり、OSとして実際に機能するために開発しなくてはならない機能が残っている。
- 未実装の機能の一つとしてファイルシステムが挙げられる。
    - 当研究室では、CbCとは異なるGearという概念を用いて分散処理を記述することができる分散フレームワークChristieを開発している。
    - GearsOSのファイルシステムをChristieと同様の仕組みを用いて実装したい。
    - そのためにjavaで構成されているChristieをCbCで構成し直していく。 

> - コンピュータの核となるOSには高い信頼性に加え、拡張性が必要となる。
>     - OSの信頼性を検証するために定理支援証明(agda)やモデル検査を利用したい。
>     - プログラムの整合性を検査をメタレベルの計算で行いたい。
>     - そのためにはノーマルレベルとメタレベルを分離した記述が行える仕組みが必要である。
> - 当研究室ではノーマルとメタレベルを分離して記述が行えるCの拡張言語CbCを開発している。


## 進捗内容
- 内定は相変わらずでてない。
    - 筆記で一社転んだので再勉強してました
    - SPI問題集では拾えてない問題で死亡
        - 嘘つき問題、多面体の頂点

- GearsOSをそろそろ進めようと
    - OS研究会の時に書いたwcを動くようにする?
    - 論文を読みながら

## その他の報告
- リングフィット買いました。
    - 鬱気味なのが治ったりなんだり。