# HG changeset patch # User Tatsuki IHA # Date 1517823332 -32400 # Node ID ca7c9340f60bbbab3597bcfda26fb47b8ea267ef # Parent 1d8a79195742ff701c4ef7c5dc5eb1c31764dca3 Update diff -r 1d8a79195742 -r ca7c9340f60b mindmap.mm --- 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 @@ - + + + + + + + + + + + + + + + + + + + + + + @@ -43,6 +64,9 @@ + + + diff -r 1d8a79195742 -r ca7c9340f60b paper/conclusion.tex --- 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 で必要になったときに初めてデータの通信を行うことで、最低限のデータ通信で処理を実行できる。 diff -r 1d8a79195742 -r ca7c9340f60b paper/introduction.tex --- 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{本論文の構成} diff -r 1d8a79195742 -r ca7c9340f60b paper/master_paper.pdf Binary file paper/master_paper.pdf has changed diff -r 1d8a79195742 -r ca7c9340f60b paper/reference.bib --- 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 コンパイラの改良",