# HG changeset patch
# User tobaru
# Date 1526809298 -32400
# Node ID 07b7aba92874380901a21a34a65952fa48924d23
# Parent  c456e4d68e1acc12eca511b1c10fd1b932dd3874
fix

diff -r c456e4d68e1a -r 07b7aba92874 Slide/prosym.html
--- a/Slide/prosym.html	Sun May 20 16:59:54 2018 +0900
+++ b/Slide/prosym.html	Sun May 20 18:41:38 2018 +0900
@@ -86,7 +86,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin15]
-                on 2018-05-20 16:59:15 +0900 with Markdown engine kramdown (1.13.2)
+                on 2018-05-20 17:18:27 +0900 with Markdown engine kramdown (1.13.2)
                   using options {}
   -->
 
@@ -144,10 +144,10 @@
 <!-- _S9SLIDE_ -->
 <h1 id="cbc">CbC</h1>
 <ul>
-  <li>ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC(Continuation based C) を用いる。</li>
+  <li>ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC を用いる。</li>
   <li>ノーマルレベルの計算
     <ul>
-      <li>コンピュータの計算はプログラミング言語で計算される。</li>
+      <li>コンピュータの計算はプログラミング言語で行われる。</li>
       <li>その部分をノーマルレベルの計算と呼ぶ。</li>
     </ul>
   </li>
@@ -190,11 +190,20 @@
     goto cg2(c);
 }
 </code></pre>
-<p># スライドの流れ
-- CbC
-- <font color="red">Gears OS における並列実行</font>
-- 比較
-- 今後の課題</p>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-1">スライドの流れ</h1>
+<ul>
+  <li>CbC</li>
+  <li>
+    <font color="red">Gears OS における並列実行</font>
+  </li>
+  <li>比較</li>
+  <li>今後の課題</li>
+</ul>
 
 
 </div>
@@ -269,7 +278,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-1">スライドの流れ</h1>
+<h1 id="section-2">スライドの流れ</h1>
 <ul>
   <li>CbC</li>
   <li>Gears OS における並列実行</li>
@@ -368,7 +377,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-2">評価の考察</h1>
+<h1 id="section-3">評価の考察</h1>
 <ul>
   <li>コア数が上がるごとに、処理速度が上がっている。</li>
   <li>GPUでの実行は 32CPU に比べて約7.2倍の速度向上が見られた。</li>
@@ -393,7 +402,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-3">スライドの流れ</h1>
+<h1 id="section-4">スライドの流れ</h1>
 <ul>
   <li>CbC</li>
   <li>Gears OS における並列実行</li>
@@ -407,7 +416,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-4">今後の課題</h1>
+<h1 id="section-5">今後の課題</h1>
 <ul>
   <li>Go 言語との比較から 1CPU での動作が遅いことがわかった。</li>
   <li>par goto 文を使用することで、Contextを生成し、並列処理を行う。</li>
diff -r c456e4d68e1a -r 07b7aba92874 Slide/prosym.md
--- a/Slide/prosym.md	Sun May 20 16:59:54 2018 +0900
+++ b/Slide/prosym.md	Sun May 20 18:41:38 2018 +0900
@@ -24,7 +24,12 @@
 	- OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまう。
 - 本研究室では、それらを実現することを目標に Gears OS の開発を行なっている。
 
+% 欠けてしまうで終わってるので　"それら"は 分かりづらい
+% 並列API 研究目的とAPIとの繋がりがない
+% モジュールとAPIの説明分ける
+% 拡張性と信頼性を実現する時に Interfaceと par goto 構文がなぜ必要なのかに繋げる話が必要
 % APIと実装の分離が望ましい理由は？
+
 # API と実装の分離
 - Gears OS は Continuation based C(以下、CbC)によって記述されている。
 - CbC は Code Gear と Data Gear の単位でプログラムを記述していて、システムやアプリケーションを作る際に、この2つは柔軟に再利用する必要がある。
@@ -32,12 +37,45 @@
 
 % 上と繋がってない
 % なんでモジュールシステムが必要？
