Mercurial > hg > Papers > 2023 > soto-master

changeset 7:c821e707a5ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add paper dpp
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sun, 22 Jan 2023 21:20:59 +0900
parents 8c1e9a6d58e2
children d4f3d9d283a2
files Paper/Makefile Paper/fig/dpp-model.pdf Paper/master_paper.out Paper/master_paper.pdf Paper/master_paper.tex Paper/src/dpp-verif/spin.pml Paper/tex/agda.tex Paper/tex/dpp_impl.tex Paper/tex/spin_dpp.tex
diffstat 9 files changed, 93 insertions(+), 52 deletions(-) [+]
line wrap: on
line diff
--- a/Paper/Makefile	Sat Jan 21 20:47:38 2023 +0900
+++ b/Paper/Makefile	Sun Jan 22 21:20:59 2023 +0900
@@ -36,7 +36,7 @@
 	open $(TARGET).pdf
 
 clean:
-	rm -f *.dvi *.aux *.log *.ilg *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx src/*/*.replaced *.fdb_latexmk *.fls
+	rm -f *.dvi *.aux *.log *.ilg *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx src/**/*.replaced *.fdb_latexmk *.fls
 
 remake:
 	make clean
Binary file Paper/fig/dpp-model.pdf has changed
--- a/Paper/master_paper.out	Sat Jan 21 20:47:38 2023 +0900
+++ b/Paper/master_paper.out	Sun Jan 22 21:20:59 2023 +0900
@@ -22,14 +22,14 @@
 \BOOKMARK [2][]{subsection.5.3.3}{\376\377\0005\000.\0003\000.\0003\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\151\034\212\074}{section.5.3}% 21
 \BOOKMARK [0][]{chapter.6}{\376\377\173\054\0006\172\340\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373}{}% 22
 \BOOKMARK [1][]{section.6.1}{\376\377\0006\000.\0001\000\040\060\342\060\307\060\353\151\034\147\373\060\150\060\157}{chapter.6}% 23
-\BOOKMARK [1][]{section.6.2}{\376\377\0006\000.\0002\000\040\000S\000P\000I\000N\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373}{chapter.6}% 24
-\BOOKMARK [1][]{section.6.3}{\376\377\0006\000.\0003\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373\060\156\155\101\060\214}{chapter.6}% 25
-\BOOKMARK [1][]{section.6.4}{\376\377\0006\000.\0004\000\040\000D\000i\000n\000i\000n\000g\000\040\000P\000h\000i\000l\000o\000s\000o\000p\000h\000e\000r\000s\000\040\000P\000r\000o\000b\000l\000e\000m}{chapter.6}% 26
-\BOOKMARK [2][]{subsection.6.4.1}{\376\377\0006\000.\0004\000.\0001\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000D\000P\000P\060\156\133\237\210\305}{section.6.4}% 27
-\BOOKMARK [2][]{subsection.6.4.2}{\376\377\0006\000.\0004\000.\0002\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000D\000P\000P\060\156\151\034\212\074}{section.6.4}% 28
-\BOOKMARK [2][]{subsection.6.4.3}{\376\377\0006\000.\0004\000.\0003\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000\040\000l\000i\000v\000e\000\040\000l\000o\000c\000k\060\156\151\034\212\074\145\271\154\325\060\153\060\144\060\104\060\146}{section.6.4}% 29
-\BOOKMARK [2][]{subsection.6.4.4}{\376\377\0006\000.\0004\000.\0004\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\147\060\156\060\342\060\307\060\353\151\034\147\373\060\156\212\125\117\241}{section.6.4}% 30
-\BOOKMARK [0][]{chapter.7}{\376\377\173\054\0007\172\340\000\040\116\312\137\214\060\156\134\125\147\033}{}% 31
+\BOOKMARK [1][]{section.6.2}{\376\377\0006\000.\0002\000\040\000D\000i\000n\000i\000n\000g\000\040\000P\000h\000i\000l\000o\000s\000o\000p\000h\000e\000r\000s\000\040\000P\000r\000o\000b\000l\000e\000m}{chapter.6}% 24
+\BOOKMARK [1][]{section.6.3}{\376\377\0006\000.\0003\000\040\000S\000P\000I\000N\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373}{chapter.6}% 25
+\BOOKMARK [1][]{section.6.4}{\376\377\0006\000.\0004\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373\060\156\155\101\060\214}{chapter.6}% 26
+\BOOKMARK [1][]{section.6.5}{\376\377\0006\000.\0005\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000D\000P\000P\060\156\133\237\210\305}{chapter.6}% 27
+\BOOKMARK [1][]{section.6.6}{\376\377\0006\000.\0006\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000D\000P\000P\060\156\151\034\212\074}{chapter.6}% 28
+\BOOKMARK [1][]{section.6.7}{\376\377\0006\000.\0007\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000\040\000l\000i\000v\000e\000\040\000l\000o\000c\000k\060\156\151\034\212\074\145\271\154\325\060\153\060\144\060\104\060\146}{chapter.6}% 29
+\BOOKMARK [1][]{section.6.8}{\376\377\0006\000.\0008\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\147\060\156\060\342\060\307\060\353\151\034\147\373\060\156\212\125\117\241}{chapter.6}% 30
+\BOOKMARK [0][]{chapter.7}{\376\377\173\054\0007\172\340\000\040\060\176\060\150\060\201\060\150\116\312\137\214\060\156\134\125\147\033}{}% 31
 \BOOKMARK [0][]{chapter*.7}{\376\377\213\035\217\236}{}% 32
 \BOOKMARK [0][]{chapter*.8}{\376\377\123\302\200\003\145\207\163\056}{}% 33
 \BOOKMARK [0][]{chapter*.8}{\376\377\116\330\223\062}{}% 34
