# HG changeset patch # User atton # Date 1485133241 -32400 # Node ID 925d7e02b712b35d93db8910c75f571464234255 # Parent c748fb29667320fb2aad9caaf3180292a78e4ebb Add bibliography diff -r c748fb296673 -r 925d7e02b712 paper/cbc.tex --- a/paper/cbc.tex Sun Jan 22 16:35:37 2017 +0900 +++ b/paper/cbc.tex Mon Jan 23 10:00:41 2017 +0900 @@ -107,7 +107,7 @@ 現在存在するメタ計算としてメモリの確保と割り当て、並列に書き込むことが可能な Synchronized Queue、データの保存に用いる非破壊赤黒木がある。 GearsOS では CodeSegment と DataSegment はそれぞれ CodeGear と DataGear と呼ばれている。 -マルチコアCPU環境では CodeGear と CodeSegment は同一だが、GPU 環境では CodeGear には OpenCL/CUDA における kernel も含まれる。 % TODO: ref +マルチコアCPU環境では CodeGear と CodeSegment は同一だが、GPU 環境では CodeGear には OpenCL/CUDA における kernel も含まれる。 % TODO: ref OpenCL/CUDA kernel とは GPU で実行される関数のことであり、GPU上のメモリに配置されたデータ群に対して並列に実行されるものである。 通常 GPU でデータの処理を行なう場合はデータの転送、転送終了を同期で確認、 kernel 実行、kernel の終了を同期で確認する、という手順が必要である。 CPU/GPU での処理をメタ計算で行なうことにより、ノーマルレベルでは CodeGear が実行されるデバイスや DataGear の位置を意識する必要が無いというメリットがある。 diff -r c748fb296673 -r 925d7e02b712 paper/introduction.tex --- a/paper/introduction.tex Sun Jan 22 16:35:37 2017 +0900 +++ b/paper/introduction.tex Mon Jan 23 10:00:41 2017 +0900 @@ -14,7 +14,7 @@ モデル検査器や証明でソフトウェアを検証する際、検証を行なう言語と実装に使われる言語が異なるという問題がある。 言語が異なれば二重で同じソフトウェアを記述する必要がある上、検証に用いるソースコードは状態遷移系でプログラムを記述するなど実装コードに比べて記述が困難である。 検証されたコードから実行可能なコードを生成可能な検証系もあるが、既存の実装に対する検証は行なえない。 -そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{cbc} 言語を開発している。 %TODO: ref +そこで、当研究室では検証と実装が同一の言語で行なえる Continuation based C\cite{utah-master} 言語を開発している。 Continuation based C (CbC)はC言語と似た構文を持つ言語である。 CbC では処理の単位は関数ではなく CodeSegment という単位で行なわれる。 @@ -36,4 +36,4 @@ 第\ref{chapter:agda}章では証明支援系プログラミング言語 Agda についての解説を行なう。 Agda の構文や使い方、Curry-Howard Isomorphism や Natural Deduction といった証明に関する解説も行なう。 第\ref{chapter:subtype}章では、部分型を用いて CbC のプログラムを Agda で記述し、証明を行なう。 -CodeSegment や DataSegment の Agda 上での定義や、メタ計算がどのように定義されるかを解説する。 +CodeSegment や DataSegment の Agda 上での定義や、メタ計算はどのように定義されるかを解説する。 diff -r c748fb296673 -r 925d7e02b712 paper/reference.bib --- a/paper/reference.bib Sun Jan 22 16:35:37 2017 +0900 +++ b/paper/reference.bib Mon Jan 23 10:00:41 2017 +0900 @@ -132,4 +132,9 @@ month = "may" } -% TODO : 会長さんの修論 +@mastersthesis{utah-master, + author = "徳森海斗", + title = "LLVM Clang 上の Continuation based C コンパイラ の改良", + school = "琉球大学 大学院理工学研究科 情報工学専攻", + year = "2016" +}