# HG changeset patch
# User autobackup
# Date 1616512203 -32400
# Node ID fae0d5b27a2dce21567757ca889f2874e076d18d
# Parent  a51e6bab65e8c4648432fe48b25209c5afe16231
backup 2021-03-24

diff -r a51e6bab65e8 -r fae0d5b27a2d user/matac42/note/2021/03/23.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/note/2021/03/23.md	Wed Mar 24 00:10:03 2021 +0900
@@ -0,0 +1,9 @@
+# 研究目的
+
+なかなか思い浮かばない
+
+ファイルシステムにおいてディレクトリはトランザクションを持っているが、個々のファイルに関しては無い。
+
+その理由として、トランザクションは重たい処理であることが挙げられるが、コンピュータのスペックは向上を続けているため個々のファイルにトランザクションを実装し運用することが可能になりつつ有る。
+
+GearsOSに関して、個々のファイルに関しても整合性を保つためにトランザクション処理を取り入れたい。
\ No newline at end of file
diff -r a51e6bab65e8 -r fae0d5b27a2d user/pine/メモ/2021/03/23.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/pine/メモ/2021/03/23.md	Wed Mar 24 00:10:03 2021 +0900
@@ -0,0 +1,13 @@
+# 研究目的
+
+- 本研究室では、Continuation Based C(CbC)を用いて、信頼性と拡張性を両立するOSであるGearsOSを開発している。
+
+- 円滑なOS開発を行うために、GearsOSのデバッガを作成する。
+
+## やったこと
+- 今週は何もやってないです。。。
+
+
+## やること
+- 先輩のGearsの論文を見る
+- 例題を書いてみる
diff -r a51e6bab65e8 -r fae0d5b27a2d user/soto/log/untitled.md
--- a/user/soto/log/untitled.md	Wed Mar 17 00:10:03 2021 +0900
+++ b/user/soto/log/untitled.md	Wed Mar 24 00:10:03 2021 +0900
@@ -1,31 +1,35 @@
 # 研究目的
+- 
+
+# 今週やった事
+- kono先生とCbCからset jumpを消そうとしていました
 
-- OSやアプリケーションの信頼性を高めることは重要な課題である。
+## set jmpを消す
+現在のCbCには、set jumpが使われている部分がある。
+これを消したい。
 
-- 研究室でCbCという言語を開発している。その信頼性を証明したい。
-    - CbCとは、Cからループ制御構造とサブルーチンコールを取り除き、継続を導入したCの下位言語である。継続呼び出しは引数付き goto 文で表現される。
+型が`jmp_buf`であるものを`int`64個の配列で受け取れるようにする。
 
-- cbcはサブルーチンとループ制御をcから取り除いている。その為、それを実装した際のプログラムを検証をする必要がある。
+` innerRes = CreateDeclStmt(bufII, false, false, DeclSpec::TST_typename, CreateIdentifierInfo("jmp_buf", Loc));`を  
+`innerRes = CreateDeclStmt(bufII, false, false, 64, DeclSpec::TST_typename, CreateIdentifierInfo("int", Loc));`
+で  
+できるようにする
+
+`StmtResult Parser::CreateDeclStmt(IdentifierInfo *II, bool isRetCS, bool copyType, DeclSpec::TST valueType, IdentifierInfo* Name, DeclSpec::TQ TQ){`を  
+`StmtResult Parser::CreateDeclStmt(IdentifierInfo *II, bool isRetCS, bool copyType, int array, DeclSpec::TST valueType, IdentifierInfo* Name, DeclSpec::TQ TQ){`
+これにする。arrayが追加されただけ
 
-- プログラムの検証手法のひとつに、Hoare Logic がある。
-    - これを説明すると、「プログラムの事前条件(P)が成立しているとき、コマンド(C)実行して停止すると事後条件(Q)が成り立つ」というものである。
+そして`CreateDeclStmt()`に以下を追加。
+```CbC
+  if (array) {
+    DeclSpec FDS(AttrFactory);
+    D.AddTypeInfo(DeclaratorChunk::getArray(0,false,false,Actions.ActOnIntegerConstant(Loc,array).get(),Loc, FDS.getConstSpecLoc() ),
+            std::move(FDS.getAttributes()), SourceLocation());
+  }
+```
 
-    - つまり、関数が任意の値が引数として実行された際に、任意の値が帰ってきた場合を「関数は正常に実行される」といえる。
-
-    - CbC では実行を継続するため、ある関数の実行結果は事後条件になるが、その実行結果が遷移する次の関数の事前条件になる。それを繋げていくため、個々の関数の正当性を証明することと接続の健全性について証明するだけでプログラム全体の検証を行うことができる。
+`AddTypeInfo`を直接書いて解決させよう
 
 
-- cbcの実行を継続するという性質に Hoare Logicを連続して用いると、個々の関数の正当性の証明と接続の健全性について証明する事でプログラム全体の検証を行う事ができる。
-
-- これらのことから、Hoare Logicを用いてCbCを検証する。
-
-
-- 先行研究ではCbCにおけるWhileLoopの検証を行なった。
-
-- agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である赤黒木の検証を行う
-
-# 今週やった事
-- スライドの作成
-
-## 余談
--　明日が入試当日
+# 余談
+-　卒業式でした