# HG changeset patch
# User tobaru
# Date 1526957792 -32400
# Node ID 6fdcb5241bdab89bd463afc898ccc8a39915ef9f
# Parent  d4e58a38aae79f347c518a8dd17c1981634c6d53
before Society

diff -r d4e58a38aae7 -r 6fdcb5241bda Slide/prosym.html
--- a/Slide/prosym.html	Tue May 22 10:13:39 2018 +0900
+++ b/Slide/prosym.html	Tue May 22 11:56:32 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-22 10:11:16 +0900 with Markdown engine kramdown (1.13.2)
+                on 2018-05-22 10:58:28 +0900 with Markdown engine kramdown (1.13.2)
                   using options {}
   -->
 
@@ -109,7 +109,7 @@
 <h2 id="section">スライドの流れ</h2>
 <ul>
   <li>
-    <font color="red">Interface</font>
+    <font color="red">Gears OS での形式化とInterfaceの導入</font>
   </li>
   <li>並列API</li>
   <li>CbC</li>
@@ -122,7 +122,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="gears-os-interface">Gears OS での形式化とInterfaceの導入</h2>
+<h2 id="gears-os-">Gears OS での形式化</h2>
 <ul>
   <li>形式化とは仕様、実装、実行を Logic で記述する事である。</li>
   <li>Gears OS では、継続を使った関数型プログラムとして実装を記述する</li>
@@ -136,7 +136,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="gears-os--interface">Gears OS の Interface</h2>
 <ul>
-  <li>Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
+  <li>Code Gear と Deta Gear は Interface と呼ばれるまとまりで記述される。
     <ul>
       <li>Gears OS のモジュール化</li>
     </ul>
@@ -153,7 +153,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="section-1">スライドの流れ</h2>
 <ul>
-  <li>Interface</li>
+  <li>Gears OS での形式化とInterfaceの導入</li>
   <li>
     <font color="red">並列API</font>
   </li>
@@ -185,7 +185,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="section-2">スライドの流れ</h2>
 <ul>
-  <li>Interface</li>
+  <li>Gears OS での形式化とInterfaceの導入</li>
   <li>並列API</li>
   <li>
     <font color="red">CbC</font>
@@ -205,7 +205,7 @@
     <ul>
       <li>ノーマルレベルの計算
         <ul>
-          <li>コンピュータの計算はプログラミング言語で行われる。</li>
+          <li>コンピュータの計算はプログラミング言語で記述される。</li>
           <li>その部分をノーマルレベルの計算と呼ぶ。</li>
         </ul>
       </li>
@@ -269,7 +269,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="section-3">スライドの流れ</h2>
 <ul>
-  <li>Interface</li>
+  <li>Gears OS での形式化とInterfaceの導入</li>
   <li>並列API</li>
   <li>CbC</li>
   <li>
@@ -297,7 +297,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="gears-os-">Gears OS の構造</h2>
+<h2 id="gears-os--1">Gears OS の構造</h2>
 <ul>
   <li>Gears OS は以下の要素で構成されている
     <ul>
@@ -321,10 +321,25 @@
 <ul>
   <li>1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。</li>
   <li>この Meta Data Gear を Context と呼ぶ。</li>
-  <li>Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。</li>
+  <li><strong>Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。</strong></li>
   <li>ノーマルレベルでは見る事ができない。</li>
+</ul>
+<div style="text-align: center;">
+    <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400" />
+</div>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="task">Task</h2>
+<ul>
   <li>Context は Task でもある。</li>
-  <li>Task は実行する Code Gear と Data Gear を全て持っている。</li>
+  <li>Task は実行する Code Gear と Data Gear を全て持っている。
+    <ul>
+      <li>Interface の Code Gear と Data Gear は Meta Data Gear に格納</li>
+    </ul>
+  </li>
 </ul>
 <div style="text-align: center;">
     <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400" />
@@ -364,8 +379,11 @@
 <!-- _S9SLIDE_ -->
 <h2 id="code-gear--code-gear-">1つの Code Gear の実行は他の Code Gear に割り込まれない</h2>
 <ul>
