Mercurial > hg > Papers > 2022 > soto-sigos
changeset 4:7434c0aa1859
WIP SIGの論文ルールに基づいて修正中
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 05 May 2022 17:01:12 +0900 |
| parents | 952d4dbb7c6a |
| children | 6c0b1fcbac2d |
| files | Paper/soto-sigos.aux Paper/soto-sigos.dvi Paper/soto-sigos.fdb_latexmk Paper/soto-sigos.log Paper/soto-sigos.pdf Paper/soto-sigos.synctex.gz Paper/soto-sigos.tex Paper/tex/cbc.tex Paper/tex/cbc_agda.tex Paper/tex/dpp_impl.tex Paper/tex/intro.tex |
| diffstat | 11 files changed, 119 insertions(+), 108 deletions(-) [+] |
line wrap: on
line diff
--- a/Paper/soto-sigos.aux Thu May 05 03:30:26 2022 +0900 +++ b/Paper/soto-sigos.aux Thu May 05 17:01:12 2022 +0900 @@ -33,15 +33,15 @@ \@writefile{lol}{\contentsline {lstlisting}{\numberline {9}{\ignorespaces Gears Agdaでの DPP の step 実行}}{4}{}\protected@file@percent } \newlabel{agda-dpp-lfork}{{10}{4}} \@writefile{lol}{\contentsline {lstlisting}{\numberline {10}{\ignorespaces Gears Agdaでの DPP の左のフォークを取る記述}}{4}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {6}\hskip 1zw{DPPのモデル検査}}{5}{}\protected@file@percent } +\newlabel{agda-dpp-bruteforce}{{11}{5}} +\@writefile{lol}{\contentsline {lstlisting}{\numberline {11}{\ignorespaces Gears Agdaでの DPP の場合を網羅するコード}}{5}{}\protected@file@percent } +\@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{まとめと今後の課題}}{5}{}\protected@file@percent } \citation{*} \bibstyle{ipsjsort} \bibdata{reference} \bibcite{agda-wiki}{1} \bibcite{agda-alpa}{2} -\@writefile{toc}{\contentsline {section}{\numberline {6}\hskip 1zw{DPPのモデル検査}}{5}{}\protected@file@percent } -\newlabel{agda-dpp-bruteforce}{{11}{5}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {11}{\ignorespaces Gears Agdaでの DPP の場合を網羅するコード}}{5}{}\protected@file@percent } -\@writefile{toc}{\contentsline {section}{\numberline {7}\hskip 1zw{まとめと今後の課題}}{5}{}\protected@file@percent } \bibcite{ats2}{3} \bibcite{cbc-gcc}{4} \bibcite{cbc-llvm}{5}
--- a/Paper/soto-sigos.fdb_latexmk Thu May 05 03:30:26 2022 +0900 +++ b/Paper/soto-sigos.fdb_latexmk Thu May 05 17:01:12 2022 +0900 @@ -1,17 +1,17 @@ # Fdb version 3 -["bibtex soto-sigos"] 1651688945 "soto-sigos.aux" "soto-sigos.bbl" "soto-sigos" 1651688946 +["bibtex soto-sigos"] 1651737147 "soto-sigos.aux" "soto-sigos.bbl" "soto-sigos" 1651737624 "./ipsjsort.bst" 1541385384 25930 d27669b348c8e9a5c1cc93168b2b5e89 "" "reference.bib" 1650721531 8174 141307c3535f6e6da421a5ffb91d3db0 "" - "soto-sigos.aux" 1651688946 4473 72b17962261903c19be0d13abefbd397 "latex" + "soto-sigos.aux" 1651737624 4473 0ef7b506ff18fc5dee496af2cfee504c "latex" (generated) "soto-sigos.bbl" "soto-sigos.blg" -["dvipdf"] 1651688946 "soto-sigos.dvi" "soto-sigos.pdf" "soto-sigos" 1651688946 - "soto-sigos.dvi" 1651688946 66764 a04c3839e858c08442a39bf3db610eca "latex" +["dvipdf"] 1651737624 "soto-sigos.dvi" "soto-sigos.pdf" "soto-sigos" 1651737624 + "soto-sigos.dvi" 1651737624 67704 4681641b19a65818d71ff202aabf1980 "latex" (generated) "soto-sigos.pdf" -["latex"] 1651688945 "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" "soto-sigos.dvi" "soto-sigos" 1651688946 - "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" 1651688878 5261 a6bc4ac07bdab035bc9778a1f8fa9812 "" +["latex"] 1651737623 "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" "soto-sigos.dvi" "soto-sigos" 1651737624 + "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" 1651737484 5195 9d9552659d053108c13e2b96a4c1f622 "" "/usr/share/texmf-dist/fonts/map/fontname/texfonts.map" 1647844622 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/share/texmf-dist/fonts/tfm/adobe/times/ptmr7t.tfm" 1647844622 2124 2601a75482e9426d33db523edf23570a "" "/usr/share/texmf-dist/fonts/tfm/jknappen/ec/ecrm0700.tfm" 1647844622 3584 cf973739aac7ab6247f9150296af7954 "" @@ -135,16 +135,16 @@ "fig/cbc_codegear.pdf" 1651684831 30110 abae9d544b613e6b77036cde8327a20f "" "ipsj.cls" 1650809266 142123 ecf81ecc4679baed6ac44a1571336871 "" "ipsjtech.sty" 1541385384 6572 e6269869e3c126f2d200f352d590509a "" - "soto-sigos.aux" 1651688946 4473 72b17962261903c19be0d13abefbd397 "latex" - "soto-sigos.bbl" 1651688945 5285 fc93245f635fcc8bdb721d450a7e0e37 "bibtex soto-sigos" - "soto-sigos.tex" 1651688878 5261 a6bc4ac07bdab035bc9778a1f8fa9812 "" + "soto-sigos.aux" 1651737624 4473 0ef7b506ff18fc5dee496af2cfee504c "latex" + "soto-sigos.bbl" 1651737147 5285 fc93245f635fcc8bdb721d450a7e0e37 "bibtex soto-sigos" + "soto-sigos.tex" 1651737484 5195 9d9552659d053108c13e2b96a4c1f622 "" "src/agda-dpp-impl.agda.replaced" 1651667549 2824 60454fbbf20d18849d1886385e94384b "" "src/agda-dpp-modelcheck.agda.replaced" 1651672378 3179 60cc940175e150991d362fe173027e9b "" "src/agda/cbc-agda.agda.replaced" 1651647471 1143 ab39102eb0f69d3b9f8e4e985a7c1e37 "" - "tex/cbc.tex" 1651688590 2216 c194a2cd2075b1e26ac8b51a728306a4 "" - "tex/cbc_agda.tex" 1651688631 4606 2279e1583a4c51075974ecc2bf95a7d7 "" - "tex/dpp_impl.tex" 1651688944 6361 19e932852f3f0ef1508bfd8f6a9481d8 "" - "tex/intro.tex" 1651570383 3454 c2cd2b67fe52c3a93b6c540ef98ec175 "" + "tex/cbc.tex" 1651737528 2178 b13fd43f52b97ef94deec7bbcb7cc281 "" + "tex/cbc_agda.tex" 1651737623 4587 d8497dfdfab149d9967eae83b11bdfdd "" + "tex/dpp_impl.tex" 1651737146 7062 52e589c98bda93ae7949a3a3de7a981f "" + "tex/intro.tex" 1651737508 3416 1876cbbcc836295829022053b3c430b3 "" (generated) "soto-sigos.aux" "soto-sigos.dvi"
--- a/Paper/soto-sigos.log Thu May 05 03:30:26 2022 +0900 +++ b/Paper/soto-sigos.log Thu May 05 17:01:12 2022 +0900 @@ -1,4 +1,4 @@ -This is e-pTeX, Version 3.141592653-p3.9.0-210218-2.6 (utf8.euc) (TeX Live 2021/Arch Linux) (preloaded format=platex 2022.4.23) 5 MAY 2022 03:29 +This is e-pTeX, Version 3.141592653-p3.9.0-210218-2.6 (utf8.euc) (TeX Live 2021/Arch Linux) (preloaded format=platex 2022.4.23) 5 MAY 2022 17:00 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -3443,9 +3443,9 @@ consecutive: ) [2] LaTeX Font Info: Font shape `JT1/hmc/bx/n' will be -(Font) scaled to size 9.24725pt on input line 61. +(Font) scaled to size 9.24725pt on input line 60. LaTeX Font Info: Font shape `JY1/hmc/bx/n' will be -(Font) scaled to size 9.24725pt on input line 61. +(Font) scaled to size 9.24725pt on input line 60. ) (./tex/dpp_impl.tex File: fig/Dining.pdf Graphic file (type pdf) <fig/Dining.pdf> @@ -3461,7 +3461,7 @@ consecutive: ) (./src/agda-dpp-impl.agda.replaced consecutive: -[4])) (./src/agda-dpp-modelcheck.agda.replaced) (./soto-sigos.bbl +[4])) (./src/agda-dpp-modelcheck.agda.replaced) [5] (./soto-sigos.bbl LaTeX Font Info: Calculating math sizes for size <8.8711> on input line 1. LaTeX Font Info: External font `lmex10' loaded for size (Font) <8.8711> on input line 1. @@ -3473,7 +3473,7 @@ (Font) scaled to size 5.97511pt on input line 1. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be (Font) scaled to size 4.26796pt on input line 1. - [5] + Underfull \hbox (badness 10000) in paragraph at lines 12--14 []\T1/lmr/m/n/8.8711 : ATS-PL-SYS, $\T1/lmtt/m/n/8.8711 http : / / www . ats-[]lang . org/$\T1/lmr/m/n/8.8711 . [] @@ -3599,10 +3599,10 @@ Here is how much of TeX's memory you used: 10946 strings out of 478739 166780 string characters out of 5863952 - 1450538 words of memory out of 5000000 + 1452538 words of memory out of 5000000 29184 multiletter control sequences out of 15000+600000 583961 words of font info for 188 fonts, out of 8000000 for 9000 929 hyphenation exceptions out of 8191 55i,10n,63p,483b,1976s stack positions out of 5000i,500n,10000p,200000b,80000s -Output written on soto-sigos.dvi (6 pages, 66764 bytes). +Output written on soto-sigos.dvi (6 pages, 67704 bytes).
--- a/Paper/soto-sigos.tex Thu May 05 03:30:26 2022 +0900 +++ b/Paper/soto-sigos.tex Thu May 05 17:01:12 2022 +0900 @@ -65,11 +65,11 @@ %概要 \begin{abstract} - 当研究室では Continuation based C (CbC) という言語を用いて、拡張性と信頼性を両立するOSであるGearsOSを開発している。 - CbC とは、 C言語から通常の関数呼び出しではなく、アセンブラでいうjmp命令により関数を遷移する継続を導入した C 言語の下位言語である。 - すでにGearsOSはメタ計算によるモデル検査機構を持っている。 - GearsOSのCodeGear/DataGearはGearsAgdaにより形式証明に向いた形に記述することができる。 - モデル検査機構をGearsAgdaにより記述することでHoare Logic的な逐次実行型のプログラムの証明だけでなく、並行実行を含むプログラムの証明が可能になる。 + 当研究室では Continuation based C (CbC) という言語を用いて,拡張性と信頼性を両立するOSであるGearsOSを開発している. + CbC とは, C言語から通常の関数呼び出しではなく,アセンブラでいうjmp命令により関数を遷移する継続を導入した C 言語の下位言語である. + すでにGearsOSはメタ計算によるモデル検査機構を持っている. + GearsOSのCodeGear/DataGearはGearsAgdaにより形式証明に向いた形に記述することができる. + モデル検査機構をGearsAgdaにより記述することでHoare Logic的な逐次実行型のプログラムの証明だけでなく,並行実行を含むプログラムの証明が可能になる. \end{abstract} \maketitle @@ -81,47 +81,49 @@ \input{tex/cbc_agda.tex}% Gears Agda の記法 loopのやつやる \section{モデル検査} -モデル検査とは、検証手法の一つである。 -他の検証手法として代表的なものとして、定理証明が挙げられる +モデル検査とは,検証手法の一つである. +他の検証手法として代表的なものとして,定理証明が挙げられる. モデル検査はプログラムが入力に対して仕様を満たした動作を -行うことを網羅的に検証することを指す。 +行うことを網羅的に検証することを指す. -モデル検査と定理証明を比較した際に、モデル検査は入力が無限になる -状態爆発が起こり得るという問題がある。 +モデル検査と定理証明を比較した際に,モデル検査は入力が無限になる +状態爆発が起こり得るという問題がある. 定理証明では数学的な証明をするため状態爆発を起こさず検証を行うことが -できるが、専門的な知識が多く難易度が高いという欠点がある。 +できるが,専門的な知識が多く難易度が高いという欠点がある. \input{tex/dpp_impl.tex}% Gears Agda の記法 loopのやつやる \section{DPPのモデル検査} -モデル検査の機能として、入力の網羅が挙げられる。 -今回のDPPの入力の網羅として、哲学者が思考をつづけるのか、食事をはじめようとするのかと -食事中に食事をそのままつづけるのか、思考をするために食事を止めようとするのかが分岐する。 +モデル検査の機能として,入力の網羅が挙げられる. +今回のDPPの入力の網羅として,哲学者が思考をつづけるのか,食事をはじめようとするのかと +食事中に食事をそのままつづけるのか,思考をするために食事を止めようとするのかが分岐する. -そのため、next-codeがthinkingかeatingであるものに対して分岐を網羅する Code \ref{agda-dpp-bruteforce} -を定義した。 +そのため,next-codeがthinkingかeatingであるものに対して分岐を網羅する Code \ref{agda-dpp-bruteforce} +を定義した. \lstinputlisting[caption= Gears Agdaでの DPP の場合を網羅するコード, label=agda-dpp-bruteforce]{src/agda-dpp-modelcheck.agda.replaced} -内部で行っていることとして、その Code Gear 内に存在している next-code が thinking もしくは eatingである場合に -そのプロセスのnext-codeをそのままにするか、それぞれ pickup-rfork か putdown-lfork にする。 -そのため、その部分に対してbit全探索を行い、場合の網羅を行っている。 +内部で行っていることとして,その Code Gear 内に存在している next-code が thinking もしくは eatingである場合に +そのプロセスのnext-codeをそのままにするか,それぞれ pickup-rfork か putdown-lfork にする. +そのため,その部分に対してbit全探索を行い,場合の網羅を行っている. % まとめ \section{まとめと今後の課題} 今回は Agda に CbC の継続の概念を追加した Gears Agda にて -DPPのモデル検査を行おうとした。 -結果として、DPPの実装と入力の網羅までできた。 +DPPのモデル検査を行おうとした. +結果として,DPPの実装と入力の網羅までできた. これからプロセスがすべてほかのプロセスの終了待ちになった場合に -dead lock 状態になっていることを検知できるようにしたい。 -加えて、assertの機能をつけて仕様から外れたことをしていないことを示したい。 +dead lock 状態になっていることを検知できるようにしたい. +加えて,assertの機能をつけて仕様から外れたことをしていないことを示したい. \nocite{*} \bibliographystyle{ipsjsort} \bibliography{reference} -\end{document} \ No newline at end of file +\end{document} + +% . , \ No newline at end of file
--- a/Paper/tex/cbc.tex Thu May 05 03:30:26 2022 +0900 +++ b/Paper/tex/cbc.tex Thu May 05 17:01:12 2022 +0900 @@ -1,34 +1,34 @@ \section{Continuation based C} Continuation based C\cite{kaito-lola} (以下 CbC) は -関数呼び出しの際にjmp命令で遷移をし、環境を持たずに遷移する -ことができるC言語である、 -つまりC言語の下位言語にあたり、よりアセンブラに近い記述を行う +関数呼び出しの際にjmp命令で遷移をし,環境を持たずに遷移する +ことができるC言語である, +つまりC言語の下位言語にあたり,よりアセンブラに近い記述を行う。 -jmp命令であるため関数遷移をし、実行が終了しても +jmp命令であるため関数遷移をし,実行が終了しても もとの関数に戻ることはない。 そのため次に遷移する Code Gear を指定する。 -これは、関数型プログラミングでの末尾関数呼び出しに相当する。 +これは,関数型プログラミングでの末尾関数呼び出しに相当する。 -Code Gear に Deta Gear を与え、それをもとに処理を行い、 -出力として Data Gear を返し、また次の Code Gearに遷移 +Code Gear に Deta Gear を与え,それをもとに処理を行い, +出力として Data Gear を返し,また次の Code Gearに遷移 していく流れとなる。 -CbC では CodeGear を処理の単位、 +CbC では CodeGear を処理の単位, DataGear をデータの単位として記述するプログラミング言語である。 -他のプログラミング言語とは違い、 -Code Gear が 暗黙の環境を持たず、受け取った Data Gear のみを -もとに処理をすること、 -さらに Code Gear 単位で処理が完結していることから、 +他のプログラミング言語とは違い, +Code Gear が 暗黙の環境を持たず,受け取った Data Gear のみを +もとに処理をすること, +さらに Code Gear 単位で処理が完結していることから, 検証に適したプログラミング言語であると言える。 -また、プログラムを記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、資源管理等を記述しなければならない処理が存在する。 +また,プログラムを記述する際は,ノーマルレベルの計算の他に,メモリ管理,スレッド管理,資源管理等を記述しなければならない処理が存在する。 これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。 -メタ計算は OS の機能を通して処理することが多く、信頼性の高い記述が求められる。 -そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している +メタ計算は OS の機能を通して処理することが多く,信頼性の高い記述が求められる。 +そのため, CbC ではメタ計算を分離するために Meta CodeGear, Meta DataGear を定義している。 -Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。 +Meta CodeGear は CbC 上でのメタ計算で,通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。 図 \ref{fig:meta-cgdg} のように CodeGear を実行する前後や DataGear の大枠として Meta Gear が存在している。 \begin{figure}[htpb]
--- a/Paper/tex/cbc_agda.tex Thu May 05 03:30:26 2022 +0900 +++ b/Paper/tex/cbc_agda.tex Thu May 05 17:01:12 2022 +0900 @@ -1,6 +1,6 @@ \section{GearsAgda 形式で書く agda} CbC の継続の概念を取り入れた Agda の記法を説明する。 -Agdaでは関数の再帰呼び出しが可能であるが、CbCでは値が 帰って来ない。そのためAgda +Agda では関数の再帰呼び出しが可能であるが, CbC では値が 帰って来ない。そのため Agda で実装を行う際には再帰呼び出しを行わないようにする。 以下で Gears Agda の記述方法を足し算を行うプログラムを用いて説明する。 @@ -14,62 +14,61 @@ \lstinputlisting[caption= Agdaでの CodeGear の初期化, label=agda-exec-cg, firstline=24]{src/agda/cbc-agda.agda.replaced} Code \ref{agda-dg}が Data Gear の定義をしている。 -今回は足し算を実装するので、varx に vary を足すことを考える。 +今回は足し算を実装するので,varx に vary を足すことを考える。 そのためそれらが2つの自然数を持つようにしている。 Code \ref{agda-cg}では Code Gear の定義になる。 -最初に Data Gear となる env を受け取ったあと、そのまま次の関数に遷移させている。 +最初に Data Gear となる env を受け取ったあと,そのまま次の関数に遷移させている。 -Agda の記述は curry-Howard 対応になっていて、 -最初に関数名のあとに:(コロン)の後ろに命題を記述し、 -そのあとに関数名のあとに引数を書き、=(イコール)の後ろに定義を記述しています。 +Agda の記述は Curry-Howard 対応になっていて, +最初に関数名のあとに :(コロン)の後ろに命題を記述し, +そのあとに関数名のあとに引数を書き, =(イコール)の後ろに定義を記述しています。 Gears Agda での Code Gear の命題は必ず (Env $\rightarrow$ t) $\rightarrow$ t で 終了するようになっている。この (Env $\rightarrow$ t) は引数で受け取る型で Env を 受け取ってtを返すという意味になる。これが Code Gear を実行したあとの末尾関数呼び出しを -行う次の Code Gear となる。 最後にtを返すとなっているのは、これ自体が Code Gear であることを +行う次の Code Gear となる。 最後にtを返すとなっているのは,これ自体が Code Gear であることを 示している。 受け取ったあとに別の関数に再度渡している。 -これは後述するが、Agdaの繰り返し処理を行う際に停止性を +これは後述するが, Agda の繰り返し処理を行う際に停止性を 見失うために減少列を引数に取っている。 -内部の処理はreducerを減らしながらvarxを増やすことで -varyの値をvarxに与えていくことで足し算を定義している。 +内部の処理は reducer を減らしながら varx を増やすことで +vary の値を varx に与えていくことで足し算を定義している。 基本的に繰り返し実行するコードを実装する場合には -実行時に減少し、その関数がいずれ停止することを示す -reducerを含めるようにしている。 +実行時に減少し,その関数がいずれ停止することを示す reducer を含めるようにしている。 reducerを含めなかった際の Code Gear を Code \ref{agda-not-cg}に示す。 -agdaではパターンマッチを行うことで場合分けを考えることができるが、 +agdaではパターンマッチを行うことで場合分けを考えることができるが, 受け取った Code Gear であるenvを with を使用してパターンマッチを試みている。 -パターンマッチ自体は可能だが、この方法だとAgdaが関数が停止することを認識できない。 -そのため、\{-$\#$ TERMINATING $\#$-\} を関数定義の前にアノテーションし +パターンマッチ自体は可能だが,この方法だとAgdaが関数が停止することを認識できない。 +そのため,\{-$\#$ TERMINATING $\#$-\} を関数定義の前にアノテーションし この関数が停止することを記述してコンパイルが通るようにしている。 Code \ref{agda-exec-cg} は受け取った引数で Data Gear を初期化して それを Code Gear に与えることで実行を行っている。 今回の例では 引数から Data Gear を作成するのは -複雑ではないため、一度で Data Gear を作成してそれを Code Gear に渡している +複雑ではないため,一度で Data Gear を作成してそれを Code Gear に渡している 引数から Data Gear を作成するのが複雑な場合は一度 入力から Data Gear を作成する Code Gear を用いる。 -加えて、実行なので命題の部分の最後が Env になっている。 +加えて,実行なので命題の部分の最後が Env になっている。 \subsection{agda による Meta Gears} -通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。 +通常の Meta Gears はノーマルレベルの CodeGear, DataGear では扱えないメタレベルの計算を扱う単位である。 今回はモデル検査を行う際に使用する \begin{itemize} \item Meta DataGear \mbox{}\\ Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる。 - 通常の Data Gear を wraping している。今回はこれを用いることで、モデル検査の状態を保存する + 通常の Data Gear を wraping している。今回はこれを用いることで,モデル検査の状態を保存する \item Meta CodeGear\mbox{}\\ Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返 - す CodeGear である。今回はここでモデル検査を行う。 + す CodeGear である。今回はここでモデル検査を行う \end{itemize}
--- a/Paper/tex/dpp_impl.tex Thu May 05 03:30:26 2022 +0900 +++ b/Paper/tex/dpp_impl.tex Thu May 05 17:01:12 2022 +0900 @@ -1,5 +1,5 @@ \section{Dining Philosophers Problem} -今回はモデル検査を行う対象として Dining Philosophers Problem +今回はモデル検査を行う対象として Dining Philosophers Problem (以下DPP) を用いることとした。 DPPとは資源共有問題であり、モデル検査をする際に挙げられる代表的な問題 である。 @@ -23,7 +23,7 @@ \item 食事するためには2本のフォークを取る必要があり、これを同時に取ることはできない \item しばらくの食事から思考に戻る際には両手に持ったフォークをテーブルに置く \item 最後に取ったフォークから先に置くため、左のフォークから置き、右のフォークを置く - \item 哲学者はこの食事と思考を繰り返し行う。哲学者同士が会話することはない + \item 哲学者はこの食事と思考を繰り返し行い、哲学者同士が会話することはない \end{itemize} つまり、哲学者は以下のようなフローを独立して並列に実行することとなる。 @@ -72,7 +72,7 @@ tableはテーブルに置いてあるフォークの状態のことで、 pidが1の人の右側にあるフォークが List の最初にあり、 -pidが1の人の左側にあるフォーク、つまりpidが2の人の右側にあるフォークが +pidが1の人の左側にあるフォーク、すなわちpidが2の人の右側にあるフォークが その次のListに格納されていくようになっている。 また、自然数の List になっているが、 その場所のフォークがテーブルの上にある場合は自然数の0が、 @@ -95,6 +95,16 @@ Code \ref{agda-dpp-lfork}がstep実行をした際に哲学者が左側のフォークを取る記述になる。 +左側のフォークを取る際には table の index は pid の次の値になっている。 +図 \ref{fig:DPP} を見ると直感的に理解ができる。 + +最後の哲学者は一番最初のフォークを参照する必要がある。 +フォークの状態を確認し、値が0である場合はフォークがテーブルの上にあるので +それを自分のpidに書き換えleft-handをtrueに書き換えてフォークを手に持つ +フォークの状態が0以外、すなわち他の哲学者がその場所のフォークを取得している場合は +状態を変化させずに処理を続ける。 +このように左のフォークを取る記述をした。 + 右側のフォークを取る場合は引数の部分を1足さずにそのまま受け取る。 比較するべきtableのListと哲学者のListは一致しているため、put\_lforkのように最後の哲学者が 最初のフォークを参照することもない。
--- a/Paper/tex/intro.tex Thu May 05 03:30:26 2022 +0900 +++ b/Paper/tex/intro.tex Thu May 05 17:01:12 2022 +0900 @@ -1,46 +1,46 @@ \section{Gears Agda でのモデル検査} \pagenumbering{arabic} -思い思いにプログラムを書くと、冗長なコードができてしまい、 +思い思いにプログラムを書くと,冗長なコードができてしまい, 実行時間も遅い場合がある。 この場合にコードに対してアルゴリズムを適応すると実行が最適化され -実行時間が減り、かつ第三者がコードを読んだ際にロジックが統一されているため理解が容易くなる。 -つまり、一般的に良いコードが作成できる。 +実行時間が減り,かつ第三者がコードを読んだ際にロジックが統一されているため理解が容易くなる。 +つまり,一般的に良いコードが作成できる。 -しかし、世の中にはすでに大量のアルゴリズムが存在するため、 -これを一人のプログラマーが全て覚え、適応できる場面を思いつくというのは不可能に近い。 +しかし,世の中にはすでに大量のアルゴリズムが存在するため, +これを一人のプログラマーが全て覚え,適応できる場面を思いつくというのは不可能に近い。 その道に詳しい人が複数人いる場面というのも稀だと考えられる。 -そのため、人が書いたコードに対してアルゴリズムを使用するコードに変換できるようにしたい。 +そのため,人が書いたコードに対してアルゴリズムを使用するコードに変換できるようにしたい。 -この際、アルゴリズム適応前後で処理が変わっていないか検証するのは普通のプログラミング言語では難しい。 -一般的なプログラミング言語では、関数の遷移が自由であることから、関数遷移などで発生した +この際,アルゴリズム適応前後で処理が変わっていないか検証するのは普通のプログラミング言語では難しい。 +一般的なプログラミング言語では,関数の遷移が自由であることから,関数遷移などで発生した 暗黙の環境が存在するためである。 -この問題を解決するため、Gears Agda を用いる。 +この問題を解決するため,Gears Agda を用いる。 -Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を取り入れた記法で書かれた Agda のこと +Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を取り入れた記法で書かれた Agda のことで, 通常のプログラミング言語では関数を実行する際にはメインルーチンからサブルーチンに遷移する。 -この際メインルーチンで使用していた変数などの環境はスタックされ、サブルーチンが終了した際にメインルーチンに戻り、 +この際メインルーチンで使用していた変数などの環境はスタックされ,サブルーチンが終了した際にメインルーチンに戻り, スタックしていた変数をもとに戻す流れとなる。 -CbCの場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ、スタックを持たず環境を保持しない。 +CbCの場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ,スタックを持たず環境を保持しない。 更に遷移後にメインルーチンに戻ることもない。 -つまり関数の実行では暗黙な環境が存在せず、関数が受け取った引数のみを使用する。 -これにより限定的な実行条件を作成でき、検証がしやすくなる。 +つまり関数の実行では暗黙な環境が存在せず,関数が受け取った引数のみを使用する。 +これにより限定的な実行条件を作成でき,検証がしやすくなる。 -現在、アルゴリズムの適応可否は以下の方法を考えている。 +現在,アルゴリズムの適応可否は以下の方法を考えている。 -あらかじめ、アルゴリズムの実装と検証をおこなったアルゴリズムSetsを用意しておく +あらかじめ,アルゴリズムの実装と検証をおこなったアルゴリズムSetsを用意しておく。 -書いたコードが事前に定義していたアルゴリズムの仕様を満たしているかを検証していき、 +書いたコードが事前に定義していたアルゴリズムの仕様を満たしているかを検証していき, 満たしているコードがあった場合にそのコードを事前に定義してあるアルゴリズムに入れ替える方針を考えている。 -この際、実装が仕様を満たしているか検証する手法には、定理証明やモデル検査などが挙げられる。 +この際,実装が仕様を満たしているか検証する手法には,定理証明やモデル検査などが挙げられる。 -アルゴリズムの入れ替え可否判定には Gears Agda でモデル検査を行い、アルゴリズムの仕様がコードに適応できるか検証するのが -妥当だと考えている -思い思いに書いたコードに対して定理証明を行うのはコストが高く、適応するものの内部動作が一致しない場合定理証明を行っても使えないためである。 +アルゴリズムの入れ替え可否判定には Gears Agda でモデル検査を行い, +アルゴリズムの仕様がコードに適応できるか検証するのが妥当だと考えている。 +思い思いに書いたコードに対して定理証明を行うのはコストが高く,適応するものの内部動作が一致しない場合定理証明を行っても使えないためである。 本論文では Gears Agda でのモデル検査の先駆けとして Dining philosophers problem (DPP) のモデル検査を行う。