# 研究目的
- アプリケーションの信頼性を保証するには土台となるOSの信頼性を高く保証する必要がある
- しかしOSの機能をテストですべて検証するのは不可能である。
- 定理証明やモデル検査を利用して、テストに頼らずに保証したい
- 証明しやすい形、かつ実際に動くソースコードが必要
- 継続ベースの状態遷移系で再実装することで表現しやすくしたい
- プログラムは二つの計算に分離される
- プログラムは入力と出力の関係を決める計算(ノーマルレベル)
- その計算に必要なメタな計算(メタレベル)
- プログラムの信頼性の保証を動作しつつ行うには、メタレベルの計算を活用したい
- そのためにはメタレベルの計算を柔軟に扱うAPIや実装方法が必要
- 本研究ではノーマル/メタレベルでの実装に適した、継続を基本とする言語Continuation Based Cを用いて、OSの実装を行い、メタ計算APIについて考察する。
# 今週
- 奨学金の免除申請の書類が来たので作文をすることに
- 業績系いろいろ書かないと…
- 指導教員の推薦の作文がありますがどうしましょう…
- 知り合いのエンジニアが沖縄に来てたので飲みに行っていた
- アシャリフ先生のpukiwiki置換
- ひたすらperlを書いてeuc-jpにキレる世界観
- RustのFileWriteを書いた
- Rakuのenv系のビルドツールにプルリクを送ったけれど無視されて辛い
# CbC関連
- B3の松岡くんと作業した
- ArmなCbC GCCのdependendsで指定していた
arm-none-eabi-gcc
が古いらしい
|
|
# Raku関係
Rakudo-Star(rakuの季節ごとにでる詰め合わせパック)のビルドツールがConfigure.pl
からrstar
に変更になっていた。
- MoarVM, NQP, Rakuのそれぞれでは
Configure.pl
が使われているらしい rstar
はbash script
気づいたらv2020.10
に…
|
|