# HG changeset patch # User Nobuyasu Oshiro # Date 1339670716 -32400 # Node ID 9de3eaf8b40f9b8e2700a2c483d7548e8eb7cfb5 # Parent 2016fd4e0191444a1e0eec345452edd99e149f15 modify explanation of CbC diff -r 2016fd4e0191 -r 9de3eaf8b40f paper/aplas2012.tex --- a/paper/aplas2012.tex Wed Jun 13 16:23:41 2012 +0900 +++ b/paper/aplas2012.tex Thu Jun 14 19:45:16 2012 +0900 @@ -114,7 +114,109 @@ function. In this case, it returns result 0 to the operating system. +\section{ What's good?} +CbC is a kind of high level assembler language. It can do several +original C language cannot do. For examples, + +{\small +\begin{verbatim} + Thread Scheduler + Context Switch + Synchronization Primitives + I/O wait semantics + +\end{verbatim} +} + +are impossible to write in C. Usually it requires some help of +assembler language such as \verb+__asm+ statement extension which is +of course not portable. + +\subsection{ Scheduler example} + +We can easily write these things in CbC, because +CbC has no hidden information behind the stack frame of C. +A thread simply go to the scheduler, + +{\small +\begin{verbatim} + goto scheduler(self, task_list); + +\end{verbatim} +} + +and the scheduler simply pass the control to the next +thread in the task queue. + +{\small +\begin{verbatim} + code scheduler(Thread self,TaskPtr list) + { + TaskPtr t = list; + TaskPtr e; + list = list->next; + goto list->thread->next(list->thread,list); + } + +\end{verbatim} +} + +Of course it is a simulator, but it is an implementation +also. If we have a CPU resource API, we can write real multi +CPU scheduler in CbC. + +This is impossible in C, because we cannot access the hidden +stack which is necessary to switch in the scheduler. In CbC, +everything is visible, so we can switch threads very easily. + +This means we can use CbC as an executable specification +language of OS API. + +\subsection{ Self Verification} + +Since we can write a scheduler in CbC, we can also enumerate +all possible interleaving of a concurrent program. We have +implement a model checker in CwC. CbC can be a self verifiable +language\cite{kono08a}. + +SPIN\cite{holzmann97model} is a very reliable model checker, but it have to +use special specification language PROMELA. We cannot directly +use PROMELA as an implementation language, and it is slightly +difficult to study its concurrent execution semantics including +communication ports. + +There are another kind of model checker for real programming +language, such as Java PathFinder\cite{havelund98model}. Java PathFinder use +Java Virtual Machine (JVM) for state space enumeration which +is very expensive some time. + +In CbC, state enumerator itself is written in CbC, and its concurrency +semantics is written in CbC itself. Besides it is very close +to the implementation. Actually we can use CbC as an implementation +language. Since enumerator is written in the application itself, we +can perform abstraction or approximation in the application specific +way, which is a little difficult in Java PathFinder. It is possible +to handle JVM API for the purpose, although. + +We can use CPS transformed CbC source code for verification, but +we don't have to transform all of the source code, because CwC +supports all C constructs. (But not in C++... Theoretically it is +possible with using cfront converter, it should be difficult). + + +\subsection{ As a target language} + +Now we have GCC implementation of CbC, it runs very fast. Many +popular languages are implemented on top of C. Some of them +uses very large switch statement for the byte code interpreter. +We don't have to use these hacks, when we use CbC as an implementation +language. + +CbC is naturally similar to the state charts. It means it is very +close to UML diagrams. Although CbC does not have Object Oriented +feature such as message passing nor inheritance, which is not +crucial in UML. @@ -129,14 +231,14 @@ \newpage \section{recursive type syntax} -We implemented \verb+__rectype+ syntax in GCC. +We implemented \verb+__rectype+ syntax in CbC on GCC. \verb+__rectype+ syntax is declare a recursive type. This example is using \verb+__rectype+ in CbC. \begin{figure}[htpb] \begin{verbatim} __code csA( __rectype *p) { - goto p(csB); + goto p(csB); } \end{verbatim} \caption{example using \_\_rectype} @@ -155,7 +257,7 @@ \begin{verbatim} void csA( void (*p)(void*)) { - p(csB); + p(csB); } \end{verbatim} @@ -163,12 +265,12 @@ \begin{verbatim} __code csA( __code (*p)( __code (*)( __code (*)( __code )))) { - goto p(csB); + goto p(csB); } \end{verbatim} -\subsection{Implementation of \_\_rectype in GCC} +\subsection{Implementation of \_\_rectype in CbC on GCC} \begin{figure}[htpb] @@ -194,18 +296,18 @@ \begin{verbatim} struct interface { - __code (*next)(struct interface); + __code (*next)(struct interface); }; __code csA(struct interface p) { - struct interface ds = { csB }; - goto p.next(ds); + struct interface ds = { csB }; + goto p.next(ds); } int main() { - struct interface ds = { print }; - goto csA(ds); - return 0; + struct interface ds = { print }; + goto csA(ds); + return 0; } \end{verbatim} @@ -227,24 +329,19 @@ \small \begin{tabular}{|l|r|r|r|} \hline (unit: s) & ./conv1 1 & ./conv1 2 & ./conv1 3 \\ \hline -Micro-C(32bit) & 9.93 & 6.31 & 7.18 \\ \hline -Micro-C(64bit) & 5.03 & 5.12 & 5.00 \\ \hline \hline -GCC -O3(32bit) & 2.52 & 2.34 & 1.53 \\ \hline -GCC -O3(64bit) & 1.80 & 1.20 & 1.44 \\ \hline +Micro-C(32bit) & 9.93 & 6.31 & 7.18 \\ \hline +Micro-C(64bit) & 5.03 & 5.12 & 5.00 \\ \hline \hline +GCC -O3(32bit) & 2.52 & 2.34 & 1.53 \\ \hline +GCC -O3(64bit) & 1.80 & 1.20 & 1.44 \\ \hline \end{tabular} \caption{Micro-C, GCC bench mark (in sec)} \label{tab:mc,gcc,compare} \end{table} - - - - - \bibliographystyle{junsrt} \bibliography{cbc} -\nocite{kono:2002a, kono:2000a, kono:2008a, yogi:2008a, yogi:2008b, yan:2002a,gcc_internals} +\nocite{cminusminus, havelund98model, holzmann97model, kono:2002a, kono:2000a, kono:2008a, yogi:2008a, yogi:2008b, yan:2002a, gcc, cbc_sourceforge} diff -r 2016fd4e0191 -r 9de3eaf8b40f paper/cbc.bib --- a/paper/cbc.bib Wed Jun 13 16:23:41 2012 +0900 +++ b/paper/cbc.bib Thu Jun 14 19:45:16 2012 +0900 @@ -46,10 +46,47 @@ year = 2002 } - +@article{cminusminus, +author = "Norman Ramsey and Simon~Peyton Jones.", +title = "A single intermediate language that supports multiple implementations of exceptions.", +journal = "ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation", +month = "June", +year = 2000 +} + + +@article{kono08a, +author = "河野　真治", +title = "検証を自身で表現できるハードウェア、ソフトウェア記述言語 Continuation based C と>、そのCell への応用", +journal = "電子通信学会VLD研究会", +month = "March", +year = 2008 +} + +@article{holzmann97model, +author = "Gerard~J. Holzmann.", +title = "The model checker {SPIN}.", +journal = "Software Engineering, Vol.~23, No.~5, pp. 279--295,", +year = 1997 +} + +@article{havelund98model, +author = "K.~Havelund and T.~Pressburger.", +title = "Model checking java programs using java pathfinder", +year = 1998 +} + + -@manual{gcc_internals, -author = "{GNU Compiler Collection (GCC) Internals}", -title ="{http://gcc.gnu.org/onlinedocs/gccint/}", +@source{cbc_sourceforge, +author = "{河野真治}", +title = "CbC", +mounth = "March", +year = 2008 +} + +@manual{gcc, +author = "GNU Compiler Collection (GCC) Internals", +title ="http://gcc.gnu.org/onlinedocs/gccint/" }