# HG changeset patch
# User tobaru
# Date 1526381221 -32400
# Node ID 60405cc47b3a451d860fbaca695373f6f743dd1d
# Parent e6422d20c0f2ca6df60b104da9e802bd4610bb2c
chapter1
diff -r e6422d20c0f2 -r 60405cc47b3a Slide/prosym.html
--- a/Slide/prosym.html Tue May 15 18:31:03 2018 +0900
+++ b/Slide/prosym.html Tue May 15 19:47:01 2018 +0900
@@ -86,7 +86,7 @@
@@ -127,12 +127,69 @@
-
スライドの流れ
+
メタ計算
+
+ - ノーマルレベルの計算
+
+ - コンピュータの計算はプログラミング言語で計算される。
+ - その部分をノーマルレベルの計算と呼ぶ。
+
+
+ - メタレベルの計算
+
+ - コードが実行される際の以下の部分が、メタレベルの計算という。
+
+ - 処理系の詳細や使用する資源
+ - コードの仕様や型などの言語以外の部分
+
+
+
+
+
+
+
+
+
+
+
CbC
+
+ - ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC(Continuation based C) を用いる。
+ - CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。
+ - CbC は関数呼び出し時の暗黙の環境を使わずに、コードの単位を行き来できる引数付き goto 文を持つ C と互換性のある言語である。
+ - CbC を用いてCode Gear と Data Gear、メタ構造を導入する。
+
+
+
+
+
+
+
Gears OS
+
+ - CbC を用いて導入したCode Gear、Data Gear、メタ構造を用いて、検証された Gears OS を構築したい。
+ - 検証には 定理証明支援系である Agda を用いる。
+ - Gears の記述をモジュール化するために Interface を導入した。
+ - さらに並列処理の記述ように par goto 構文を導入する。
+
+
+
+
+
+
+
par goto の実行
+
+ - 本論文では Interface と par goto の実装を記述し、評価を行なった。
+ - また、マルチ CPU と GPU 上での par goto 文の実行を確認した。
+
+
+
+
+
+
+
スライドの流れ
-
- CbC
+ Gears OS におけるメタ計算
- - GearsOS
- Interface
- Context
- Gears OS の並列処理
@@ -146,16 +203,13 @@
-
CbC
+Gears OS におけるメタ計算
-
Gears OS
-
+
Gaears OS の構成
@@ -173,7 +227,7 @@
-
Gears OS の並列処理
+Gears OS の並列処理
@@ -185,19 +239,19 @@
-
並列構文
+並列構文
-
比較
+比較
-
今後の課題
+今後の課題
diff -r e6422d20c0f2 -r 60405cc47b3a Slide/prosym.md
--- a/Slide/prosym.md Tue May 15 18:31:03 2018 +0900
+++ b/Slide/prosym.md Tue May 15 19:47:01 2018 +0900
@@ -19,9 +19,33 @@
- 本研究室では、OS の信頼性の保証と拡張性を実現することを目標に Gears OS を設計中である。
- par gotoかAPIの説明まで書く?
+# メタ計算
+- ノーマルレベルの計算
+ - コンピュータの計算はプログラミング言語で計算される。
+ - その部分をノーマルレベルの計算と呼ぶ。
+- メタレベルの計算
+ - コードが実行される際の以下の部分が、メタレベルの計算という。
+ - 処理系の詳細や使用する資源
+ - コードの仕様や型などの言語以外の部分
+
+# CbC
+- ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC(Continuation based C) を用いる。
+- CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。
+- CbC は関数呼び出し時の暗黙の環境を使わずに、コードの単位を行き来できる引数付き goto 文を持つ C と互換性のある言語である。
+- CbC を用いてCode Gear と Data Gear、メタ構造を導入する。
+
+# Gears OS
+- CbC を用いて導入したCode Gear、Data Gear、メタ構造を用いて、検証された Gears OS を構築したい。
+- 検証には 定理証明支援系である Agda を用いる。
+- Gears の記述をモジュール化するために Interface を導入した。
+- さらに並列処理の記述ように par goto 構文を導入する。
+
+# par goto の実行
+- 本論文では Interface と par goto の実装を記述し、評価を行なった。
+- また、マルチ CPU と GPU 上での par goto 文の実行を確認した。
+
# スライドの流れ
-- CbC
-- GearsOS
+- Gears OS におけるメタ計算
- Interface
- Context
- Gears OS の並列処理
@@ -30,10 +54,10 @@
- 比較
- 今後の課題
-# CbC
+# Gears OS におけるメタ計算
-# Gears OS
-- Gaears OS の構成
+
+# Gaears OS の構成
# Interface
diff -r e6422d20c0f2 -r 60405cc47b3a Slide/prosym.pdf.html
--- a/Slide/prosym.pdf.html Tue May 15 18:31:03 2018 +0900
+++ b/Slide/prosym.pdf.html Tue May 15 19:47:01 2018 +0900
@@ -70,7 +70,7 @@
@@ -111,12 +111,69 @@
-
スライドの流れ
+
メタ計算
+
+ - ノーマルレベルの計算
+
+ - コンピュータの計算はプログラミング言語で計算される。
+ - その部分をノーマルレベルの計算と呼ぶ。
+
+
+ - メタレベルの計算
+
+ - コードが実行される際の以下の部分が、メタレベルの計算という。
+
+ - 処理系の詳細や使用する資源
+ - コードの仕様や型などの言語以外の部分
+
+
+
+
+
+
+
+
+
+
+
CbC
+
+ - ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC(Continuation based C) を用いる。
+ - CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。
+ - CbC は関数呼び出し時の暗黙の環境を使わずに、コードの単位を行き来できる引数付き goto 文を持つ C と互換性のある言語である。
+ - CbC を用いてCode Gear と Data Gear、メタ構造を導入する。
+
+
+
+
+
+
+
Gears OS
+
+ - CbC を用いて導入したCode Gear、Data Gear、メタ構造を用いて、検証された Gears OS を構築したい。
+ - 検証には 定理証明支援系である Agda を用いる。
+ - Gears の記述をモジュール化するために Interface を導入した。
+ - さらに並列処理の記述ように par goto 構文を導入する。
+
+
+
+
+
+
+
par goto の実行
+
+ - 本論文では Interface と par goto の実装を記述し、評価を行なった。
+ - また、マルチ CPU と GPU 上での par goto 文の実行を確認した。
+
+
+
+
+
+
+
スライドの流れ
-
- CbC
+ Gears OS におけるメタ計算
- - GearsOS
- Interface
- Context
- Gears OS の並列処理
@@ -130,16 +187,13 @@
-
CbC
+Gears OS におけるメタ計算
-
Gears OS
-
+
Gaears OS の構成
@@ -157,7 +211,7 @@
-
Gears OS の並列処理
+Gears OS の並列処理
@@ -169,19 +223,19 @@
-
並列構文
+並列構文
-
比較
+比較
-
今後の課題
+今後の課題
diff -r e6422d20c0f2 -r 60405cc47b3a sigos.mm
--- a/sigos.mm Tue May 15 18:31:03 2018 +0900
+++ b/sigos.mm Tue May 15 19:47:01 2018 +0900
@@ -1,9 +1,12 @@