annotate user/itsuki/2021/6-22.md @ 121:6138bdc8f9dc

backup 2023-05-11
author autobackup
date Thu, 11 May 2023 00:10:04 +0900
parents c14b8395b5ed
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
73
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
1 # 進捗報告
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
2 ## 研究目的
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
3 - 当研究室ではOSの信頼性の検証に重きを置いた、GearsOSを開発している。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
4 - GearsOSはノーマルレベルとメタレベルを分離して記述が行えるCの拡張言語CbC(Continuation based C)で構成されている。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
5 - GearsOSは現在開発途上であり、OSとして実際に機能するために開発しなくてはならない機能が残っている。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
6 - 未実装の機能の一つとしてファイルシステムが挙げられる。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
7 - 当研究室では、CbCとは異なるGearという概念を用いて分散処理を記述することができる分散フレームワークChristieを開発している。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
8 - GearsOSのファイルシステムをChristieと同様の仕組みを用いて実装したい。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
9 - そのためにjavaで構成されているChristieをCbCで構成し直していく。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
10
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
11 > - コンピュータの核となるOSには高い信頼性に加え、拡張性が必要となる。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
12 > - OSの信頼性を検証するために定理支援証明(agda)やモデル検査を利用したい。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
13 > - プログラムの整合性を検査をメタレベルの計算で行いたい。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
14 > - そのためにはノーマルレベルとメタレベルを分離した記述が行える仕組みが必要である。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
15 > - 当研究室ではノーマルとメタレベルを分離して記述が行えるCの拡張言語CbCを開発している。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
16
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
17
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
18 ## 進捗内容
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
19 - またゆーくんとGearsの基本操作の確認してました。
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
20 - 自分も結構忘れてたので思い出しつつ、論文読みつつ
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
21 - とりあえずHelloWorldを書いてみた
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
22 - いずれhgから消す予定
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
23 - 木曜の18時と土曜朝9時にzoomで一緒にやるように
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
24 - 次回はwcあたりを記述していきたい
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
25 - もう少しHelloWorldをこねてみてもいいかも
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
26
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
27 - 筆記で落ちたと思ってた企業が面接に進んだ
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
28 - 一次面接がだいぶ先なので他にもエントリーする予定
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
29 -
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
30
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
31 ## 雑談
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
32 - 自宅のエアコンが壊れた
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
33 - 室外機がぼろくなってガス管を傷つけたのが原因
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
34 - 買い替えが決定
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
35 - 費用は大家さんもちなので助かった
c14b8395b5ed backup 2021-06-23
autobackup
parents:
diff changeset
36 - 「業者は今忙しいからだいぶ先になるよ」と死亡宣告された