Binary file Paper/master_paper.pdf has changed
--- a/Paper/master_paper.tex	Sat Jan 21 20:47:38 2023 +0900
+++ b/Paper/master_paper.tex	Sun Jan 22 21:20:59 2023 +0900
@@ -137,14 +137,14 @@
 並列処理を定理証明にて検証するには考慮する状態が多すぎる。
 そのため、並列処理はモデル検査にて検証する。
 \section{モデル検査とは}
-\section{SPINによるモデル検査}% 内容にそぐわない場合は使わない
+\input{tex/spin_dpp.tex}% Gears Agda の記法　loopのやつやる
 \section{Gears Agdaによるモデル検査の流れ}
 
 % Gears Agdaの場合はListの方が停止することがわかりやすいので、今回はState Listを作成した。本来はburanceされたtree structureが最も良い
 
 \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる
 
-\chapter{今後の展望}
+\chapter{まとめと今後の展望}
 ここまでで Gears Agda により定理証明を用いた検証と
 モデル検査による検証方法を確立した．
 これからは Red Black Tree の定理証明を用いた検証と，
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/dpp-verif/spin.pml	Sun Jan 22 21:20:59 2023 +0900
@@ -0,0 +1,16 @@
+proctype Philosopher(byte id) {
+Think:
+ if
+ :: atomic { fork[id] == 0 -> fork[id] = id + 1; };
+ :: atomic { fork[(id + 1)%N] == 0 -> fork[(id + 1)%N] = id + 1; };
+ fi;
+One:
+ if
+ :: atomic { fork[id] == id + 1 -> fork[(id + 1)%N] == 0 -> fork[(id + 1)%N] = id + 1; nr_eat++; };
+ :: atomic { fork[id] == 0 -> fork[(id + 1)%N] == id + 1 -> fork[id] = id + 1; nr_eat++; };
+ fi;
+Eat:
+ d_step { nr_eat--; fork[(id + 1)%N] = 0; }
+ fork[id] = 0;
+ goto Think;
+}
\ No newline at end of file
--- a/Paper/tex/agda.tex	Sat Jan 21 20:47:38 2023 +0900
+++ b/Paper/tex/agda.tex	Sun Jan 22 21:20:59 2023 +0900
@@ -98,7 +98,7 @@
 \verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという
 \coderef{cong}の \verb/cong/ を使って，y の値を 1 減らしたのち，再帰的に \verb/+zero y/
 を用いて証明している．
