Mercurial > hg > Document > Growi

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/software/hg/hgweb-fix.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,18 @@
+日付が one month ago とかでるのが不快なので日付になおす
+
+```
+*** /usr/local/Cellar/mercurial/5.6.1/lib/python3.9/site-packages/mercurial/templates/static/mercurial.js       Mon Dec 14 17:25:07 2020
+--- /usr/local/Cellar/mercurial/5.6.1/lib/python3.9/site-packages/mercurial/templates/static/mercurial.js.orig  Mon Dec 14 17:23:04 2020
+***************
+*** 293,301 ****
+                                return "in the distant future";
+                        }
+                }
+-                 if (delta > (scales.day)){
+-              　　　 return shortDate(once);
+-             　　}
+
+                if (delta > (2 * scales.year)){
+                        return shortdate(once);
+--- 293,298 ----
+```
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/Okud/DeviceDriver/2020/12/08.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,21 @@
+# Gears OS Device Driver 作成
+## 研究理由
+- OSには信頼性の保証が求められている。
+- 当研究室では、継続を基本とする言語Continuation Based Cを用いて、OSの実装を行っている。
+- Gears OSをRaspberry Piに搭載することができれば、他のハードウェアにも載せることができる。
+- Gears OSを載せたRaspberry Piはシリアル通信を用いて他のハードから入力しなければならない。
+- 直接キーボードをつないで入力できれば便利になる。
+- そこで、Gears OSのDevice Driverを作成する。
+
+## 進捗
+- シリアル通信をしたときのmacの文字化けを直した
+        - ケーブルを新調した(amazonで379円)
+        - 参考にしたサイト(https://qiita.com/tmishina/items/612d7d1a7d76364a9e45)
+- MKにxv6のmakeの仕方を教わり、環境をもらった。
+
+## Todo
+- xv6をUEFIからbootする。
+        - bootできるxv6をarm仕様にする
+        - arm仕様のxv6をbootできる様にする
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/anatofuz/note/2020/12/014.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,1 @@
+#test
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/anatofuz/note/2020/12/08.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,93 @@
+# 研究目的
+- アプリケーションの信頼性を保証するには土台となるOSの信頼性を高く保証する必要がある
+    - しかしOSの機能をテストですべて検証するのは不可能である。
+- 定理証明やモデル検査を利用して、テストに頼らずに保証したい
+    - 証明しやすい形、かつ実際に動くソースコードが必要
+    - 継続ベースの状態遷移系で再実装することで表現しやすくしたい
+- プログラムは二つの計算に分離される
+    - プログラムは入力と出力の関係を決める計算(ノーマルレベル)
+    - その計算に必要なメタな計算(メタレベル)
+- プログラムの信頼性の保証を動作しつつ行うには、メタレベルの計算を活用したい
+- そのためにはメタレベルの計算を柔軟に扱うAPIや実装方法が必要
+- 本研究ではノーマル/メタレベルでの実装に適した、継続を基本とする言語Continuation Based Cを用いて、OSの実装を行い、メタ計算APIについて考察する。
+
+
+# 最近
+- growiをCLIで編集できるツール書いていました
+- シス管関係
+- Interfaceの実装を考えている
+- 修論のmindmapを書き始めました
+
+# Interfaceの複数実装
+- Haskellの例題見ながら雰囲気を考えている
+    - どのIntefaceが使われているかは型ごとにenumを作成したい
+
+```c
+/*
+data Point = Pt Double
+
+instance Eq Point where
+  (Pt x) == (Pt x') = x == x'
+
+instance Ord Point where
+  compare (Pt x) (Pt x')
+    | x == x'   = EQ
+    | x < x'    = LT
+    | otherwise = GT
+
+main = do print $ (Pt 1) == (Pt 2)  -- 出力: False
+          print $ (Pt 1) >= (Pt 2)  -- 出力: False
+          print $ (Pt 1) <= (Pt 2)  -- 出力: True
+*/
+
+typedef struct Rectangle {
+  int l;
+  int w;
+}
+
+
+typedef struct Ord {
+  __code equal(Impl* eq, Impl* other, __code ok(...), __code none(...));
+  __code lt(Impl* eq, Impl* other, __code ok(...), __code none(...));
+  __code pt(Impl* eq, Impl* other, __code ok(...), __code none(...));
+}
+
+impl Ord typedef struct Rectangle {
+
+  __code rectangleual(Impl* rectangle, Impl* other, __code ok(...), __code none(...)) {
+    goto rectangle->eq(other, ok, none, ...);
+  }
+
+  __code lt(Impl* rectangle, Impl* other, __code ok(...), __code none(...)) {
+    if (rectangle.x > other.x) {
+      goto ok(...);
+    }
+    goto none(...);
+  }
+
+}
+
+typedef enum PointTypeManager {
+  Point-Ord,
+  Point-Equal
+}
+```
+
+# Option
+
+Rustに影響されているのでMaybeみたいなやつがほしい気がする
+
+```c
+typedef struct Option <Type, Impl> {
+  __code some(Impl* option, union Data* data, __code next(...));
+  __code none(Impl* option, __code next(...));
+  __code is_ok(Impl* option, __code ok(union Data* data, ...), __code none(...));
+} Option;
+```
+
+- 意外とかけそうなので例題書いてみるか...
+    - 1 Interfaceが複数のImplを持つ例題を書くかみたいな気持ち
+    - 今のInterfaceにImplをもたせる方針をやめるか、中でシンボルテーブルみたいなのを持ちたい気がする
+        - いやそれがcontextではあるのだけれど...
+- .....と思いきやgotoすればいいという感じだったので却下
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/anatofuz/note/2020/12/10.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,1 @@
+# 2020/12/10
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/anatofuz/note/2020/12/14.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,1 @@
+# hello
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/anatofuz/note/2020/12/15.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,1 @@
+# aaa
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/anatofuz/note/2020/12/16.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,3 @@
+# 2020/12/16
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/ikkun/memo/2020/12/08.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,25 @@
+# GearsOSにおけるモデル検査
+
+# 研究目的
+* 一般的にアプリケーションはテストと言われる方法を用いてバグを発見し修正することで信頼性を高める、しかしバグの再現性が低い場合には発見は困難になる。この際にはデバックを行うプログラマーの経験による予測が必要であり、予想した原因に基づいて１つ１つチェックをしていく必要がある。
+* モデル検査とは、検証したいアプリケーションの状態遷移記述を用いて行われ、特定の状態から遷移する全ての組み合わせに対して検査を行うことで、信頼性を保証する。
+* 当研究室で開発しているGearsOSはアプリケーションやサービスの信頼性をOSの機能として保証することを目指しており、モデル検査による検証や、定理証明を用いる事での信頼性へのアプローチを行っています。
+* 本研究ではGearsOSにおけるDPPのモデル検査を行うことでGearsOSにおけるモデル検査手法の確立と、さらにGearsOS上での自身のモデル検査について研究する。
+
+# 実装の全体像
+* モデル検査を行うための例題としてのDPPを扱う。DPPは並列で動きつつ、スレッド間でデータのやり取りを行う。このためデッドロックが起こる。今回の研究ではこのデッドロックをモデル検査で検出する。
+* スレッド間でのデータのやり取りはCASを用いているSynchronizedQueueでデータの保証を行う。
+* モデル検査を行うために、DPPを動かしつつstatmantDBとmemoryTreeによってログを保存する。
+
+# 目次構成
+
+* 序論(研究目的、背景）
+* モデル検査によるアプローチ（他のモデル検査ツール、CｂCと検証、）
+* GearsOSによるモデル検査手法（DPP、タブロー展開、）
+* GearsOS上での実装（pargoto、synchronizedqueue、cpuworker、statmantDB、memoryTree
+- pargoto でのphilsの起動
+- cpuworkerをSynchronizedqueueのCaS優先に
+- 状態を保存するstatmantDB、memoryTree
+-
+* 評価
+* 結論
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/ikkun/memo/2020/12/15.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,1 @@
+# /user/ikkun/memo/2020/12/15
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/jogo/note.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,1 @@
+ゼミの記事
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/jogo/note/2020/12/15.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,1 @@
+#
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/jogo/note/2020/12/22.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,1 @@
+テスト
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/note/2020/12/14.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,21 @@
+# 今日やったこと
+* toeic対策
+    * センテンスとreading
+* enpitのデモ練
+    * 撮った写真をwebサイトに反映させた．
+* macbookの充電器を買いたかった...
+    * エディオンに無かった．
+* 406のプリンターにIPアドレスを振って，使えるようにした．
+    * VLANのイメージを掴めた．
+* gcdsの設定をx windowを利用してubuntu上でできるか試した．
+    * できなかった．
+    * windowsでやることにする．
+# 明日は
+* gcdsの設定
+    * 同期内容を確定したい．
+    * windowsを借りたい．
+* toeic対策
+    * part別攻略を終わらせて，次から模試に入れるようにしたい．
+* enpitデモ
+* ゼミ
+* キッチンカーが琉大に来るらしいので見にいこうと思う．
\ No newline at end of file
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/matac42/note/2020/12/15.md	Wed Dec 16 15:04:03 2020 +0900
@@ -0,0 +1,9 @@
+# 今日やったこと
+* toeic対策
+    * part別攻略が一旦終わった．
+* enpit
+    * 頂いた写真を追加した．
+
+# 明日は
+* toeic対策
+    * 模試をやりたい．
\ No newline at end of file