# HG changeset patch # User atsuki # Date 1203081362 -32400 # Node ID 9b2553e32341b2b2688908e2a3f250f8d605ceb6 # Parent fd717f2d19abb2b7ab5ff17376dca2e1b593bbdb *** empty log message *** diff -r fd717f2d19ab -r 9b2553e32341 paper/bibliography.tex --- 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 diff -r fd717f2d19ab -r 9b2553e32341 paper/chapter4.tex --- 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Ǥϡڤ٤ 夲ơֿ򾯤ʤȸȤʤ diff -r fd717f2d19ab -r 9b2553e32341 paper/src/DiningPhil.java --- /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(); + } +}