Mercurial > hg > Papers > 2008 > atsuki-master

changeset 12:9b2553e32341

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author atsuki
date Fri, 15 Feb 2008 22:16:02 +0900
parents fd717f2d19ab
children f2f4577cf0ab
files paper/bibliography.tex paper/chapter4.tex paper/src/DiningPhil.java
diffstat 3 files changed, 144 insertions(+), 73 deletions(-) [+]
line wrap: on
line diff
--- a/paper/bibliography.tex	Fri Feb 15 19:59:17 2008 +0900
+++ b/paper/bibliography.tex	Fri Feb 15 22:16:02 2008 +0900
@@ -1,19 +1,19 @@
 \begin{thebibliography}{99}
     \bibitem{bib:jssst2006}
-	下地篤樹, 河野真治. ``タブロー法を用いたContinuation based Cプログラムの検証''.
-	日本ソフトウェア科学会第23回大会, 2006.
+	Ƽ, . ``֥ˡѤContinuation based Cץθ''.
+	ܥեȥʳز23, 2006.
     \bibitem{bib:sigos2007}
-	下地篤樹, 河野真治. ``線形時相論理によるContinuation based Cプログラムの検証''.
-	情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), April, 2007.
+	Ƽ, . ``ˤContinuation based Cץθ''.
+	ز񥷥ƥॽեȥȥڥ졼ƥ󥰡ƥฦ(OS), April, 2007.
     \bibitem{bib:jssst2000kono}
-	河野真治. ``継続を持つCの下位言語によるシステム記述''.
-	日本ソフトウェア科学会第17回大会, 2000.
+	. ``³Cβ̸ˤ륷ƥ൭''.
+	ܥեȥʳز17, 2000.
     \bibitem{bib:sigos2000shimabukuro}
-	島袋仁, 河野真治. ``C with Continuationと、そのPlayStationへの応用''.
-	情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), May, 2000.
+	޿, . ``C with ContinuationȡPlayStationؤα''.
+	ز񥷥ƥॽեȥȥڥ졼ƥ󥰡ƥฦ(OS), May, 2000.
     \bibitem{bib:jssst2001higa}
-	比嘉薫, 河野真治. ``タブロー法の負荷分散について''.
-	日本ソフトウェア科学会第18回大会論文集, Sep, 2001.
+	ŷ, . ``֥ˡʬˤĤ''.
+	ܥեȥʳز18ʸ, Sep, 2001.
     \bibitem{bib:spin}
 	``Spin - Formal Verification''.
 	http://spinroot.com/spin/whatispin.html
--- a/paper/chapter4.tex	Fri Feb 15 19:59:17 2008 +0900
+++ b/paper/chapter4.tex	Fri Feb 15 22:16:02 2008 +0900
@@ -6,8 +6,8 @@
 
 ޤڤȤ߹֥ŸˤƤ¾θڥġȤӤԤ
 
-ӤоݤȤƤϡSPIN  JavaPathFinder Ѥ롣CbCˤ뵭Ҥȹ碌ơ
-Dining Philosopher ξֶ֤õˤ֤¬ꤷ
+ӤоݤȤƤϡSPIN  Java PathFinder Ѥ롣CbCˤ뵭Ҥȹ碌ơ
+Dining Philosophers Problemξֶ֤õˤ֤¬ꤷ
 
 
 \section{¹ԴĶɾˡ}
@@ -32,22 +32,22 @@
 
 \section{Dining Philosophers ProblemΥ֥Ÿ}
 CbCǼDining Philosophers ProblemФƥ֥ŸŬѤ
-ץ(ůؼ)37Ĥξη¬̤ɽ\ref{tab:dpp_tableau}Τ褦ˤʤä
+ץ(ůؼ)38Ĥξη¬̤ɽ\ref{tab:dpp_tableau}Τ褦ˤʤä
 