-\lstinputlisting[caption=congによる等式変換の例,label=code:cong]{src/cong.agda.replaced}
+\lstinputlisting[caption=congの定義,label=code:cong]{src/cong.agda.replaced}
 
 %% \begin{lstlisting}[caption=等式変形の例,label=proof]
 %% +zero : { y : ℕ } → y + zero  ≡ y
@@ -116,7 +116,7 @@
 \coderef{agda-term-post} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である．
 ここでは，\verb/+zero/ を利用し， \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり，左右の項が等しいことを示す \verb/refl/ になっている．
 
-\lstinputlisting[caption=等式変形の例3/3,label=code:agda-term-post]{src/agda-term3.agda.replaced}
+\lstinputlisting[caption=congを用いた等式変形の例,label=code:agda-term-post]{src/agda-term3.agda.replaced}
 \coderef{agda-term-post} では \verb/suc (y + x)/ $equiv$ \verb/y + (suc x)/ という等式に対して $equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $equiv$ \verb/suc (y + x)/の形にし，\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した．
 これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた．
 
--- a/Paper/tex/dpp_impl.tex	Sat Jan 21 20:47:38 2023 +0900
+++ b/Paper/tex/dpp_impl.tex	Sun Jan 22 21:20:59 2023 +0900
@@ -1,39 +1,4 @@
-\section{Dining Philosophers Problem}
-今回はモデル検査を行う対象として Dining Philosophers Problem （以下DPP）
-を用いることとした．
-DPP とは資源共有問題であり，モデル検査をする際に挙げられる代表的な問題
-である．
-
-DPPのストーリーを図 \ref{fig:DPP} に示している． 
-
-\begin{figure}[htpb]
-    \begin{center}
-     \scalebox{0.5}{\includegraphics{fig/Dining.pdf}}
-    \end{center}
-    \caption{メタ計算を可視化した CodeGear と DataGear}
-    \label{fig:DPP}
-\end{figure}   
-
-したがって，哲学者は以下のようなフローを独立して並列に繰り返し実行することとなる．
-
-\begin{enumerate}
-    \item しばらくの間思考を行う
-    \item 食事をするために右のフォークを取る
-    \item 右のフォークを取ったら，次は左のフォークを取る
-    \item 両方のフォークを取ったら，しばらく食事をする
-    \item 思考に戻るために左手に持っているフォークをテーブルに置く
-    \item 左手のフォークを置いたあとは右のフォークをテーブルに置く
-\end{enumerate}
-
-この際，すべての哲学者が同時に右のフォークを取った場合のことを考える．
-すべての哲学者はフォークを持っている．次に哲学者は左のフォークを取ろうと
-する．しかしフォークは哲学者の人数と同じ数だけ存在しているため，
-テーブルの上にフォークはすでにひとつも存在しない．
-すべての哲学者は左のフォークを取ろうとするが
-誰も右のフォークを置くことがないため，すべての哲学者の動作がこの状態で止まる．（dead lock）
-これが起こることを Gears Agda で検出したい．
-
-\subsection{Gears Agda によるDPPの実装}
+\section{Gears Agda によるDPPの実装}
 
 DPP の記述の主要部分を示し，説明する．
 
@@ -100,7 +65,7 @@
 
 思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている．
 
-\subsection{Gears Agda によるDPPの検証}
+\section{Gears Agda によるDPPの検証}
 
 これまでの実装は一般的なDPPの実装であったため、
 Code / Data Gear の実装であった。
@@ -171,7 +136,7 @@
 
 あとは State List を dead lock の検査を行う Meta Code Gear に与えるとどの state が dead lockしているかを検証することができる
 
-\subsection{Gears Agda による live lockの検証方法について}
+\section{Gears Agda による live lockの検証方法について}
 live lockとは、状態が変動しているが、その状態はループしており、実行が進んでいないことを指す。
 
 DPPにて例を上げると、(上の哲学者のフローだと) dead lock が発生するため、フローを変更したとする。それは以下のような動作を追加する。
