# HG changeset patch # User soto # Date 1651739886 -32400 # Node ID 6c0b1fcbac2d8e8081eaa6c095e7aa573c439732 # Parent 7434c0aa1859b65dfa0feb3c3cf47e24b828c54d FIX SIGの論文ルールに基づいて修正 diff -r 7434c0aa1859 -r 6c0b1fcbac2d Paper/soto-sigos.dvi Binary file Paper/soto-sigos.dvi has changed diff -r 7434c0aa1859 -r 6c0b1fcbac2d Paper/soto-sigos.fdb_latexmk --- a/Paper/soto-sigos.fdb_latexmk Thu May 05 17:01:12 2022 +0900 +++ b/Paper/soto-sigos.fdb_latexmk Thu May 05 17:38:06 2022 +0900 @@ -1,17 +1,17 @@ # Fdb version 3 -["bibtex soto-sigos"] 1651737147 "soto-sigos.aux" "soto-sigos.bbl" "soto-sigos" 1651737624 +["bibtex soto-sigos"] 1651739057 "soto-sigos.aux" "soto-sigos.bbl" "soto-sigos" 1651739709 "./ipsjsort.bst" 1541385384 25930 d27669b348c8e9a5c1cc93168b2b5e89 "" "reference.bib" 1650721531 8174 141307c3535f6e6da421a5ffb91d3db0 "" - "soto-sigos.aux" 1651737624 4473 0ef7b506ff18fc5dee496af2cfee504c "latex" + "soto-sigos.aux" 1651739709 4473 0ef7b506ff18fc5dee496af2cfee504c "latex" (generated) "soto-sigos.bbl" "soto-sigos.blg" -["dvipdf"] 1651737624 "soto-sigos.dvi" "soto-sigos.pdf" "soto-sigos" 1651737624 - "soto-sigos.dvi" 1651737624 67704 4681641b19a65818d71ff202aabf1980 "latex" +["dvipdf"] 1651739709 "soto-sigos.dvi" "soto-sigos.pdf" "soto-sigos" 1651739709 + "soto-sigos.dvi" 1651739709 67908 9ea91f7e3c11987d76a61d6680d451d3 "latex" (generated) "soto-sigos.pdf" -["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 "" +["latex"] 1651739708 "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" "soto-sigos.dvi" "soto-sigos" 1651739709 + "/home/soto/lab/soto-sigos/Paper/soto-sigos.tex" 1651739708 5269 9fb5ed6f6ebe4ffdc43f6549ce2db125 "" "/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" 1651737624 4473 0ef7b506ff18fc5dee496af2cfee504c "latex" - "soto-sigos.bbl" 1651737147 5285 fc93245f635fcc8bdb721d450a7e0e37 "bibtex soto-sigos" - "soto-sigos.tex" 1651737484 5195 9d9552659d053108c13e2b96a4c1f622 "" + "soto-sigos.aux" 1651739709 4473 0ef7b506ff18fc5dee496af2cfee504c "latex" + "soto-sigos.bbl" 1651739057 5285 fc93245f635fcc8bdb721d450a7e0e37 "bibtex soto-sigos" + "soto-sigos.tex" 1651739708 5269 9fb5ed6f6ebe4ffdc43f6549ce2db125 "" "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" 1651737528 2178 b13fd43f52b97ef94deec7bbcb7cc281 "" - "tex/cbc_agda.tex" 1651737623 4587 d8497dfdfab149d9967eae83b11bdfdd "" - "tex/dpp_impl.tex" 1651737146 7062 52e589c98bda93ae7949a3a3de7a981f "" - "tex/intro.tex" 1651737508 3416 1876cbbcc836295829022053b3c430b3 "" + "tex/cbc.tex" 1651739682 2226 dc5c1d561f9ae2126a042ffb96b67360 "" + "tex/cbc_agda.tex" 1651739675 4619 23680a51e50a47a36d558165de0af034 "" + "tex/dpp_impl.tex" 1651739658 7074 a37d202fec1e5b5a34e9f7d0337bda56 "" + "tex/intro.tex" 1651739694 3474 25f20157d5beaa1ef82406eb9fdebc37 "" (generated) "soto-sigos.aux" "soto-sigos.dvi" diff -r 7434c0aa1859 -r 6c0b1fcbac2d Paper/soto-sigos.log --- a/Paper/soto-sigos.log Thu May 05 17:01:12 2022 +0900 +++ b/Paper/soto-sigos.log Thu May 05 17:38:06 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 17:00 +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:35 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -3396,33 +3396,33 @@ (Font) scaled to size 11.38124pt on input line 1. ) (./tex/cbc.tex LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 7.53018pt on input line 11. +(Font) scaled to size 7.53018pt on input line 7. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 7.53018pt on input line 11. +(Font) scaled to size 7.53018pt on input line 7. LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 6.84561pt on input line 11. +(Font) scaled to size 6.84561pt on input line 7. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 6.84561pt on input line 11. +(Font) scaled to size 6.84561pt on input line 7. (I search kanjifont definition file: . . ) (I search font definition file: . . . . . . . ) -LaTeX Font Info: Trying to load font information for OMS+txsy on input line 11. +LaTeX Font Info: Trying to load font information for OMS+txsy on input line 7. (/usr/share/texmf-dist/tex/latex/txfonts/omstxsy.fd File: omstxsy.fd 2000/12/15 v3.1 ) -LaTeX Font Info: Trying to load font information for T1+txsy on input line 11. -LaTeX Font Info: No file T1txsy.fd. on input line 11. +LaTeX Font Info: Trying to load font information for T1+txsy on input line 7. +LaTeX Font Info: No file T1txsy.fd. on input line 7. LaTeX Font Warning: Font shape `T1/txsy/m/n' undefined -(Font) using `T1/cmr/m/n' instead on input line 11. - -LaTeX Font Info: Trying to load font information for OT1+ptm on input line 11. +(Font) using `T1/cmr/m/n' instead on input line 7. + +LaTeX Font Info: Trying to load font information for OT1+ptm on input line 7. (/usr/share/texmf-dist/tex/latex/psnfss/ot1ptm.fd File: ot1ptm.fd 2001/06/04 font definitions for OT1/ptm. ) LaTeX Font Info: Font shape `JT1/hmc/m/n' will be -(Font) scaled to size 8.8993pt on input line 11. +(Font) scaled to size 8.8993pt on input line 7. LaTeX Font Info: Font shape `JY1/hmc/m/n' will be -(Font) scaled to size 8.8993pt on input line 11. +(Font) scaled to size 8.8993pt on input line 7. [1 @@ -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 60. +(Font) scaled to size 9.24725pt on input line 61. LaTeX Font Info: Font shape `JY1/hmc/bx/n' will be -(Font) scaled to size 9.24725pt on input line 60. +(Font) scaled to size 9.24725pt on input line 61. ) (./tex/dpp_impl.tex File: fig/Dining.pdf Graphic file (type pdf) @@ -3603,6 +3603,6 @@ 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, 67704 bytes). + 55i,11n,63p,483b,1976s stack positions out of 5000i,500n,10000p,200000b,80000s + +Output written on soto-sigos.dvi (6 pages, 67908 bytes). diff -r 7434c0aa1859 -r 6c0b1fcbac2d Paper/soto-sigos.pdf Binary file Paper/soto-sigos.pdf has changed diff -r 7434c0aa1859 -r 6c0b1fcbac2d Paper/soto-sigos.synctex.gz Binary file Paper/soto-sigos.synctex.gz has changed diff -r 7434c0aa1859 -r 6c0b1fcbac2d Paper/soto-sigos.tex --- a/Paper/soto-sigos.tex Thu May 05 17:01:12 2022 +0900 +++ b/Paper/soto-sigos.tex Thu May 05 17:38:06 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,49 +81,47 @@ \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 diff -r 7434c0aa1859 -r 6c0b1fcbac2d Paper/tex/cbc.tex --- a/Paper/tex/cbc.tex Thu May 05 17:01:12 2022 +0900 +++ b/Paper/tex/cbc.tex Thu May 05 17:38:06 2022 +0900 @@ -1,35 +1,35 @@ \section{Continuation based C} -Continuation based C\cite{kaito-lola} (以下 CbC) は -関数呼び出しの際にjmp命令で遷移をし,環境を持たずに遷移する -ことができるC言語である, -つまりC言語の下位言語にあたり,よりアセンブラに近い記述を行う。 +Continuation based C\cite{kaito-lola} （以下 CbC） は +関数呼び出しの際にjmp命令で遷移をし，環境を持たずに遷移する +ことができるC言語である， +つまりC言語の下位言語にあたり，よりアセンブラに近い記述を行う． -jmp命令であるため関数遷移をし,実行が終了しても -もとの関数に戻ることはない。 -そのため次に遷移する Code Gear を指定する。 -これは,関数型プログラミングでの末尾関数呼び出しに相当する。 +jmp命令であるため関数遷移をし，実行が終了しても +もとの関数に戻ることはない． +そのため次に遷移する Code Gear を指定する． +これは，関数型プログラミングでの末尾関数呼び出しに相当する． -Code Gear に Deta Gear を与え,それをもとに処理を行い, -出力として Data Gear を返し,また次の Code Gearに遷移 -していく流れとなる。 +Code Gear に Deta Gear を与え，それをもとに処理を行い， +出力として Data Gear を返し，また次の Code Gearに遷移 +していく流れとなる． -CbC では CodeGear を処理の単位, -DataGear をデータの単位として記述するプログラミング言語である。 +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 を実行する際に必要なメタ計算を分離するための単位である。 -図 \ref{fig:meta-cgdg} のように CodeGear を実行する前後や DataGear の大枠として Meta Gear が存在している。 +Meta CodeGear は CbC 上でのメタ計算で，通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である． +図 \ref{fig:meta-cgdg} のように CodeGear を実行する前後や DataGear の大枠として Meta Gear が存在している． \begin{figure}[htpb] \begin{center} diff -r 7434c0aa1859 -r 6c0b1fcbac2d Paper/tex/cbc_agda.tex --- a/Paper/tex/cbc_agda.tex Thu May 05 17:01:12 2022 +0900 +++ b/Paper/tex/cbc_agda.tex Thu May 05 17:38:06 2022 +0900 @@ -1,9 +1,9 @@ \section{GearsAgda 形式で書く agda} -CbC の継続の概念を取り入れた Agda の記法を説明する。 -Agda では関数の再帰呼び出しが可能であるが, CbC では値が 帰って来ない。そのため Agda -で実装を行う際には再帰呼び出しを行わないようにする。 +CbC の継続の概念を取り入れた Agda の記法を説明する． +Agdaでは関数の再帰呼び出しが可能であるが，CbCでは値が 帰って来ない．そのためAgda +で実装を行う際には再帰呼び出しを行わないようにする． -以下で Gears Agda の記述方法を足し算を行うプログラムを用いて説明する。 +以下で Gears Agda の記述方法を足し算を行うプログラムを用いて説明する． \lstinputlisting[caption= Agdaでの Data Gear の定義, label=agda-dg, firstline=6, lastline=11]{src/agda/cbc-agda.agda.replaced} @@ -13,62 +13,63 @@ \lstinputlisting[caption= Agdaでの CodeGear の初期化, label=agda-exec-cg, firstline=24]{src/agda/cbc-agda.agda.replaced} -Code \ref{agda-dg}が Data Gear の定義をしている。 -今回は足し算を実装するので,varx に vary を足すことを考える。 -そのためそれらが2つの自然数を持つようにしている。 +Code \ref{agda-dg}が Data Gear の定義をしている． +今回は足し算を実装するので，varx に vary を足すことを考える． +そのためそれらが2つの自然数を持つようにしている． -Code \ref{agda-cg}では Code Gear の定義になる。 -最初に Data Gear となる env を受け取ったあと,そのまま次の関数に遷移させている。 +Code \ref{agda-cg}では Code Gear の定義になる． +最初に 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 であることを -示している。 +Gears Agda での Code Gear の命題は必ず （Env $\rightarrow$ t） $\rightarrow$ t で +終了するようになっている．この （Env $\rightarrow$ t） は引数で受け取る型で Env を +受け取って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ではパターンマッチを行うことで場合分けを考えることができるが, -受け取った Code Gear であるenvを with を使用してパターンマッチを試みている。 -パターンマッチ自体は可能だが,この方法だとAgdaが関数が停止することを認識できない。 -そのため,\{-$\#$ TERMINATING $\#$-\} を関数定義の前にアノテーションし -この関数が停止することを記述してコンパイルが通るようにしている。 +reducerを含めなかった際の Code Gear を Code \ref{agda-not-cg}に示す． +agdaではパターンマッチを行うことで場合分けを考えることができるが， +受け取った Code Gear であるenvを with を使用してパターンマッチを試みている． +パターンマッチ自体は可能だが，この方法だとAgdaが関数が停止することを認識できない． +そのため，\{-$\#$ TERMINATING $\#$-\} を関数定義の前にアノテーションし +この関数が停止することを記述してコンパイルが通るようにしている． Code \ref{agda-exec-cg} は受け取った引数で Data Gear を初期化して -それを Code Gear に与えることで実行を行っている。 +それを Code Gear に与えることで実行を行っている． 今回の例では 引数から Data Gear を作成するのは -複雑ではないため,一度で Data Gear を作成してそれを Code Gear に渡している +複雑ではないため，一度で Data Gear を作成してそれを Code Gear に渡している 引数から Data Gear を作成するのが複雑な場合は一度 入力から -Data Gear を作成する Code 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 している。今回はこれを用いることで,モデル検査の状態を保存する + Agda 上で Meta DataGear を持つことでデータ構造自体が関係を持つデータを作ることができる． + 通常の Data Gear を wraping している．今回はこれを用いることで，モデル検査の状態を保存する \item Meta CodeGear\mbox{}\\ Meta CodeGear は 通常の CodeGear では扱えないメタレベルの計算を扱う CodeGear - である。Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返 - す CodeGear である。今回はここでモデル検査を行う + である．Agda での Meta CodeGear は Meta DataGear を引数に取りそれらの関係を返 + す CodeGear である．今回はここでモデル検査を行う \end{itemize} diff -r 7434c0aa1859 -r 6c0b1fcbac2d Paper/tex/dpp_impl.tex --- a/Paper/tex/dpp_impl.tex Thu May 05 17:01:12 2022 +0900 +++ b/Paper/tex/dpp_impl.tex Thu May 05 17:38:06 2022 +0900 @@ -1,8 +1,8 @@ \section{Dining Philosophers Problem} -今回はモデル検査を行う対象として Dining Philosophers Problem (以下DPP) -を用いることとした。 -DPPとは資源共有問題であり、モデル検査をする際に挙げられる代表的な問題 -である。 +今回はモデル検査を行う対象として Dining Philosophers Problem （以下DPP） +を用いることとした． +DPPとは資源共有問題であり，モデル検査をする際に挙げられる代表的な問題 +である． \begin{figure}[htpb] \begin{center} @@ -12,40 +12,40 @@ \label{fig:DPP} \end{figure} -問題のストーリーをまとめると以下のようになる。 +問題のストーリーをまとめると以下のようになる． \begin{itemize} - \item 哲学者がN人円卓についている(Nは2以上の自然数) + \item 哲学者がN人円卓についている（Nは2以上の自然数） \item 哲学者の目の前には食べ物が用意されている \item 哲学者の人数と同じだけのフォークがそれぞれ哲学者の間に置かれている - \item 哲学者はしばらく思考したのち、しばらく食事する動作を繰り返しおこなう + \item 哲学者はしばらく思考したのち，しばらく食事する動作を繰り返しおこなう \item 思考から食事をする際には右のフォークを取ったのちに左のフォークを取ることで食事を始める - \item 食事するためには2本のフォークを取る必要があり、これを同時に取ることはできない + \item 食事するためには2本のフォークを取る必要があり，これを同時に取ることはできない \item しばらくの食事から思考に戻る際には両手に持ったフォークをテーブルに置く - \item 最後に取ったフォークから先に置くため、左のフォークから置き、右のフォークを置く - \item 哲学者はこの食事と思考を繰り返し行い、哲学者同士が会話することはない + \item 最後に取ったフォークから先に置くため，左のフォークから置き，右のフォークを置く + \item 哲学者はこの食事と思考を繰り返し行い，哲学者同士が会話することはない \end{itemize} -つまり、哲学者は以下のようなフローを独立して並列に実行することとなる。 +つまり，哲学者は以下のようなフローを独立して並列に実行することとなる． \begin{enumerate} \item しばらくの間思考を行う \item 食事をするために右のフォークを取る - \item 右のフォークを取ったら、次は左のフォークを取る - \item 両方のフォークを取ったら、しばらく食事をする + \item 右のフォークを取ったら，次は左のフォークを取る + \item 両方のフォークを取ったら，しばらく食事をする \item 思考に戻るために左手に持っているフォークをテーブルに置く \item 左手のフォークを置いたあとは右のフォークをテーブルに置く - \item しばらくの間思考する。つまり最初に戻る + \item しばらくの間思考する．つまり最初に戻る \end{enumerate} -この際、すべての哲学者が同時に右のフォークを取った場合のことを考える。 -すべての哲学者はフォークを持っている。次に哲学者は左のフォークを取ろうと -する。しかしフォークは哲学者の人数と同じ数だけ存在しているため、 -テーブルの上にフォークはすでにひとつも存在しない。 +この際，すべての哲学者が同時に右のフォークを取った場合のことを考える． +すべての哲学者はフォークを持っている．次に哲学者は左のフォークを取ろうと +する．しかしフォークは哲学者の人数と同じ数だけ存在しているため， +テーブルの上にフォークはすでにひとつも存在しない． すべての哲学者は左のフォークを取ろうとするが -誰も右のフォークを置くことがないため、すべての哲学者の動作がこの状態で止まる。(dead lock) +誰も右のフォークを置くことがないため，すべての哲学者の動作がこの状態で止まる．（dead lock） -これが起こることを Gears Agda で検出したい。 +これが起こることを Gears Agda で検出したい． \subsection{Gears Agda によるDPPの実装} \lstinputlisting[caption= Gears Agdaでの DPP の 哲学者の状態 , label=agda-dpp-state, lastline=7]{src/agda-dpp-impl.agda.replaced} @@ -55,61 +55,61 @@ \lstinputlisting[caption= Gears Agdaでの DPP の Data Gear , label=agda-dpp-dg, firstline=17, lastline=21]{src/agda-dpp-impl.agda.replaced} Code \ref{agda-dpp-state}は -前述した哲学者の状態を書き記して、哲学者が今行おうとしている動作を網羅している。 +前述した哲学者の状態を書き記して，哲学者が今行おうとしている動作を網羅している． Code \ref{agda-dpp-process}は -哲学者一人ずつの環境を持っている。 -pidはその哲学者がどこに座っているかの識別子で、 -right / left hand はフォークを手に持っているかを格納している。 -next-codeは次に行う動作を格納している。 +哲学者一人ずつの環境を持っている． +pidはその哲学者がどこに座っているかの識別子で， +right / left hand はフォークを手に持っているかを格納している． +next-codeは次に行う動作を格納している． -Code \ref{agda-dpp-dg} が Data Gear になる。 +Code \ref{agda-dpp-dg} が Data Gear になる． -phは前もって定義した一人の哲学者のプロセスの List になる。 -List になっている理由は、哲学者が複数人いるためである。 +phは前もって定義した一人の哲学者のプロセスの List になる． +List になっている理由は，哲学者が複数人いるためである． -そのため実行時にListから一人ずつ取り出して実行をしていく。 +そのため実行時にListから一人ずつ取り出して実行をしていく． -tableはテーブルに置いてあるフォークの状態のことで、 -pidが1の人の右側にあるフォークが List の最初にあり、 -pidが1の人の左側にあるフォーク、すなわちpidが2の人の右側にあるフォークが -その次のListに格納されていくようになっている。 -また、自然数の List になっているが、 -その場所のフォークがテーブルの上にある場合は自然数の0が、 -誰かが所持している場合はその人のpidが格納されるようになっている。 +tableはテーブルに置いてあるフォークの状態のことで， +pidが1の人の右側にあるフォークが List の最初にあり， +pidが1の人の左側にあるフォーク，すなわちpidが2の人の右側にあるフォークが +その次のListに格納されていくようになっている． +また，自然数の List になっているが， +その場所のフォークがテーブルの上にある場合は自然数の0が， +誰かが所持している場合はその人のpidが格納されるようになっている． \lstinputlisting[caption= Gears Agdaでの DPP の Data Gear のinit, label=agda-dpp-init, firstline=23, lastline=30]{src/agda-dpp-impl.agda.replaced} -Code \ref{agda-dpp-init}が入力から Data Gear を作成する Code Gear になる。 -ここでは哲学者の人数を自然数で受け取り、人数分の List Phi と table を一つづつ作成し env を作成している。 -また、最初の哲学者の状態は思考することであるため、next-code には C\_thinking を格納している。 +Code \ref{agda-dpp-init}が入力から Data Gear を作成する Code Gear になる． +ここでは哲学者の人数を自然数で受け取り，人数分の List Phi と table を一つづつ作成し env を作成している． +また，最初の哲学者の状態は思考することであるため，next-code には C\_thinking を格納している． \lstinputlisting[caption= Gears Agdaでの DPP の step 実行, label=agda-dpp-step, firstline=31, lastline=37]{src/agda-dpp-impl.agda.replaced} -Agda では並列実行を行うことができない。そのためstep単位の実行を一つづつ行うことで -並列実行をしていることとする。 +Agda では並列実行を行うことができない．そのためstep単位の実行を一つづつ行うことで +並列実行をしていることとする． -この際に Env にある List Phi の中身を展開しながら一つづつ行動を処理していく。 +この際に Env にある List Phi の中身を展開しながら一つづつ行動を処理していく． \lstinputlisting[caption=Gears Agdaでの DPP の左のフォークを取る記述, label=agda-dpp-lfork, firstline=39]{src/agda-dpp-impl.agda.replaced} -Code \ref{agda-dpp-lfork}がstep実行をした際に哲学者が左側のフォークを取る記述になる。 +Code \ref{agda-dpp-lfork}がstep実行をした際に哲学者が左側のフォークを取る記述になる． -左側のフォークを取る際には table の index は pid の次の値になっている。 -図 \ref{fig:DPP} を見ると直感的に理解ができる。 +左側のフォークを取る際には table の index は pid の次の値になっている． +図 \ref{fig:DPP} を見ると直感的に理解ができる． -最後の哲学者は一番最初のフォークを参照する必要がある。 -フォークの状態を確認し、値が0である場合はフォークがテーブルの上にあるので +最後の哲学者は一番最初のフォークを参照する必要がある． +フォークの状態を確認し，値が0である場合はフォークがテーブルの上にあるので それを自分のpidに書き換えleft-handをtrueに書き換えてフォークを手に持つ -フォークの状態が0以外、すなわち他の哲学者がその場所のフォークを取得している場合は -状態を変化させずに処理を続ける。 -このように左のフォークを取る記述をした。 +フォークの状態が0以外，すなわち他の哲学者がその場所のフォークを取得している場合は +状態を変化させずに処理を続ける． +このように左のフォークを取る記述をした． -右側のフォークを取る場合は引数の部分を1足さずにそのまま受け取る。 -比較するべきtableのListと哲学者のListは一致しているため、put\_lforkのように最後の哲学者が -最初のフォークを参照することもない。 +右側のフォークを取る場合は引数の部分を1足さずにそのまま受け取る． +比較するべきtableのListと哲学者のListは一致しているため，put\_lforkのように最後の哲学者が +最初のフォークを参照することもない． -似たような形で哲学者がフォークを置く putdown-l/rfork を実装した。 +似たような形で哲学者がフォークを置く putdown-l/rfork を実装した． -思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている。 +思考と食事の実装に関してはそのまま状態を変更することなく進むようにしている． diff -r 7434c0aa1859 -r 6c0b1fcbac2d Paper/tex/intro.tex --- a/Paper/tex/intro.tex Thu May 05 17:01:12 2022 +0900 +++ b/Paper/tex/intro.tex Thu May 05 17:38:06 2022 +0900 @@ -1,46 +1,46 @@ \section{Gears Agda でのモデル検査} \pagenumbering{arabic} -思い思いにプログラムを書くと,冗長なコードができてしまい, -実行時間も遅い場合がある。 +思い思いにプログラムを書くと，冗長なコードができてしまい， +実行時間も遅い場合がある． この場合にコードに対してアルゴリズムを適応すると実行が最適化され -実行時間が減り,かつ第三者がコードを読んだ際にロジックが統一されているため理解が容易くなる。 -つまり,一般的に良いコードが作成できる。 +実行時間が減り，かつ第三者がコードを読んだ際にロジックが統一されているため理解が容易くなる． +つまり，一般的に良いコードが作成できる． -しかし,世の中にはすでに大量のアルゴリズムが存在するため, -これを一人のプログラマーが全て覚え,適応できる場面を思いつくというのは不可能に近い。 -その道に詳しい人が複数人いる場面というのも稀だと考えられる。 +しかし，世の中にはすでに大量のアルゴリズムが存在するため， +これを一人のプログラマーが全て覚え，適応できる場面を思いつくというのは不可能に近い． +その道に詳しい人が複数人いる場面というのも稀だと考えられる． -そのため,人が書いたコードに対してアルゴリズムを使用するコードに変換できるようにしたい。 +そのため，人が書いたコードに対してアルゴリズムを使用するコードに変換できるようにしたい． -この際,アルゴリズム適応前後で処理が変わっていないか検証するのは普通のプログラミング言語では難しい。 -一般的なプログラミング言語では,関数の遷移が自由であることから,関数遷移などで発生した -暗黙の環境が存在するためである。 +この際，アルゴリズム適応前後で処理が変わっていないか検証するのは普通のプログラミング言語では難しい． +一般的なプログラミング言語では，関数の遷移が自由であることから，関数遷移などで発生した +暗黙の環境が存在するためである． -この問題を解決するため,Gears Agda を用いる。 +この問題を解決するため，Gears Agda を用いる． -Gears Agda とは当研究室で開発している Continuation based C (CbC) の概念を取り入れた記法で書かれた Agda のことで, -通常のプログラミング言語では関数を実行する際にはメインルーチンからサブルーチンに遷移する。 -この際メインルーチンで使用していた変数などの環境はスタックされ,サブルーチンが終了した際にメインルーチンに戻り, -スタックしていた変数をもとに戻す流れとなる。 -CbCの場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ,スタックを持たず環境を保持しない。 -更に遷移後にメインルーチンに戻ることもない。 -つまり関数の実行では暗黙な環境が存在せず,関数が受け取った引数のみを使用する。 -これにより限定的な実行条件を作成でき,検証がしやすくなる。 +Gears Agda とは当研究室で開発している Continuation based C （CbC） の概念を取り入れた記法で書かれた Agda のことで， +通常のプログラミング言語では関数を実行する際にはメインルーチンからサブルーチンに遷移する． +この際メインルーチンで使用していた変数などの環境はスタックされ，サブルーチンが終了した際にメインルーチンに戻り， +スタックしていた変数をもとに戻す流れとなる． +CbCの場合はサブルーチンコールの際にアセンブラで言うjmpで関数遷移を行うことができ，スタックを持たず環境を保持しない． +更に遷移後にメインルーチンに戻ることもない． +つまり関数の実行では暗黙な環境が存在せず，関数が受け取った引数のみを使用する． +これにより限定的な実行条件を作成でき，検証がしやすくなる． -現在,アルゴリズムの適応可否は以下の方法を考えている。 +現在，アルゴリズムの適応可否は以下の方法を考えている． -あらかじめ,アルゴリズムの実装と検証をおこなったアルゴリズムSetsを用意しておく。 +あらかじめ，アルゴリズムの実装と検証をおこなったアルゴリズムSetsを用意しておく． -書いたコードが事前に定義していたアルゴリズムの仕様を満たしているかを検証していき, -満たしているコードがあった場合にそのコードを事前に定義してあるアルゴリズムに入れ替える方針を考えている。 +書いたコードが事前に定義していたアルゴリズムの仕様を満たしているかを検証していき， +満たしているコードがあった場合にそのコードを事前に定義してあるアルゴリズムに入れ替える方針を考えている． -この際,実装が仕様を満たしているか検証する手法には,定理証明やモデル検査などが挙げられる。 +この際，実装が仕様を満たしているか検証する手法には，定理証明やモデル検査などが挙げられる． -アルゴリズムの入れ替え可否判定には Gears Agda でモデル検査を行い, -アルゴリズムの仕様がコードに適応できるか検証するのが妥当だと考えている。 -思い思いに書いたコードに対して定理証明を行うのはコストが高く,適応するものの内部動作が一致しない場合定理証明を行っても使えないためである。 +アルゴリズムの入れ替え可否判定には Gears Agda でモデル検査を行い， +アルゴリズムの仕様がコードに適応できるか検証するのが妥当だと考えている． +思い思いに書いたコードに対して定理証明を行うのはコストが高く，適応するものの内部動作が一致しない場合定理証明を行っても使えないためである． -本論文では Gears Agda でのモデル検査の先駆けとして Dining philosophers problem (DPP) のモデル検査を行う。 +本論文では Gears Agda でのモデル検査の先駆けとして Dining philosophers problem （DPP） のモデル検査を行う．