-\begin{table}
-    \centering
-    \begin{tabular}{|r|r|r|} \hline
-	ץ & ֿ & ¹Ի() \\ \hline
-	3 & 1,340 & 0.01 \\ \hline
-	4 & 6,115 & 0.08 \\ \hline
-	5 & 38,984 & 0.66 \\ \hline
-	6 & 159,299 & 3.79 \\ \hline
-	7 & 845,529 & 28.59 \\ \hline
-	8 & 3915,727 & 199.80 \\ \hline
-    \end{tabular}
-    \caption{Dining Philosophers ProblemΥ֥Ÿ}
-    \label{tab:dpp_tableau}
-\end{table}
+%\begin{table}
+%    \centering
+%    \begin{tabular}{|r|r|r|} \hline
+%	ץ & ֿ & ¹Ի() \\ \hline
+%	3 & 1,340 & 0.01 \\ \hline
+%	4 & 6,115 & 0.08 \\ \hline
+%	5 & 38,984 & 0.66 \\ \hline
+%	6 & 159,299 & 3.79 \\ \hline
+%	7 & 845,529 & 27.59 \\ \hline
+%	8 & 3915,727 & 199.80 \\ \hline
+%    \end{tabular}
+%    \caption{Dining Philosophers ProblemΥ֥Ÿ}
+%    \label{tab:dpp_tableau}
+%\end{table}
 
 ɽ\ref{tab:dpp_tableau}򸫤ȡץФƾֿ
 ؿäƤ뤳Ȥ狼롣
@@ -62,18 +62,7 @@
 ޤ¾θڥġȤӤԤ
 \\
 
-ץ5Ĥξη¬̤ɽ\ref{tab:ltl_tableau}Τ褦ˤʤä
-
-\begin{table}
-    \centering
-    \begin{tabular}{|r|r|r|} \hline
-	ץ & ֿ & ¹Ի() \\ \hline
-	5 & 38,984 & 0.68 \\ \hline
-	6 & 159,299 & 3.90 \\ \hline
-    \end{tabular}
-    \caption{Dining Philosophers Problem˥ǥåɥåΤȤ߹¹Է}
-    \label{tab:ltl_tableau}
-\end{table}
+ץ58Ĥξη¬̤ɽ\ref{tab:ltl_tableau}Τ褦ˤʤä
 
 ѤΥɥȤȤ߹ǤΥ֥Ÿϡ
 Ȥ߹ΤΤ٤Ƽ¹Ի֤ϤޤѤäƤʤ
@@ -118,18 +107,7 @@
 \ref{src:dpp.prm}SPINˤpan.cʤɤΥե뤬롣
 gccǥѥ뤹뤳Ȥǡ¹ԥե뤬롣
 
-ץ56Ĥξη¬̤ɽ\ref{tab:spin_dpp}Τ褦ˤʤä
-
-\begin{table}
-    \centering
-    \begin{tabular}{|r|r|r|} \hline
-	ץ & ֿ & ¹Ի() \\ \hline
-	5 & 94 & 0.008 \\ \hline
-	6 & 212 & 0.01 \\ \hline
-    \end{tabular}
-    \caption{SPINˤDining Philosophers Problemθڷ}
-    \label{tab:spin_dpp}
-\end{table}
+ץ58Ĥξη¬̤ɽ\ref{tab:spin_dpp}Τ褦ˤʤä
 
 ޤץ5ĤξSPIN줿ڴμ¹Է̤ϰʲΤ褦ˤʤä
 
@@ -162,7 +140,11 @@
 \verb|212 states, stored|줿ˡʾ֤οǤ롣
 
 \subsection{Java PathFinderˤDining Philosophers Problemθ}
-JPFˤϡȤDiningPhil.javaѰդƤΤǤѤ롣
+JPFˤϡȤDiningPhil.java\cite{bib:jpf}ѰդƤΤǤѤ롣
+%\ref{src:dpp.java}Java PathFinderWebڡ\cite{bib:jpf}
+%ѤJavaˤDining Philosophers ProblemεҤǤ롣
+
+\lstinputlisting[caption=JavaˤDining Philosophers Problemε,label=src:dpp.java]{src/DiningPhil.java}
 
 ȤȤƤϡ\verb|javac|ˤJavaΥХȥɤơ
 \verb|jpf|Ǽ¹ԤǤ롣
@@ -170,24 +152,71 @@
 JPFμ¹Է̤ϡֿϤʤ¹Ի֤ΤӤ롣
 ɽ\ref{tab:jpf_dpp}˷¬̤򼨤
 