@@ -186,7 +151,7 @@
 今回のはDPPであるためEatingが挙げられているが、他の実装であれば、どのコマンドが実行されるのが正常な動きなのかを決める。それがloop中に存在いしているかを見れば live lock を検知できる。
 
 
-\subsection{Gears Agda でのモデル検査の評価}
+\section{Gears Agda でのモデル検査の評価}
 
 SPINで行ったDPPのモデル検査に比べると、Gears Agdaの方が制約が多いため難解に思える。しかし、Gears Agda ではプログラムの実装も含んでいる。
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/tex/spin_dpp.tex	Sun Jan 22 21:20:59 2023 +0900
@@ -0,0 +1,60 @@
+\section{Dining Philosophers Problem}
+今回はモデル検査を行う対象として Dining Philosophers Problem (以下DPP)
+を用いることとした．
+DPP とは資源共有問題であり，モデル検査をする際に挙げられる代表的な問題
+である．
+
+DPPのストーリーを図 \ref{fig:DPP} に示している． 
+
+\begin{figure}[htpb]
+    \begin{center}
+     \scalebox{0.5}{\includegraphics{fig/Dining.pdf}}
+    \end{center}
+    \caption{メタ計算を可視化した CodeGear と DataGear}
+    \label{fig:DPP}
+\end{figure}   
+
+したがって，哲学者は以下のようなフローを独立して並列に繰り返し実行することとなる．
+
+\begin{enumerate}
+    \item しばらくの間思考を行う
+    \item 食事をするために右のフォークを取る
+    \item 右のフォークを取ったら，次は左のフォークを取る
+    \item 両方のフォークを取ったら，しばらく食事をする
+    \item 思考に戻るために左手に持っているフォークをテーブルに置く
+    \item 左手のフォークを置いたあとは右のフォークをテーブルに置く
+\end{enumerate}
+
+この際，すべての哲学者が同時に右のフォークを取った場合のことを考える．
+すべての哲学者はフォークを持っている．次に哲学者は左のフォークを取ろうと
+する．しかしフォークは哲学者の人数と同じ数だけ存在しているため，
+テーブルの上にフォークはすでにひとつも存在しない．
+すべての哲学者は左のフォークを取ろうとするが
+誰も右のフォークを置くことがないため，すべての哲学者の動作がこの状態で止まる．（dead lock）
+これが起こることを Gears Agda で検出したい．
+
+\section{SPINによるモデル検査}% 内容にそぐわない場合は使わない
+
+SPIN(Simple Promela INterpreter) とは一般的にモデル検査に使用されるツールである。Promera(Process Meta Language) によって記述されたコードを元にプログラムが取る状態を網羅し、モデル検査を行うことができる。
+
+今回 Gears Agda でのモデル検査と比較するために、SPINでのDPPプログラムのモデル検査に必要なコードの一部を\coderef{spin-dpp}に載せる。
+
+\lstinputlisting[caption= SPINにてDPPをモデル検査する際のコードの一部 , label=code:spin-dpp]{src/dpp-verif/spin.pml}
+
+コードを簡単に説明する。哲学者がThinkの状態から食事をしようとしだした際の状態の変化が4行目と5行目になっている。
+forkの状態を配列で管理している。0 である状態が誰もそのforkを持っていない状態である。ここでは、5人目の人が右手にあるフォークを取ろうとした際に配列の最初を取ることが5行目に記述されている。
+
+左手のフォークを取る動作も同じように記述する。
+SPINではこのコードを元にプログラムが取りうる状態全てを網羅し、モデル検査を行うことができる。
+
+\figref{DPP-model}はこのPromelaから作成された状態遷移図になる。
+SPINではコードからプログラムの状態遷移図を出力することができる他、プログラムのstep実行など幅広くモデル検査を行うことができる。
+
+\begin{figure}[htpb]
+    \begin{center}
+     \scalebox{0.6}{\includegraphics{fig/dpp-model.pdf}}
+    \end{center}
+    \caption{SPINにて作成した状態遷移図}
+    \label{fig:DPP-model}
+\end{figure}
+