changeset 10:9de3eaf8b40f

modify explanation of CbC
author Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
date Thu, 14 Jun 2012 19:45:16 +0900
parents 2016fd4e0191
children bf3c780d3039
files paper/aplas2012.tex paper/cbc.bib
diffstat 2 files changed, 159 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- 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}
 
 
 
--- 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/"
 }