-\begin{table}
-    \centering
+\begin{table}[htbp]
+    \begin{center}
+    \caption{Dining Philosophers ProblemΥ֥Ÿ}
+    \begin{tabular}{|r|r|r|} \hline
+	ץ & ֿ & ¹Ի() \\ \hline
+	3 & 1,340 & 0.01 \\ \hline
+	4 & 6,115 & 0.08 \\ \hline
+	5 & 38,984 & 0.66 \\ \hline
+	6 & 159,299 & 3.79 \\ \hline
+	7 & 845,529 & 27.59 \\ \hline
+	8 & 3915,727 & 199.80 \\ \hline
+    \end{tabular}
+    \end{center}
+    \label{tab:dpp_tableau}
+%\end{table}
+
+%\begin{table}
+    \begin{center}
+    \caption{Dining Philosophers Problem˥ǥåɥåΤȤ߹¬}
+    \begin{tabular}{|r|r|r|} \hline
+	ץ & ֿ & ¹Ի() \\ \hline
+	5 & 38,984 & 0.68 \\ \hline
+	6 & 159,299 & 3.90 \\ \hline
+	7 & 845,529 & 28.48 \\ \hline
+	8 & 3915,727 & 201.04 \\ \hline
+    \end{tabular}
+    \end{center}
+    \label{tab:ltl_tableau}
+%\end{table}
+
+%\begin{table}
+    \begin{center}
+    \caption{SPINˤDining Philosophers Problemθڤη¬}
+    \begin{tabular}{|r|r|r|} \hline
+	ץ & ֿ & ¹Ի() \\ \hline
+	5 & 94 & 0.008 \\ \hline
+	6 & 212 & 0.01 \\ \hline
+	7 & 494 & 0.03 \\ \hline
+	8 & 212 & 0.04 \\ \hline
+    \end{tabular}
+    \end{center}
+    \label{tab:spin_dpp}
+%\end{table}
+
+%\begin{table}
+    \begin{center}
+    \caption{JPFˤDining Philosophers Problemθڤη¬}
     \begin{tabular}{|r|r|} \hline
 	ץ & ¹Ի() \\ \hline
 	5 & 3.98 \\ \hline
 	6 & 7.33 \\ \hline
+	7 & 26.29 \\ \hline
+	8 & 123.16 \\ \hline
     \end{tabular}
-    \caption{JPFˤDining Philosophers Problemθڷ}
+    \end{center}
     \label{tab:jpf_dpp}
 \end{table}
 
 
+\newpage
 \subsection{ֿõ֤˴ؤͻ}
 
 SPINˤ̤ϡ
 CbCǤθڤ٤ơֿʤ
-ֿʤȤõ֤ûˤĤʤäƤ
-ͤ롣
+ֿʤȤõ֤ûˤĤʤäƤȹͤ롣
 
 PROMELAεҤǤϡPhilosopher ǤξܵҤϡ\verb+do/od+
 ĤƤꡢ\verb+atomic+ʣξ֤ʬ䤵ʤ
@@ -198,11 +227,11 @@
 CbCξϡºݤ˼¹ԲǽʥץǤꡢץϤ
 ΤѿΤ̤Ȥʤ롣CbC Ǥϡ
 ³ɽɥȤؤΥݥ󥿤֤ɽCbC ǤεҤǤϡ
-Philosopher ξ֤5ĤΤǡֿΤؿؿŪ¿ʤäƤ롣
+Philosopher ξ֤8ĤΤǡֿΤؿؿŪ¿ʤäƤ롣
 
-JPFϡJavaThreadȤäҤȤäƤꡢInterleaving Java
-byte code ñ̤ǵ롣󡢴byte code ñ̤Interleaving
-Ĵ٤Ƥ櫓ǤϤʤʣThreadߤ˴Ĥ
+JPFϡJavaΥåɤȤäҤȤäƤꡢInterleaving Java
+Хȥñ̤ǵ롣󡢴ʥХȥñ̤Interleaving
+Ĵ٤Ƥ櫓ǤϤʤʣΥåɤߤ˴Ĥ
 ȹ礻Ĵ٤뤳Ȥˤʤ롣
 
 Java ˤ뵭ҤǤϥץΥ֥ȤΥ󥹥ѿ
@@ -210,10 +239,15 @@
 ˤäɽ롣ˡ{\tt synchronized} ʤɤεҤˤϡ
 бåꡢ¸뤿Υΰ褬ɬפǤ롣
 
