Mercurial > hg > Papers > 2018 > parusu-master
changeset 44:ca7c9340f60b
Update
| author | Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 05 Feb 2018 18:35:32 +0900 |
| parents | 1d8a79195742 |
| children | d24a4c224f71 |
| files | mindmap.mm paper/conclusion.tex paper/introduction.tex paper/master_paper.pdf paper/reference.bib |
| diffstat | 5 files changed, 78 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/mindmap.mm Mon Feb 05 14:40:17 2018 +0900 +++ b/mindmap.mm Mon Feb 05 18:35:32 2018 +0900 @@ -1,7 +1,28 @@ <map version="1.0.1"> <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net --> <node CREATED="1512458853968" ID="ID_16361895" MODIFIED="1512460306570" TEXT="Gears os の並列処理"> -<node CREATED="1512459013907" ID="ID_1199179481" MODIFIED="1512459028630" POSITION="right" TEXT="研究目的"> +<node CREATED="1512459013907" ID="ID_1199179481" MODIFIED="1517730926921" POSITION="right" TEXT="研究目的"> +<node CREATED="1517730929684" ID="ID_268702329" MODIFIED="1517730938255" TEXT="OSの話"> +<node CREATED="1517730938619" ID="ID_618406193" MODIFIED="1517731034114" TEXT="OS の信頼性を保証するのは難しい"> +<node CREATED="1517730959574" ID="ID_1233591714" MODIFIED="1517730987509" TEXT="時代とともに進歩するハードウェア、サービスに応じて OS 自体が拡張される必要がある"/> +<node CREATED="1517731034114" ID="ID_158801483" MODIFIED="1517731042835" TEXT="OS は非決定的な実装を持つ"> +<node CREATED="1517731043151" ID="ID_545030377" MODIFIED="1517731073595" TEXT="信頼性を保証するには従来のテスト、デバッグでは不十分(これは並列処理でも言えるか)"/> +<node CREATED="1517731077671" ID="ID_769632606" MODIFIED="1517731084132" TEXT="テストしきれない部分が残ってしまう"/> +</node> +<node CREATED="1517731089014" ID="ID_127450618" MODIFIED="1517731097079" TEXT="証明を用いる方法"/> +<node CREATED="1517731097328" ID="ID_335916317" MODIFIED="1517731156205" TEXT="モデル検査"> +<node CREATED="1517811634998" ID="ID_146024589" MODIFIED="1517811641044" TEXT="全ての状態を網羅する"/> +<node CREATED="1517811641617" ID="ID_1046833501" MODIFIED="1517811665982" TEXT="状態が巨大になる傾向になるため、抽象的なデータ構造を検査する"/> +</node> +</node> +<node CREATED="1517811294432" ID="ID_1832476758" MODIFIED="1517811314902" TEXT="Haskell, Python 等の OS のプログラムを coq とかで証明する"/> +<node CREATED="1517811420313" ID="ID_737470099" MODIFIED="1517811434147" TEXT="うちは、 Gears のコードを agdaで証明"/> +<node CREATED="1517811442994" ID="ID_466287053" MODIFIED="1517811449316" TEXT="SPIN でモデルチェックする"> +<node CREATED="1517811474316" ID="ID_1021466035" MODIFIED="1517811515707" TEXT="promela"/> +<node CREATED="1517811520770" ID="ID_1007640310" MODIFIED="1517811530121" TEXT="promela のコードを C に変換してモデルチェックする"/> +</node> +<node CREATED="1517811455844" ID="ID_996432990" MODIFIED="1517811472893" TEXT="CbC のコードを メタレベルで CbC のコードでモデルチェック"/> +</node> <node CREATED="1492596132358" ID="ID_251539353" MODIFIED="1492596147777" TEXT="並列処理のプログラミングは信頼性の確保が難しい"> <node CREATED="1494759599699" ID="ID_1103318080" MODIFIED="1494759613270" TEXT="複雑さ"> <node CREATED="1494759614698" ID="ID_1336227916" MODIFIED="1494759622158" TEXT="パイプライン"/> @@ -43,6 +64,9 @@ </node> <node CREATED="1492596298268" ID="ID_137287743" MODIFIED="1492596303427" TEXT="信頼性の確保"> <node CREATED="1492596303787" ID="ID_1118780576" MODIFIED="1492596308410" TEXT="モデルチェッキング"> +<node CREATED="1517732559423" ID="ID_1204189563" MODIFIED="1517732563873" TEXT="すべての状態を列挙する"> +<node CREATED="1517732567388" ID="ID_152517777" MODIFIED="1517732605532" TEXT="巨大な状態になりやすいので"/> +</node> <node CREATED="1492605188884" ID="ID_1336932146" MODIFIED="1492605199086" TEXT="single linked queue"/> <node CREATED="1492605200092" ID="ID_53892540" MODIFIED="1492605203422" TEXT="RB tree"/> </node>
--- a/paper/conclusion.tex Mon Feb 05 14:40:17 2018 +0900 +++ b/paper/conclusion.tex Mon Feb 05 18:35:32 2018 +0900 @@ -1,2 +1,22 @@ \chapter{まとめ} \section{今後の課題} +今後の課題として、Gears OS の並列処理の信頼性の保証、 チューニングを行う。 + +Gears OS では証明とモデル検査をメタレベルで実行することで信頼性を保証する。 +証明は CbC のプログラムを証明支援系の Agda\cite{agda} に対応させて証明を行う。 +現在は Gears OS の Interface 部分の動作の証明を行っており、Stack や Tree の動作の証明を行っている。 +Gears OS の並列処理の信頼性を証明するには Synchronized Queue の証明を行う必要がある。 + +モデル検査では CbC で記述されたモデル検査器である akasha \cite{atton-ipsj}を使用して行う。 +モデル検査の方針としては、Code Gear の実行を擬似並列で実行し、全ての組合せを列挙する方法で行う。 + +Gears OS は par goto 文を使用することで Context を生成し、並列処理を行う。 +しかし、Context はメモリ空間の確保や使用する全ての Code/Data Gear を設定する必要があり、生成にある程度の時間がかかってしまう。 +par goto 文は通常のプログラミングの関数呼び出しのように扱われる。 +そこで、 par goto のコンパイルタイミングで実行する Code Gear のフローをモデル検査で解析し、処理が軽い場合は並列に実行せずに、関数呼び出しを行う等の最適化を行う。 + +今回の CUDA 実装では Output Data Gear を書き出す際に一度 GPU から CPU にデータの送信する必要があった。 +しかし、CPU、 GPU 間のデータの通信はコストが高いことが例題の結果からわかった。 +GPU にあるデータは CPU 側ではポインタで持つことが出来る。 +そこで Meta Data Gear に Data Gear が CPU、GPU のどこで所持されているかを持たせる。 +GPU にある Data Gear が CPU で必要になったときに初めてデータの通信を行うことで、最低限のデータ通信で処理を実行できる。
--- a/paper/introduction.tex Mon Feb 05 14:40:17 2018 +0900 +++ b/paper/introduction.tex Mon Feb 05 18:35:32 2018 +0900 @@ -10,4 +10,3 @@ 従来の研究ではPython\cite{Sigurbjarnarson:2016:PVF:3026877.3026879} や Haskell\cite{Chen:2015:UCH:2815400.2815402}\cite{Klein:2009:SFV:1629575.1629596}による記述した OS を検証する研究も存在する。 また SPIN などのモデル検査を OS の検証に用いた例もである。 本研究室では信頼性をノーマルレベルの掲載に対して保証し、拡張性をメタレベルの計算で実現することを目標に Gears OS を開発している。 -\section{本論文の構成}
--- a/paper/reference.bib Mon Feb 05 14:40:17 2018 +0900 +++ b/paper/reference.bib Mon Feb 05 18:35:32 2018 +0900 @@ -15,6 +15,24 @@ keywords = {compare_and_swap, concurrent queue, lock-free, multiprogramming, non-blocking}, } +@inproceedings{agda, + author = {Norell, Ulf}, + title = {Dependently Typed Programming in Agda}, + booktitle = {Proceedings of the 4th International Workshop on Types in Language Design and Implementation}, + series = {TLDI '09}, + year = {2009}, + isbn = {978-1-60558-420-1}, + location = {Savannah, GA, USA}, + pages = {1--2}, + numpages = {2}, + url = {http://doi.acm.org/10.1145/1481861.1481862}, + doi = {10.1145/1481861.1481862}, + acmid = {1481862}, + publisher = {ACM}, + address = {New York, NY, USA}, + keywords = {dependent types, programming}, +} + @inproceedings{Chen:2015:UCH:2815400.2815402, author = {Chen, Haogang and Ziegler, Daniel and Chajed, Tej and Chlipala, Adam and Kaashoek, M. Frans and Zeldovich, Nickolai}, title = {Using Crash Hoare Logic for Certifying the FSCQ File System}, @@ -85,6 +103,21 @@ keywords = {operating system, run-time system, type safety, verification}, } +@article{atton-ipsj, +author="比嘉, 健太 and 河野, 真治", +title="Verification Method of Programs Using Continuation based C", +journal="情報処理学会論文誌プログラミング（PRO）", +ISSN="1882-7802", +publisher="", +year="2017", +month="feb", +volume="10", +number="2", +pages="5-5", +URL="https://ci.nii.ac.jp/naid/170000148438/en/", +DOI="", +} + @article{go, author={J. Meyerson}, journal={IEEE Software}, @@ -198,7 +231,6 @@ note = {Accessed: 2018/02/05(Mon)} } - @mastersthesis{utah-master, author = "徳森海斗", title = "LLVM Clang 上の Continuation based C コンパイラ の改良",