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

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


## 進捗内容
- Christieをまたゆーくんと読み直していました。
- 当初はTopologyManagerを読み直していた。
    - 動的で作れるTopologyがTree型しかなかった
    - いずれは別の形も動的で作れるようにしたい
- Christieのもっと根幹的な部分を先に読むことに
- DGM部分とputやTakeがどのように書かれているかを確認
    - TreeMapがDGM、DGMにキューとkeyをペアにして書き込んでいる
        - DGMにはDGを格納しておくキューとkeyがペアで書き込んである
    - DGM(dataGears)にkeyが既にあった場合などの処理も記述してある。
- 他にも分かったところいろいろ
- そろそろGearsのAPIを書き始める
```
    protected TreeMap<String, LinkedBlockingQueue<DataGear>> dataGears = new TreeMap<String, LinkedBlockingQueue<DataGear>>();

    public synchronized void put(String key, DataGear dg){
        if (dataGears.containsKey(key)) {
            dataGears.get(key).add(dg);
        } else {
            LinkedBlockingQueue<DataGear> queue = new LinkedBlockingQueue<DataGear>();
            queue.add(dg);
            dataGears.put(key, queue);
        }
    }

    public Object take(String key){
        Object data = dataGears.get(key).poll().getData();

        if (dataGears.get(key).isEmpty()) {
            dataGears.remove(key);
        }

        return data;
    }
```

- 明日1次面接してきます。
    - 他にもいろいろ企業説明会を予約。
    - 難易度を少し下げたところも一つ投げてみた。
    - 8月終わるまでに内定もらうのが目標

## 雑談
- エアコン取り替えてもらいました
    - 内部クリーン機能付き、すごい