-  <li>共有された Data Gear があった時に、それに対する変更はただ1つの Code Gear だけが許される</li>
-  <li>読み込みは複数であってもいい</li>
+  <li>共有された Data Gear があった時に、それに対する変更はただ1つの Code Gear だけが許される
+    <ul>
+      <li>読み込みは複数であってもいい</li>
+    </ul>
+  </li>
   <li>Agda 側で、並列実行を Code Gear の順次実行としてシミュレーションするため</li>
   <li>このような実行になるように Gears OS の実装を行う</li>
 </ul>
@@ -374,14 +392,20 @@
     <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400" />
 </div>
 
-<h1 id="par-goto">par goto</h1>
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="par-goto">par goto</h2>
 <ul>
   <li>Context(Task) の複製には par goto を用いる。</li>
-  <li>他に、入力の同期、タスクスケジューラへの Context の登録が行われる。</li>
   <li>複数実行した時に、共有 Data Gear に書き込みを成功したかを確認(commit)するために __exit を使用する。</li>
-  <li>par goto で生成された Task は __exit に継続することで終了する</li>
-  <li>GearsOS の Task は Output Data Gear を生成した時点で終了する</li>
-  <li>そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。</li>
+  <li>par goto で生成された Task は Output Data Gear を生成した時点で終了する
+    <ul>
+      <li>そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。</li>
+      <li>割り込みを防ぐため</li>
+    </ul>
+  </li>
 </ul>
 
 <pre lang="c"><code>__code code1(Integer *integer1, Integer * integer2, Integer *output) {
@@ -422,7 +446,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="section-4">スライドの流れ</h2>
 <ul>
-  <li>Interface</li>
+  <li>Gears OS での形式化とInterfaceの導入</li>
   <li>並列API</li>
   <li>CbC</li>
   <li>Gears OS における並列実行</li>
@@ -436,7 +460,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="gears-os--1">Gears OS の評価(目的)</h2>
+<h2 id="gears-os--2">Gears OS の評価(目的)</h2>
 <ul>
   <li>並列構文とそれを実現する Meta Compitation が十分に揃っているかを確認したい</li>
   <li>並列処理の台数効果を確認する</li>
@@ -447,7 +471,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="gears-os--2">Gears OS の評価(環境)</h2>
+<h2 id="gears-os--3">Gears OS の評価(環境)</h2>
 <ul>
   <li>CPU、GPU環境で Gears OS の測定を行う。</li>
   <li>使用した環境は次のようになる。
@@ -608,7 +632,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="section-6">スライドの流れ</h2>
 <ul>
-  <li>Interface</li>
+  <li>Gears OS での形式化とInterfaceの導入</li>
   <li>並列API</li>
   <li>CbC</li>
   <li>Gears OS における並列実行</li>
@@ -622,21 +646,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="section-7">スライドの流れ</h2>
-<ul>
-  <li>CbC</li>
-  <li>Gears OS における並列実行</li>
-  <li>比較</li>
-  <li>
-    <font color="red">今後の課題</font>
-  </li>
-</ul>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="section-8">今後の課題</h2>
+<h2 id="section-7">今後の課題</h2>
 <ul>
   <li>Go 言語との比較から 1CPU での動作が遅いことがわかった。</li>
   <li>par goto 文を使用することで、Contextを生成し、並列処理を行う。</li>
diff -r d4e58a38aae7 -r 6fdcb5241bda Slide/prosym.md
--- a/Slide/prosym.md	Tue May 22 10:13:39 2018 +0900
+++ b/Slide/prosym.md	Tue May 22 11:56:32 2018 +0900
@@ -50,7 +50,7 @@
 
 
 ## スライドの流れ
-- <font color="red">Interface</font>
+- <font color="red">Gears OS での形式化とInterfaceの導入</font>
 - 並列API
 - CbC
 - Gears OS における並列実行
@@ -58,14 +58,14 @@
 - 今後の課題 
 
 
-## Gears OS での形式化とInterfaceの導入
+## Gears OS での形式化
 - 形式化とは仕様、実装、実行を Logic で記述する事である。
 - Gears OS では、継続を使った関数型プログラムとして実装を記述する
 - Logic としては、依存型関数言語である Agda を使う(外間の発表)
 - 証明とモデル検査を使って、信頼性を確保する
 
 ## Gears OS の Interface 
-- Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
+- Code Gear と Deta Gear は Interface と呼ばれるまとまりで記述される。
 	- Gears OS のモジュール化
 - Interface 作成時に Code Gear の集合を指定することにより複数の実装(並列処理)を持つことができる。
 - Interface は Data Gear で記述されて、Meta Deta Gear と呼ばれる。
@@ -81,7 +81,7 @@
 % Contextも集合
 
 ## スライドの流れ
-- Interface
+- Gears OS での形式化とInterfaceの導入 
 - <font color="red">並列API</font>
 - CbC
 - Gears OS における並列実行
@@ -97,7 +97,7 @@
 	- 応用として par goto を使って 並列API を実装
 
 ## スライドの流れ
-- Interface
+- Gears OS での形式化とInterfaceの導入 
 - 並列API
 - <font color="red">CbC</font>
 - Gears OS における並列実行
@@ -111,7 +111,7 @@
 ## CbC 
 - ノーマルレベルとメタレベルの計算をまとめて表現できる言語として、本研究室で設計した CbC を用いる。
 	- ノーマルレベルの計算
-		- コンピュータの計算はプログラミング言語で行われる。
+		- コンピュータの計算はプログラミング言語で記述される。
 		- その部分をノーマルレベルの計算と呼ぶ。
 	- メタレベルの計算
 		- コードが実行される際の以下の部分が、メタレベルの計算という。
@@ -173,7 +173,7 @@
 
 
 ## スライドの流れ
-- Interface
+- Gears OS での形式化とInterfaceの導入 
 - 並列API
 - CbC
 - <font color="red">Gears OS における並列実行</font>
@@ -209,14 +209,21 @@
 ## Context
 - 1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。
 - この Meta Data Gear を Context と呼ぶ。 
-- Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。 
+- **Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。**
 - ノーマルレベルでは見る事ができない。
-- Context は Task でもある。
-- Task は実行する Code Gear と Data Gear を全て持っている。
 <div style="text-align: center;">
     <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400">
 </div>
 
+## Task
+- Context は Task でもある。
+- Task は実行する Code Gear と Data Gear を全て持っている。
+	- Interface の Code Gear と Data Gear は Meta Data Gear に格納
+<div style="text-align: center;">
+    <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400">
+</div>
+
+
 
 
 ## TaskManager
@@ -245,7 +252,7 @@
 
 ## 1つの Code Gear の実行は他の Code Gear に割り込まれない 
 - 共有された Data Gear があった時に、それに対する変更はただ1つの Code Gear だけが許される
-- 読み込みは複数であってもいい
+	- 読み込みは複数であってもいい
 - Agda 側で、並列実行を Code Gear の順次実行としてシミュレーションするため
 - このような実行になるように Gears OS の実装を行う
 
@@ -256,16 +263,13 @@
 </div>
 
 
-
-
-
-# par goto  
+## par goto  
 - Context(Task) の複製には par goto を用いる。
-- 他に、入力の同期、タスクスケジューラへの Context の登録が行われる。
 - 複数実行した時に、共有 Data Gear に書き込みを成功したかを確認(commit)するために __exit を使用する。
-- par goto で生成された Task は __exit に継続することで終了する
-- GearsOS の Task は Output Data Gear を生成した時点で終了する
-- そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。
+- par goto で生成された Task は Output Data Gear を生成した時点で終了する
+	- そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。
+	- 割り込みを防ぐため
+% - 他に、入力の同期、タスクスケジューラへの Context の登録が行われる。
 % - Code Gear と Data Gear の依存関係をノーマルレベルで記述できるようになる。
 ```c
 __code code1(Integer *integer1, Integer * integer2, Integer *output) {
@@ -327,7 +331,7 @@
 % ## 並列構文
 
 ## スライドの流れ
-- Interface
+- Gears OS での形式化とInterfaceの導入 
 - 並列API
 - CbC
 - Gears OS における並列実行
@@ -460,7 +464,7 @@
 
 
 ## スライドの流れ
-- Interface
+- Gears OS での形式化とInterfaceの導入 
 - 並列API
 - CbC
 - Gears OS における並列実行
@@ -468,12 +472,6 @@
 - <font color="red">今後の課題</font>
 
 
-## スライドの流れ
-- CbC
-- Gears OS における並列実行
-- 比較
-- <font color="red">今後の課題</font>
-
 ## 今後の課題
 - Go 言語との比較から 1CPU での動作が遅いことがわかった。
 - par goto 文を使用することで、Contextを生成し、並列処理を行う。
diff -r d4e58a38aae7 -r 6fdcb5241bda Slide/prosym.pdf.html
--- a/Slide/prosym.pdf.html	Tue May 22 10:13:39 2018 +0900
+++ b/Slide/prosym.pdf.html	Tue May 22 11:56:32 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-22 10:11:16 +0900 with Markdown engine kramdown (1.13.2)
+                on 2018-05-22 10:58:28 +0900 with Markdown engine kramdown (1.13.2)
                   using options {}
   -->
 
@@ -93,7 +93,7 @@
 <h2 id="section">スライドの流れ</h2>
 <ul>
   <li>
-    <font color="red">Interface</font>
+    <font color="red">Gears OS での形式化とInterfaceの導入</font>
   </li>
   <li>並列API</li>
   <li>CbC</li>
@@ -106,7 +106,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="gears-os-interface">Gears OS での形式化とInterfaceの導入</h2>
+<h2 id="gears-os-">Gears OS での形式化</h2>
 <ul>
   <li>形式化とは仕様、実装、実行を Logic で記述する事である。</li>
   <li>Gears OS では、継続を使った関数型プログラムとして実装を記述する</li>
@@ -120,7 +120,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="gears-os--interface">Gears OS の Interface</h2>
 <ul>
-  <li>Code Gear と Deta Gear は Interface と呼ばれるまとまり(モジュール)で記述される。
+  <li>Code Gear と Deta Gear は Interface と呼ばれるまとまりで記述される。
     <ul>
       <li>Gears OS のモジュール化</li>
     </ul>
@@ -137,7 +137,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="section-1">スライドの流れ</h2>
 <ul>
-  <li>Interface</li>
+  <li>Gears OS での形式化とInterfaceの導入</li>
   <li>
     <font color="red">並列API</font>
   </li>
@@ -169,7 +169,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="section-2">スライドの流れ</h2>
 <ul>
-  <li>Interface</li>
+  <li>Gears OS での形式化とInterfaceの導入</li>
   <li>並列API</li>
   <li>
     <font color="red">CbC</font>
@@ -189,7 +189,7 @@
     <ul>
       <li>ノーマルレベルの計算
         <ul>
-          <li>コンピュータの計算はプログラミング言語で行われる。</li>
+          <li>コンピュータの計算はプログラミング言語で記述される。</li>
           <li>その部分をノーマルレベルの計算と呼ぶ。</li>
         </ul>
       </li>
@@ -253,7 +253,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="section-3">スライドの流れ</h2>
 <ul>
-  <li>Interface</li>
+  <li>Gears OS での形式化とInterfaceの導入</li>
   <li>並列API</li>
   <li>CbC</li>
   <li>
@@ -281,7 +281,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="gears-os-">Gears OS の構造</h2>
+<h2 id="gears-os--1">Gears OS の構造</h2>
 <ul>
   <li>Gears OS は以下の要素で構成されている
     <ul>
@@ -305,10 +305,25 @@
 <ul>
   <li>1つのスレッド内で使われる Interface の Code Gear と Data Gear は Meta Data Gear に格納される。</li>
   <li>この Meta Data Gear を Context と呼ぶ。</li>
-  <li>Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。</li>
+  <li><strong>Context を複製して複数の CPU に割り当てることにより並列実行が可能になる。</strong></li>
   <li>ノーマルレベルでは見る事ができない。</li>
+</ul>
+<div style="text-align: center;">
+    <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400" />
+</div>
+
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="task">Task</h2>
+<ul>
   <li>Context は Task でもある。</li>
-  <li>Task は実行する Code Gear と Data Gear を全て持っている。</li>
+  <li>Task は実行する Code Gear と Data Gear を全て持っている。
+    <ul>
+      <li>Interface の Code Gear と Data Gear は Meta Data Gear に格納</li>
+    </ul>
+  </li>
 </ul>
 <div style="text-align: center;">
     <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400" />
@@ -348,8 +363,11 @@
 <!-- _S9SLIDE_ -->
 <h2 id="code-gear--code-gear-">1つの Code Gear の実行は他の Code Gear に割り込まれない</h2>
 <ul>
-  <li>共有された Data Gear があった時に、それに対する変更はただ1つの Code Gear だけが許される</li>
-  <li>読み込みは複数であってもいい</li>
+  <li>共有された Data Gear があった時に、それに対する変更はただ1つの Code Gear だけが許される
+    <ul>
+      <li>読み込みは複数であってもいい</li>
+    </ul>
+  </li>
   <li>Agda 側で、並列実行を Code Gear の順次実行としてシミュレーションするため</li>
   <li>このような実行になるように Gears OS の実装を行う</li>
 </ul>
@@ -358,14 +376,20 @@
     <img src="./image/gears_structure.png" alt="Gears OS の構造" width="400" />
 </div>
 
-<h1 id="par-goto">par goto</h1>
+
+</div>
+<div class='slide '>
+<!-- _S9SLIDE_ -->
+<h2 id="par-goto">par goto</h2>
 <ul>
   <li>Context(Task) の複製には par goto を用いる。</li>
-  <li>他に、入力の同期、タスクスケジューラへの Context の登録が行われる。</li>
   <li>複数実行した時に、共有 Data Gear に書き込みを成功したかを確認(commit)するために __exit を使用する。</li>
-  <li>par goto で生成された Task は __exit に継続することで終了する</li>
-  <li>GearsOS の Task は Output Data Gear を生成した時点で終了する</li>
-  <li>そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。</li>
+  <li>par goto で生成された Task は Output Data Gear を生成した時点で終了する
+    <ul>
+      <li>そのため、par goto では直接 __exit に継続せず、Output Data Gear への書き出し処理に継続される。</li>
+      <li>割り込みを防ぐため</li>
+    </ul>
+  </li>
 </ul>
 
 <pre lang="c"><code>__code code1(Integer *integer1, Integer * integer2, Integer *output) {
@@ -406,7 +430,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="section-4">スライドの流れ</h2>
 <ul>
-  <li>Interface</li>
+  <li>Gears OS での形式化とInterfaceの導入</li>
   <li>並列API</li>
   <li>CbC</li>
   <li>Gears OS における並列実行</li>
@@ -420,7 +444,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="gears-os--1">Gears OS の評価(目的)</h2>
+<h2 id="gears-os--2">Gears OS の評価(目的)</h2>
 <ul>
   <li>並列構文とそれを実現する Meta Compitation が十分に揃っているかを確認したい</li>
   <li>並列処理の台数効果を確認する</li>
@@ -431,7 +455,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="gears-os--2">Gears OS の評価(環境)</h2>
+<h2 id="gears-os--3">Gears OS の評価(環境)</h2>
 <ul>
   <li>CPU、GPU環境で Gears OS の測定を行う。</li>
   <li>使用した環境は次のようになる。
@@ -592,7 +616,7 @@
 <!-- _S9SLIDE_ -->
 <h2 id="section-6">スライドの流れ</h2>
 <ul>
-  <li>Interface</li>
+  <li>Gears OS での形式化とInterfaceの導入</li>
   <li>並列API</li>
   <li>CbC</li>
   <li>Gears OS における並列実行</li>
@@ -606,21 +630,7 @@
 </div>
 <div class='slide '>
 <!-- _S9SLIDE_ -->
-<h2 id="section-7">スライドの流れ</h2>
-<ul>
-  <li>CbC</li>
-  <li>Gears OS における並列実行</li>
-  <li>比較</li>
-  <li>
-    <font color="red">今後の課題</font>
-  </li>
-</ul>
-
-
-</div>
-<div class='slide '>
-<!-- _S9SLIDE_ -->
-<h2 id="section-8">今後の課題</h2>
+<h2 id="section-7">今後の課題</h2>
 <ul>
   <li>Go 言語との比較から 1CPU での動作が遅いことがわかった。</li>
   <li>par goto 文を使用することで、Contextを生成し、並列処理を行う。</li>