-JPF õ֤CbCõ֤٤ΤϡJPFbyte code 
-¹ԤSimulateƤ뤳Ȥ礭ޤ̼ΤȾֿCbC
-뵭Ҥ¿ȿꤵ롣ֿΤ JPF¬ꤹ
-ʤΤǡϿǤ롣
+JPFõ֤ץ6ĤޤǤCbCõ֤٤
+ץ7İʾˤʤCbC®Τϡ
+CbCμˤΤȿ¬롣
+CbCμǤϡBinary TreeХ󥹤Ƥʤᡢ
+õ֤ĹʤäƤȹͤ롣
+%JPF õ֤CbCõ֤٤ΤϡJPFbyte code 
+%¹ԤSimulateƤ뤳Ȥ礭ޤ̼ΤȾֿCbC
+%뵭Ҥ¿ȿꤵ롣ֿΤ JPF¬ꤹ
+%ʤΤǡϿǤ롣
 
 \subsection{CbCˤ븡ˡȷ}
 
@@ -256,13 +290,13 @@
 ñ̤ƱȤݲäƤꡢݲ줿ʬθ
 Ȥ롣
 
-JPFˤ븡ڤϡºݤΥץbyte code levelǼ¹Ԥ
+JPFˤ븡ڤϡºݤΥץХȥɥ٥Ǽ¹Ԥ
 ΤǡΤʸڤǽǤ롣Τ˾ֿ
-¿ʤꡢbyte code simulator ΥХإåɤ⤢äơ
+¿ʤꡢХȥɥߥ졼ΥХإåɤ⤢äơ
 ڤפ֤ȥ꤬礭ʤäƤޤäƤ롣
 
-JPFϥХȥɤˤSimulationǤꡢSPINPROMELA 
-ѥ뤷CΥɤˤSimulatorˤ긡ڤԤäƤ롣
+JPFϥХȥɤˤ륷ߥ졼ǤꡢSPINPROMELA 
+ѥ뤷CΥɤˤ륷ߥ졼ˤ긡ڤԤäƤ롣
 CbC ϡ¾ĤȰۤʤꡢɥʬľܼ¹
 롣ʬ˥顼뤳ȤϤʤΤCbCˤ
 ڤǤȸ롣
@@ -271,7 +305,7 @@
 
 ڤȤˤϡڤ򵭽Ҥɬפ롣
 SPINǤϡLTLPROMLEAѴץबꡢ
-LTLˤꡢ򵭽Ҥ롣ˤ
+LTLˤꡢ򵭽Ҥ롣ˤ
 ֿΤ뤬ѴPROMELAεҤ
 CΥѥ뤵ΤŪ®˥å뤳Ȥ
 ǽǤ롣
@@ -283,17 +317,17 @@
 򥹥åɤǵҤɬפ롣
 
 CbCǤϡεҤCbCΤΤǹԤʸǼ褦
-Tableau ŸƱ(¤줿)ˤǵҤ줿
+֥ŸƱ(¤줿)ǵҤ줿
 ۤȤɥХإåɤʤå뤳Ȥ롣
 ϻΥåΤCbCץȤ
 ѥ뤵Ƥ뤫Ǥ롣
 ϸڷϼΤڤƱǵҤƤ
-ȤǤ롣Tableau ŸԤ{\tt gotoʸ}
+ȤǤ롣֥ŸԤ{\tt gotoʸ}
 Ŭڤ򤹤뤳ȤˤꡢƱ٤Ǥ뤳Ȥ
 Ǥȸ롣
 
 JPFǤϰ츫ƱǸڷϤ򵭽ҤƤ褦˸뤬
-ºݤθоݤJava byte code Ǥꡢϥ󥿥ץ꥿
+ºݤθоݤJava ХȥɤǤꡢϥ󥿥ץ꥿
 Ūˤʤ餶ʤĤޤꡢJPFǤϡڤ٤
 夲ơֿ򾯤ʤȸȤʤ
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/DiningPhil.java	Fri Feb 15 22:16:02 2008 +0900
@@ -0,0 +1,37 @@
+class Fork {
+}
+
+class Philosopher extends Thread {
+  Fork left;
+  Fork right;
+
+  public Philosopher(Fork left, Fork right) {
+    this.left = left;
+    this.right = right;
+    start();
+  }
+
+  public void run() {
+    // think!
+    synchronized (left) {
+      synchronized (right) {
+        // eat!
+      }
+    }
+  }
+}
+
+class DiningPhil {
+  static final int N = 5;
+  public static void main(String[] args) {
+    //Verify.beginAtomic();
+    Fork[] forks = new Fork[N];
+    for (int i = 0; i < N; i++) {
+      forks[i] = new Fork();
+    }
+    for (int i = 0; i < N; i++) {
+      new Philosopher(forks[i], forks[(i + 1) % N]);
+    }
+    //Verify.endAtomic();
+  }
+}