# HG changeset patch # User Yasutaka Higa # Date 1467784602 -32400 # Node ID cd70291dd5135b8098a97eef124789930f7de586 # Parent 5c71f479a00d25f151ea013b50723e12080db153 Add description meta/normal level diff -r 5c71f479a00d -r cd70291dd513 paper/vmpcbc.tex --- a/paper/vmpcbc.tex Wed Jul 06 14:27:50 2016 +0900 +++ b/paper/vmpcbc.tex Wed Jul 06 14:56:42 2016 +0900 @@ -166,8 +166,8 @@ ここで、Code Segmentどうしの接続処理について考える。 処理を表すCode Segmentどうしの接続も処理であるため、Code Segmentで表現できる。 -このような計算を実現するための計算をメタ計算と呼び、メタ計算を行なうCode SegmentをMeta Code Segmentと呼ぶ。 -Meta Code SegmentはCode Segment間に存在する処理と考えることもできる(図\ref{fig:metaCSDS})。 +このような、計算を実現するための計算をメタ計算と呼び、メタ計算を行なうCode SegmentをMeta Code Segmentと呼ぶ。 +Meta Code SegmentはCode Segment間に存在する上位の処理と考えることもできる(図\ref{fig:metaCSDS})。 \begin{figure}[htbp] \begin{center} @@ -185,6 +185,7 @@ Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。 CbC におけるCode SegmentはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。 Code Segmentどうしの接続は goto による軽量継続で表される(Code\ref{src:simpleCs})。 +軽量継続とは呼び出し元の環境を持たずに次の処理へと移動することであり、呼び出し元のスタックフレームを破棄しながら関数呼び出しを行なうようなものである。 \begin{lstlisting}[label=src:simpleCs, caption=code]%Code Segmentの接続例 (10加算して2倍する)] @@ -221,35 +222,44 @@ \end{lstlisting} Code\ref{src:simpleDs}ではData Segmentとして int を持つ count と unsigned int を持つ port の2つを定義している。 -Code Segmentに\verb/goto/する際に利用するData Segmentを指定することで、Data Segment内部の値で処理が行なえる(Code\ref{src:stub})。 +Code Segment 内部では演算やポインタ演算は行なわず、メタ計算部分でポインタへの演算を行なう。 +これにはメモリ管理をメタ計算部分に分離することで、プログラムを検証しやすくするねらいがある。 +Code Segment がどの Data Segment にアクセスするかといった指定も Meta Code Segment で行なう(Code\ref{src:stub} における \verb/twice_stub/)。 +CbC における Meta Code Segment は Code Segment と Code Segment 間に存在する Code Segment である。 \begin{lstlisting}[label=src:stub, caption=stub]%Data Segmentの利用例 (countの値を2倍する)] +// Code Segment __code addTen(union Data* ds, int a) { int b = a+10; goto twice_stub(ds); } +// Meta Code Segment __code twice_stub(union Data* ds) { goto twice(ds->count.x); } +// Code Segment __code twice(int x) { int y = 2*x; goto showValue(y); } \end{lstlisting} -Code\ref{src:stub}では \verb/twice/ の処理で2倍する値が count の値であることを \verb/twice_stub/ 内で指定している。 -CbC におけるMeta Code SegmentはCode\ref{src:stub} における \verb/twice_stub/ や goto する際に必ず通るCode Segment(Code\ref{src:meta}の \verb/meta/)のように表現される。 +CbC における Meta Data Segment は Data Segment を内包する構造体として定義できる(Code\ref{src:meta} における Context)。 +また、goto する際に必ず通る Meta Code Segment を定義することで、 Code Segment どうしの接続もメタ計算として定義できる(Code\ref{src:meta} における \verb/meta/)。 +\verb/meta/ を切り替えることで Code Segment を変更することなくメタ計算のみを変更することができる。 \begin{lstlisting}[label=src:meta, caption=meta ] %メタ計算として接続した例] +// Meta Data Segment struct Context { - union Data *data; - /* メタ計算に必要なデータ */ + union Data *data; // Data Segment + unsigned int a; /* メタ計算に必要なデータ */ }; +// Meta Code Segment __code meta(struct Context* context, enum Code next) { @@ -263,24 +273,24 @@ } } +// Code Segment __code addTen(struct Context* context, int a) { x = x+10; goto meta(context, Twice); } +// Code Segment __code twice(struct Context* context, int x) { x = x*2; goto meta(context, ShowValue); } \end{lstlisting} -メタ計算の切り替えは \verb/meta/ を変更することで実現できる。 -また、Meta Data Segmentに相当する \verb/Context/ はData Segmentをフィールドに持つ構造体として表現し、メタ計算に必要な処理は構造体にフィールドを追加することで表現できる. +メタ計算の例として、メモリ管理の他にも例外処理や並列実行やネットワークアクセスなどがある。 +通常の計算を保存するようメタ計算を定義することで、例外処理などを含む計算に拡張することができる\cite{cite:monad}。 -CbC におけるメタ計算の例にメモリ管理がある。 -メモリの確保やポインタ演算をMeta Code Segmentのみで行なうことで、Code Segment側ではメモリに由来するエラーを排除することができる。 -加えて、メタ計算を切り替えることでメモリの管理方法も切り替えることができるため、不要な領域の開放するよう拡張することも容易である。 -また、通常の計算を保存するようメタ計算を定義することで、例外処理などを含む計算に拡張することができる\cite{cite:monad}。 +\section{CbC で記述した赤黒木} +// TODO \section{メタ計算を用いたデータ構造の性質の検証} CbC で記述されたデータ構造と、データ構造に対する処理の性質を実際に検証する。