+% 形式化と言わない
+% 形式化 formalization 
+% ここでいう形式化はInterfaceとは関係ない
+% interface は仕様とAPIの分離
+% 実装の分割 がInterface
+% まず、形式化が重要(仕様、実装、実行をlogicで記述)
+% その記述にAgdaを使う
+
+% Interfaceはほとんどかかない
+%  
+
+# Gears OS での形式化とInterfaceの導入
+- 形式化とは仕様、実装、実行を Logic で記述する事である。
+- Gears OS では、継続を使った関数型プログラムとして実装を記述する
+- Logic としては、依存型関数言語である Agda を使う(前の発表)
+- 証明とモデル検査を使って、信頼性を確保する
+
+# Gears OS の Interface 
+- この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
+- Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
+- Interface は Data Gear で記述されて、Meta Deta Gear と呼ばれる。
+- Java などの Class に相当する。
+- Interface を外から呼び出すための Code Gear 群の型
+- Interface を呼び出す時に必要となる引数を全て格納する Data Gear
+- 実装に使う Code Gear の番号が含まれている。
+- Code Gear の番号を変更することによって異なる実装を実現できる
+
+% Interface は実行時に実装を入れ替える事ができる
+% 呼び出すものはStack 上に積めない
+% Contextも集合
+% Inter 
+
 # 並列API
 - Geas OS 信頼性を保証するために、形式化されたモジュールシステムが必要である。
 - 本研究では、モジュールシステムとその応用である並列APIについて考察する。
 - 並列APIは継続を基本とした関数型プログラミングと両立する必要があり、ここでは CbC の goto 文を拡張した par goto を導入する。
 
 # スライドの流れ
+- Interface
 - <font color="red">CbC</font>
 - Gears OS における並列実行
 - 比較
@@ -48,18 +86,31 @@
 
 
 # CbC 
-- ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC(Continuation based C) を用いる。
+- ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC を用いる。
 - ノーマルレベルの計算
-	- コンピュータの計算はプログラミング言語で計算される。
+	- コンピュータの計算はプログラミング言語で行われる。
 	- その部分をノーマルレベルの計算と呼ぶ。
 - メタレベルの計算
 	- コードが実行される際の以下の部分が、メタレベルの計算という。
 		- 処理系の詳細や使用する資源
-		- コードの仕様や型などの言語以外の部分
+		- コードの仕様や型などの部分
+
+% ノーマルレベルとメタレベルの違い
+% 以外 = メモリ
+% 定義されたものに従って形式的にプログラムが記述されるが、その実行の資源や環境がメタレベル
+% 実行するのはOSや資源
+% 実際にはプログラムで記述されていない部分(CPU,メモリの資源、並列処理、外界の影響) この４つ書く
+% CbC の特徴はメタもかける
+% OS での資源はCbCでかける
+% シミュレーションされた外界
+% シミュレーションされてない外界はOSとは違うのでCbCで書けない
+% ぱるすさんの図入れるMeta data Gear 
+
 
 # CbC 
 - CbC を用いることで、ノーマルレベルの計算の信頼性をメタレベルから保証できるようになる。
-- CbC を用いてCode Gear と Data Gear、メタ構造を導入する。
+- CbC を用いてCode Gear と Data Gear を導入する。
+
 
 % - 検証には 定理証明支援系である Agda を用いる。
 % - Gears の記述をモジュール化するために Interface を導入した。
@@ -69,6 +120,9 @@
 % - 本論文では Interface と par goto の実装を記述し、評価を行なった。
 % - また、マルチ CPU と GPU 上での par goto 文の実行を確認した。
 
+% par goto には構文と実行の話がある
+% ストーリー的に早いのでここでは入れない 
+
 # CbC の構文
 - CbC の Code Gear は __code という型を持つ関数として記述する。
 - 継続で次の Code Gear に遷移するので、戻り値は持たない。
@@ -81,6 +135,19 @@
     goto cg2(c);
 }
 ```
+- CbC の記述だけでは並列実行にならない
+
+% 関数呼び出しで実装したい　なのでpar つける
+% 意味: 戻り値がなく　exitで呼び出す
+% par goto (並列実行を実装したい、形式化したい=Agdaの記述をしたい) 並列実行を形式化する
+% 本文のpar goto を削って載せる
+% なぜ par goto が必要か
+% context がこれの先に出てないとだめ
+% 形式化はどうするの？-> par goto を使う。
+% par goto を使えば並列実行されたGears の形式化ができる
+
+
+
 # スライドの流れ
 - CbC
 - <font color="red">Gears OS における並列実行</font>
@@ -93,27 +160,40 @@
 - それぞれにメタレベルの単位が存在し、Meta Data Gear と Meta Code Gear と呼ぶ。
 - メタレベルの計算は Perl スクリプトによって生成され、Code Gear で記述される。
 
-# Interface
-- この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
-- Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
+% # Interface
+% - この時、Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
+% - Interface 作成時に Code Gear の集合を指定することにより複数の実装を持つことができる。
 
 # Context
 - 1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。
 - この Meta Data Gear を Context と呼ぶ。 
 - Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。 
+- Context は Task でもある。
+- Task は実行する Code Gear と Data Gear を全て持っている。
 
 # par goto
 - Context の複製には par goto を用いる。
 - 他に、入力の同期、タスクスケジューラへの Context の登録が行われる。
 
-# Task 
-- Context は Task でもある。
-- 実行する Code Gear と Data Gear を全て持っている。
+% exit が説明不足
+% code gear の実行は他のシープに邪魔されない。
+% 並列実行時の書き換えは許してない
+
+# 1つの Code Gear の実行は他の Code Gear に割り込まれない 
+- 共有された Data Gear があった時に、それに対する変更はただ1つの Code Gear だけが許される
+- 読み込みは複数であってもいい
+- Agda 側で、並列実行を Code Gear の順次実行としてシミュレーションするため
+- このような実行になるように Gears OS の実装を行う
 
-% ここに入る前に __ の説明欲しい
+% 複数走ったなかの成功したものをコミットするのがexit 
+
+
+
+
 # __exit
-- par goto で生成された Task は __exit に継続することで終了する。
-- GearsOS の Task は Output Data Gear を生成した時点で終了する。
+- 複数実行した時に、共有 Data Gear に書き込みを成功したかを確認する(commit)
+- par goto で生成された Task は __exit に継続することで終了する
+- GearsOS の Task は Output Data Gear を生成した時点で終了する
 - そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。
 - Code Gear と Data Gear の依存関係をノーマルレベルで記述できるようになる。
 ```c
