--- a/Paper/master_paper.lol	Fri Jan 19 18:09:30 2024 +0900
+++ b/Paper/master_paper.lol	Fri Jan 19 19:50:13 2024 +0900
@@ -2,7 +2,9 @@
 \contentsline {lstlisting}{\numberline {3.1}Queueのインターフェース}{12}{}%
 \contentsline {lstlisting}{\numberline {3.2}Interfaceの呼び出し}{13}{}%
 \contentsline {lstlisting}{\numberline {3.3}Queueのインターフェース}{13}{}%
-\contentsline {lstlisting}{\numberline {3.4}Treeの仕様}{15}{}%
-\contentsline {lstlisting}{\numberline {3.5}RedBlackTreeの実装}{15}{}%
+\contentsline {lstlisting}{\numberline {3.4}SingleLinkedQueueの型定義}{15}{}%
+\contentsline {lstlisting}{\numberline {3.5}Treeの仕様}{15}{}%
+\contentsline {lstlisting}{\numberline {3.6}RedBlackTreeの実装}{16}{}%
+\contentsline {lstlisting}{\numberline {3.7}RedBlackTreeの仕様}{16}{}%
 \contentsline {lstlisting}{\numberline {6.1}CopyRedBlackTreeの実装}{27}{}%
 \contentsline {lstlisting}{\numberline {6.2}CopyRedBlackTreeのアルゴリズム}{29}{}%

Binary file Paper/master_paper.pdf has changed

--- a/Paper/master_paper.tex	Fri Jan 19 18:09:30 2024 +0900
+++ b/Paper/master_paper.tex	Fri Jan 19 19:50:13 2024 +0900
@@ -305,12 +305,14 @@
 
 4行目でgotoによってqueue Interfaceのtake CodeGearに継続するよう記述している．
 takeのinputDataGearにはodgCommitCPUWorker4 CodeGearを指定している．
-ソースコード\ref{src:Queue.h}の仕様記述ではtakeにはqueue，data，nextがinputDataGearの型として指定されている．
+ソースコード\ref{src:Queue.h}の仕様記述ではtakeにはqueue，nextがinputDataGearの型として指定されている．
 しかし，実際に呼び出す際にはnextに当たるodgCommitCPUWorker4のみを渡している．
 仕様記述の際に全てのCodeGearの第1引数(inputDataGear)に渡している\texttt{Impl* queue}は，
 仕様から実装のCodeGearにgotoするために必要な記述である．
 軽量継続において，CodeGearを跨いで状態を保持することはできない．
 よって仕様から実装に遷移するためには，実装のCodeGearをinput DataGearとして渡す必要がある．
+このImplの第1引数はstubCodeGearで自動挿入されるため，
+実際にAPIを使用する際は渡す必要がない．
 inputDataGearのnextはCodeGearの処理が終わった際に次にgotoするCodeGearを指定する．
 よって，take CodeGearの処理が全て終了すると，次にodgCommitCPUWorker4へgotoする．
 nextは\texttt{next(...)}と引数に\texttt{...}が渡される．
@@ -342,7 +344,13 @@
 この整数を元にCodeGearが参照される．
 20行目以降では\texttt{putSingleLinkedQueue}や\texttt{takeSingleLinkedQueue}
 のように，仕様で記述されたCodeGearを実装している．
+15，16行目では実装の型定義で定義されたその実装独自のDataGearを初期化している．
+実装の型定義はソースコード\ref{src:SingleLinkedQueue.h}の通りである．
 
+\lstinputlisting[label=src:SingleLinkedQueue.h, caption=SingleLinkedQueueの型定義]{src/SingleLinkedQueue.h}
+
+3行目にあるように，実装の型定義ではimplキーワードで実装した型名を指定する．
+4，5行目でSingleLinkedQueueが独自にもつtop，lastのDataGearを記述している．
 
 \section{GearsOSのRedBlackTree}
 
@@ -357,14 +365,24 @@
 RedBlackTreeの実装の記述の一部をソースコード\ref{src:RedBlackTreeImpl.cbc}に示す．
 
 \lstinputlisting[label=src:Tree.h, caption=Treeの仕様]{src/Tree.h}
+
+ソースコード\ref{src:Tree.h}より，Treeはtree DataGearと
+put，get，remove，nextの4つのCodeGearをAPIとして持っていることがわかる．
+他にも探索や木のローテートを行うCodeGearが実装されているが，
+RedBlackTreeのAPIとして提供しているのはput，get，removeの3つであり，
+RedBlackTree Interfaceの使用者は木に対してこの3つの操作ができる．
+それぞれノードの挿入，取得，削除を行うCodeGearである．
+取得は，指定したnodeと一致するノードを木から探し，
+存在すればそのまま返す．
+
 \lstinputlisting[label=src:RedBlackTreeImpl.cbc, caption=RedBlackTreeの実装]{src/RedBlackTreeImpl.cbc}
 
-ソースコード\ref{src:Tree.h}より，Treeはtree DataGearと
-put，get，remove，nextの4つのCodeGearを持っていることがわかる．
 ソースコード\ref{src:RedBlackTreeImpl.cbc}の4行目から，
 RedBlackTreeはTreeの仕様の実装であることがわかり，
 13〜16行目で仕様に対応するCodeGearを初期化している．
 
+\lstinputlisting[label=src:RedBlackTree.h, caption=RedBlackTreeの仕様]{src/RedBlackTree.h}
+
 \chapter{GearsFileSystem}
 
 ファイルシステムはOSにおいてユーザーやアプリケーションが使用するファイルや

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/RedBlackTree.h	Fri Jan 19 19:50:13 2024 +0900
@@ -0,0 +1,11 @@
+typedef struct RedBlackTree <> impl Tree {
+  struct Node* root;
+  struct Node* current; // reading node of original tree;
+  struct Node* previous; // parent of reading node of original tree;
+  struct Node* newNode; // writing node of new tree;
+  struct Node* parent;
+  struct Node* grandparent;
+  struct Stack* nodeStack;
+  __code findNodeNext(...);
+  int result;
+} RedBlackTree;
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/SingleLinkedQueue.h	Fri Jan 19 19:50:13 2024 +0900
@@ -0,0 +1,6 @@
+#include "../../ModelChecking/TaskIterator.h"
+
+typedef struct SingleLinkedQueue <> impl Queue {
+  struct Element* top;
+  struct Element* last;
+} SingleLinkedQueue;

--- a/TODO.md	Fri Jan 19 18:09:30 2024 +0900
+++ b/TODO.md	Fri Jan 19 19:50:13 2024 +0900
@@ -1,5 +1,6 @@
 - [x] 要旨
 - [x] 1章 最後
+- [x] implementの型定義の説明
 - [ ] GearsOSのRedBlackTreeの説明
 - [ ] DGMによる分散ファイルシステム
 - [ ] レプリケーションの説明