# HG changeset patch # User Yasutaka Higa # Date 1467789380 -32400 # Node ID 3728ac2a3c9f2dc034fa362158f783aeb0aa8c1e # Parent f8ec96d4882f57a55fdd07c0f4a44c3640dcd547 Fix lstlisting diff -r f8ec96d4882f -r 3728ac2a3c9f paper/vmpcbc.pdf Binary file paper/vmpcbc.pdf has changed diff -r f8ec96d4882f -r 3728ac2a3c9f paper/vmpcbc.tex --- a/paper/vmpcbc.tex Wed Jul 06 16:04:51 2016 +0900 +++ b/paper/vmpcbc.tex Wed Jul 06 16:16:20 2016 +0900 @@ -184,11 +184,12 @@ Code SegmentとData Segmentを用いたプログラミングスタイルで記述言語に Continuation based C\cite{cite:cbc-clang} 言語が存在する。 Continuation based C (以下 CbC)はOSや組込みシステムなどの記述を行なうことを目標に作られた、アセンブラとC言語の中間のような言語である。 CbC におけるCode SegmentはC言語における関数に、関数呼び出しが末尾のみである制約を加えようなものである。 -Code Segmentどうしの接続は goto による軽量継続で表される(Code\ref{src:simpleCs})。 +Code Segmentどうしの接続は goto による軽量継続で表される(表\ref{src:simpleCs})。 軽量継続とは呼び出し元の環境を持たずに次の処理へと移動することであり、呼び出し元のスタックフレームを破棄しながら関数呼び出しを行なうようなものである。 -\begin{lstlisting}[label=src:simpleCs, caption=code]%Code Segmentの接続例 (10加算して2倍する)] - +% {{{ Code Segment の接続(10加算して2倍する) +\begin{table} +\begin{lstlisting} __code addTen(int a) { int b = a+10; goto twice(b); @@ -198,19 +199,25 @@ int y = 2*x; goto showValue(y); } + \end{lstlisting} +\caption{Code Segment の接続(10加算して2倍する)} +\label{src:simpleCs} +\end{table} +% }}} CbCにおけるCode Segmentは、C言語の関数宣言の返り値の型の部分に \verb/__code/ を記述して定義する。 Code Segment内部には変数の宣言やif文による分岐といったC言語の文法を用いて処理を記述する。 -Code\ref{src:simpleCs}の例では、2つのCode Segment \verb/addTen/ と \verb/twice/を定義している。 +表\ref{src:simpleCs}の例では、2つのCode Segment \verb/addTen/ と \verb/twice/を定義している。 \verb/addTen/では int の値を受けとり、10加算して \verb/twice/ を実行する。 \verb/twice/ では受けとったintの値を2倍して \verb/showValue/ を実行する。 また、CbCにおけるData SegmentはC言語における構造体と共用体を用いたデータ構造である。 -各Code Segmentで必要な値を構造体で定義し、それらの共用体としてData Segmentを定義する(Code\ref{src:simpleDs})。 +各Code Segmentで必要な値を構造体で定義し、それらの共用体としてData Segmentを定義する(表\ref{src:simpleDs})。 -\begin{lstlisting}[label=src:simpleDs, caption=data]%Data Segmentの例 (10加算して2倍する)] - +% {{{ Data Segment の例 +\begin{table}[ht] +\begin{lstlisting} union Data { struct Count { int x; @@ -220,15 +227,20 @@ } port; }; \end{lstlisting} +\caption{Data Segmentの例} +\label{src:simpleDs} +\end{table} +% }}} -Code\ref{src:simpleDs}ではData Segmentとして int を持つ count と unsigned int を持つ port の2つを定義している。 +表\ref{src:simpleDs}ではData Segmentとして int を持つ count と unsigned int を持つ port の2つを定義している。 Code Segment 内部では演算やポインタ演算は行なわず、メタ計算部分でポインタへの演算を行なう。 これにはメモリ管理をメタ計算部分に分離することで、プログラムを検証しやすくするねらいがある。 -Code Segment がどの Data Segment にアクセスするかといった指定も Meta Code Segment で行なう(Code\ref{src:stub} における \verb/twice_stub/)。 +Code Segment がどの Data Segment にアクセスするかといった指定も Meta Code Segment で行なう(表\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倍する)] - +% {{{ Data Segment を指定する Meta Code Segment +\begin{table}[ht] +\begin{lstlisting} // Code Segment __code addTen(union Data* ds, int a) { int b = a+10; @@ -246,12 +258,20 @@ goto showValue(y); } \end{lstlisting} +\caption{Data Segment を指定する Meta Code Segment} +\label{src:stub} +\end{table} -CbC における Meta Data Segment は Data Segment を内包する構造体として定義できる(Code\ref{src:meta} における Context)。 -また、goto する際に必ず通る Meta Code Segment を定義することで、 Code Segment どうしの接続もメタ計算として定義できる(Code\ref{src:meta} における \verb/meta/)。 +% }}} + +CbC における Meta Data Segment は Data Segment を内包する構造体として定義できる(表\ref{src:meta} における Context)。 +また、goto する際に必ず通る Meta Code Segment を定義することで、 Code Segment どうしの接続もメタ計算として定義できる(表\ref{src:meta} における \verb/meta/)。 \verb/meta/ を切り替えることで Code Segment を変更することなくメタ計算のみを変更することができる。 -\begin{lstlisting}[label=src:meta, caption=meta ] %メタ計算として接続した例] +% {{{ Code Segment を接続するメタ計算メタ計算として接続した例 + +\begin{table}[ht] +\begin{lstlisting} // Meta Data Segment struct Context { @@ -285,6 +305,11 @@ goto meta(context, ShowValue); } \end{lstlisting} +\caption{Code Segment を接続するメタ計算メタ計算として接続した例} +\label{src:meta} +\end{table} + +% }}} メタ計算の例として、メモリ管理の他にも例外処理や並列実行やネットワークアクセスなどがある。 通常の計算を保存するようメタ計算を定義することで、例外処理などを含む計算に拡張することができる\cite{cite:monad}。 @@ -319,7 +344,9 @@ 親の色が黒である場合は木が平衡であるために処理を終了し、ユーザ側のCode Segment へと \verb/goto/ する。 親の色が赤である場合は経路情報を再現するためにスタックへと親を挿入し、次の条件判定へと \verb/goto/ する。 -\begin{table} +% {{{ 赤黒木の赤が続かないという制約の判定 + +\begin{table}[ht] \begin{lstlisting} // Meta Code Segment @@ -339,10 +366,12 @@ goto insertCase2(context, context->data[Traverse]->traverse.current); } \end{lstlisting} - \caption{赤黒木の赤が続かないという制約の判定} - \label{src:rbtree} +\caption{赤黒木の赤が続かないという制約の判定} +\label{src:rbtree} \end{table} +% }}} + ここで、赤黒木に対する処理を Code Segment とした場合、赤黒木のメモリ管理などは Meta Code Segment である。 赤黒木を利用する Code Segment からは赤黒木の処理は意識する必要がないため、赤黒木の処理はMeta Code Segment のように見え、赤黒木のメモリ管理は Meta Meta Code Segment と考えられる。 このようにメタ計算は階層構造を持つため、任意の Code Segment に対してメタ計算を適用することが可能であり、検証機構の検証なども行なうことができる。 @@ -356,18 +385,24 @@ まず、検証を行なうために満たすべき仕様を定義する。 仕様はデータ構造が常に満たすべき論理式として表現し、CbC のコードで記述する。 -検証する仕様として、とを CbC で定義する(Code\ref{src:specification})。 +検証する仕様として、とを CbC で定義する(表\ref{src:specification})。 -\begin{lstlisting}[label=src:specification, caption=s]% 木の高さの仕様記述] +% {{{ 木の高さの仕様記述 +\begin{table}[ht] +\begin{lstlisting} if (akashaInfo.maxHeight > 2*akashaInfo.minHeight) { goto meta(context, ShowTrace); } +\end{lstlisting} +\caption{木の高さの仕様記述} +\label{src:specification} +\end{table} -\end{lstlisting} +% }}} -Code\ref{src:specification}で定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。 +表\ref{src:specification}で定義した仕様に対し、挿入する値と順番の全ての組み合わせに対して確認していく。 また、仕様を満たさない反例が存在する場合はその具体的な組み合わせの値を出力する。 当研究室で開発している検証用メタ計算ライブラリ akasha と、C言語の有限モデルチェッカ CBMC\cite{cite:cbmc} を用いてこの仕様を検証した。