@@ -123,6 +203,8 @@
 }
 ```
 
+% 失敗した時はmeta compitation で処理する
+
 
 
 % # Interface
@@ -138,8 +220,12 @@
 - <font color="red">比較</font>
 - 今後の課題 
 
+# Gears OS の評価(目的)
+- 並列構文とそれを実現する Meta Compitation が十分に揃っているかを確認したい
+- 並列処理の台数効果を確認する
+- 既存の並列言語と比較して不要なオーバーヘッドがあるか調べたい  
 
-# Gears OS の評価
+# Gears OS の評価(環境)
 - CPU、GPU環境で Gears OS の測定を行う。
 - 使用した環境は次のようになる。
 	- CPU 環境
diff -r c456e4d68e1a -r 07b7aba92874 Slide/prosym.pdf.html
--- a/Slide/prosym.pdf.html	Sun May 20 16:59:54 2018 +0900
+++ b/Slide/prosym.pdf.html	Sun May 20 18:41:38 2018 +0900
@@ -70,7 +70,7 @@
 <!-- === begin markdown block ===
 
       generated by markdown/1.2.0 on Ruby 2.4.1 (2017-03-22) [x86_64-darwin15]
-                on 2018-05-20 16:59:15 +0900 with Markdown engine kramdown (1.13.2)
+                on 2018-05-20 17:18:27 +0900 with Markdown engine kramdown (1.13.2)
                   using options {}
   -->
 
@@ -128,10 +128,10 @@
 <!-- _S9SLIDE_ -->
 <h1 id="cbc">CbC</h1>
 <ul>
-  <li>ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC(Continuation based C) を用いる。</li>
+  <li>ノーマルレベルとメタレベルの計算を1つの言語で表現できる言語として、本研究室で設計した CbC を用いる。</li>
   <li>ノーマルレベルの計算
     <ul>
-      <li>コンピュータの計算はプログラミング言語で計算される。</li>
+      <li>コンピュータの計算はプログラミング言語で行われる。</li>
       <li>その部分をノーマルレベルの計算と呼ぶ。</li>
     </ul>
   </li>
@@ -174,11 +174,20 @@
     goto cg2(c);
 }
 </code></pre>
-<p># スライドの流れ
-- CbC
-- <font color="red">Gears OS における並列実行</font>
-- 比較
-- 今後の課題</p>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h1 id="section-1">スライドの流れ</h1>
+<ul>
+  <li>CbC</li>
+  <li>
+    <font color="red">Gears OS における並列実行</font>
+  </li>
+  <li>比較</li>
+  <li>今後の課題</li>
+</ul>
 
 
 </div>
@@ -253,7 +262,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-1">スライドの流れ</h1>
+<h1 id="section-2">スライドの流れ</h1>
 <ul>
   <li>CbC</li>
   <li>Gears OS における並列実行</li>
@@ -352,7 +361,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-2">評価の考察</h1>
+<h1 id="section-3">評価の考察</h1>
 <ul>
   <li>コア数が上がるごとに、処理速度が上がっている。</li>
   <li>GPUでの実行は 32CPU に比べて約7.2倍の速度向上が見られた。</li>
@@ -377,7 +386,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-3">スライドの流れ</h1>
+<h1 id="section-4">スライドの流れ</h1>
 <ul>
   <li>CbC</li>
   <li>Gears OS における並列実行</li>
@@ -391,7 +400,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h1 id="section-4">今後の課題</h1>
+<h1 id="section-5">今後の課題</h1>
 <ul>
   <li>Go 言語との比較から 1CPU での動作が遅いことがわかった。</li>
   <li>par goto 文を使用することで、Contextを生成し、並列処理を行う。</li>