Mercurial > hg > Papers > 2012 > aplas
annotate paper/rectype.ind @ 15:68d2c32f74cf
modify explanation of rectype syntax
| author | Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 15 Jun 2012 00:24:11 +0900 |
| parents | 66931f63db4d |
| children | b5bef0479ef5 |
| rev | line source |
|---|---|
| 11 | 1 -title: Recursive type syntax in Continuation based C |
| 2 | |
| 3 \newcommand{\rectype}{{\tt \_\_rectype}} | |
| 4 | |
| 5 --author: Shinji Kono, Nobuyasu Oshiro | |
| 6 | |
| 7 --abstract: | |
| 8 We have implemented Continuation based C (CbC). | |
| 9 CbC is an extension of C, which has parameterized goto statement. | |
| 10 It is useful for finite state automaton or many core tasks. | |
| 11 Goto statement is a way to force tail call elimination. | |
| 12 The destination of goto statement is called Code Segment, which is actually a normal function of C. | |
| 13 To represent recursive function call, the type system of C is not enough, because | |
| 14 it has no recursive types. | |
| 15 We introduce \rectype keyword for recursive type, and it is implemented in GCC-4.6.0. | |
| 16 We will compare the conventional methods, \rectype keyword and a method using C structure. | |
| 17 Also we show usage of CbC and it's benchmark. | |
| 18 | |
| 19 | |
| 20 --Continuation based C | |
| 21 | |
| 22 CbC's basic programming unit is a code segment. It is not a subroutine, but it | |
| 23 looks like a function, because it has input and output. We can use C struct | |
| 24 as input and output interfaces. | |
| 25 | |
| 26 struct interface1 { int i; }; | |
| 27 struct interface2 { int o; }; | |
| 28 | |
| 29 __code f(struct interface1 a) { | |
| 30 struct interface2 b; b.o=a.i; | |
| 31 goto g(b); | |
| 32 } | |
| 33 | |
| 34 In this example, a code segment | |
| 35 \verb+f+ has \verb+input a+ and sends \verb+output b+ to a code segment \verb+g+. | |
| 36 There is no return from code segment \verb+b+, \verb+b+ should call another | |
| 37 continuation using \verb+goto+. Any control structure in C is allowed in CwC | |
| 38 language, but in case of CbC, we restrict ourselves to use \verb+if+ statement | |
| 39 only, because it is sufficient to implement C to CbC translation. In this case, | |
| 40 code segment has one input interface and several output interfaces (fig.\ref{code}). | |
| 41 | |
| 42 \includegraphics[width=6cm]{ | |
| 43 \begin{figure}[htb] | |
| 44 \begin{center} | |
| 45 \includegraphics[width=6cm]{figure/code.pdf} | |
| 46 \caption{code} | |
| 47 \end{center} | |
| 48 \label{code} | |
| 49 \end{figure} | |
| 50 | |
| 51 | |
| 52 | |
| 53 \verb+__code+ and parameterized global goto statement is an extension of | |
| 54 Continuation based C. Unlike \verb+C--+ \cite{cminusminus}'s parameterized goto, | |
| 55 we cannot goto into normal C function. | |
| 56 | |
| 57 --Intermix with C | |
| 58 | |
| 59 In CwC, we can go to a code segment from a C function and we can call C functions | |
| 60 in a code segment. So we don't have to shift completely from C to CbC. The later | |
| 61 one is straight forward, but the former one needs further extensions. | |
| 62 | |
| 63 void *env; | |
| 64 __code (*exit)(int); | |
| 65 | |
| 66 __code h(char *s) { | |
| 67 printf(s); | |
| 68 goto (*exit)(0),env; | |
| 69 } | |
| 70 | |
| 71 int main() { | |
| 72 env = __environment; | |
| 73 exit = __return; | |
| 74 goto h("hello World\n"); | |
| 75 } | |
| 76 | |
| 77 In this hello world example, the environment of \verb+main()+ | |
| 78 and its continuation is kept in global variables. The environment | |
| 79 and the continuation can be get using \verb+__environment+, | |
| 80 and \verb+__return+. Arbitrary mixture of code segments and functions | |
| 81 are allowed (in CwC). The continuation of \verb+goto+ statement | |
| 82 never returns to original function, but it goes to caller of original | |
| 83 function. In this case, it returns result 0 to the operating system. | |
| 84 | |
| 85 | |
| 86 --What's good? | |
| 87 | |
| 88 CbC is a kind of high level assembler language. It can do several | |
| 89 original C language cannot do. For examples, | |
| 90 | |
| 91 {\small | |
| 92 \begin{verbatim} | |
| 93 Thread Scheduler | |
| 94 Context Switch | |
| 95 Synchronization Primitives | |
| 96 I/O wait semantics | |
| 97 | |
| 98 \end{verbatim} | |
| 99 } | |
| 100 | |
| 101 are impossible to write in C. Usually it requires some help of | |
| 102 assembler language such as \verb+__asm+ statement extension which is | |
| 103 of course not portable. | |
| 104 | |
| 105 --Scheduler example | |
| 106 | |
| 107 We can easily write these things in CbC, because | |
| 108 CbC has no hidden information behind the stack frame of C. | |
| 109 A thread simply go to the scheduler, | |
| 110 | |
| 111 goto scheduler(self, task_list); | |
| 112 | |
| 113 | |
| 114 and the scheduler simply pass the control to the next | |
| 115 thread in the task queue. | |
| 116 | |
| 117 code scheduler(Thread self,TaskPtr list) | |
| 118 { | |
| 119 TaskPtr t = list; | |
| 120 TaskPtr e; | |
| 121 list = list->next; | |
| 122 goto list->thread->next(list->thread,list); | |
| 123 } | |
| 124 | |
| 125 Of course it is a simulator, but it is an implementation | |
| 126 also. If we have a CPU resource API, we can write real multi | |
| 127 CPU scheduler in CbC. | |
| 128 | |
| 129 This is impossible in C, because we cannot access the hidden | |
| 130 stack which is necessary to switch in the scheduler. In CbC, | |
| 131 everything is visible, so we can switch threads very easily. | |
| 132 | |
| 133 This means we can use CbC as an executable specification | |
| 134 language of OS API. | |
| 135 | |
| 136 --Self Verification | |
| 137 | |
| 138 Since we can write a scheduler in CbC, we can also enumerate | |
| 139 all possible interleaving of a concurrent program. We have | |
| 140 implement a model checker in CwC. CbC can be a self verifiable | |
| 141 language\cite{kono08a}. | |
| 142 | |
| 143 SPIN\cite{holzmann97model} is a very reliable model checker, but it have to | |
| 144 use special specification language PROMELA. We cannot directly | |
| 145 use PROMELA as an implementation language, and it is slightly | |
| 146 difficult to study its concurrent execution semantics including | |
| 147 communication ports. | |
| 148 | |
| 149 There are another kind of model checker for real programming | |
| 150 language, such as Java PathFinder\cite{havelund98model}. Java PathFinder use | |
| 151 Java Virtual Machine (JVM) for state space enumeration which | |
| 152 is very expensive some time. | |
| 153 | |
| 154 In CbC, state enumerator itself is written in CbC, and its concurrency | |
| 155 semantics is written in CbC itself. Besides it is very close | |
| 156 to the implementation. Actually we can use CbC as an implementation | |
| 157 language. Since enumerator is written in the application itself, we | |
| 158 can perform abstraction or approximation in the application specific | |
| 159 way, which is a little difficult in Java PathFinder. It is possible | |
| 160 to handle JVM API for the purpose, although. | |
| 161 | |
| 162 We can use CPS transformed CbC source code for verification, but | |
| 163 we don't have to transform all of the source code, because CwC | |
| 164 supports all C constructs. (But not in C++... Theoretically it is | |
| 165 possible with using cfront converter, it should be difficult). | |
| 166 | |
| 167 | |
| 168 --As a target language | |
| 169 | |
| 170 Now we have GCC implementation of CbC, it runs very fast. Many | |
| 171 popular languages are implemented on top of C. Some of them | |
| 172 uses very large switch statement for the byte code interpreter. | |
| 173 We don't have to use these hacks, when we use CbC as an implementation | |
| 174 language. | |
| 175 | |
| 176 CbC is naturally similar to the state charts. It means it is very | |
| 177 close to UML diagrams. Although CbC does not have Object Oriented | |
| 178 feature such as message passing nor inheritance, which is not | |
| 179 crucial in UML. | |
| 180 | |
| 181 | |
| 14 | 182 --Recursive type syntax |
| 183 | |
| 184 CbC's program pass next pointer of code segment on argument. | |
| 185 It is passed as follows. | |
| 186 | |
| 187 __code csA( __code (*p)() ) { | |
| 188 goto p(csB); | |
| 189 } | |
| 190 | |
|
15
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
191 p is next pointer of codesegment. |
| 14 | 192 But, This declarationd is not right. |
| 193 Because p have arguments. | |
|
15
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
194 We wanted to the same type of p's arguments as type of csA's arguments. |
|
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
195 Right declaration is as follows. |
| 14 | 196 |
|
15
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
197 __code csA( __code (*p)( __code (*)( __code (*)( __code *)))) { |
| 14 | 198 goto p(csB); |
| 199 } | |
| 200 | |
|
15
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
201 The syntax of C Must be declared recursively. |
|
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
202 The following declaration if it may be that the type checking of p. |
| 11 | 203 |
|
15
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
204 __code csA( __code (*p)( __code )) { |
|
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
205 goto p(csB); |
|
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
206 } |
|
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
207 |
|
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
208 However this declaration is long. |
|
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
209 Therefore we implemented \rectype syntax in CbC on GCC. |
|
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
210 |
| 11 | 211 \rectype syntax is declare a recursive type. |
|
15
68d2c32f74cf
modify explanation of rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents:
14
diff
changeset
|
212 This example is using \rectype syntax. |
| 11 | 213 |
| 214 __code csA( __rectype *p) { | |
| 215 goto p(csB); | |
| 216 } | |
| 217 | |
| 218 *p represent pointer of csA at \ref{code:rectype} . | |
| 219 p's argument type is same csA that function pointer. | |
| 220 | |
| 221 | |
| 222 | |
| 223 | |
| 224 It is the same as the following. | |
| 225 | |
| 226 void csA( void (*p)(void*)) { | |
| 227 p(csB); | |
| 228 } | |
| 229 | |
| 230 --Implementation of \rectype in CbC on GCC | |
| 231 | |
| 232 | |
| 233 \begin{figure}[htpb] | |
| 234 \begin{minipage}{0.5\hsize} | |
| 235 \begin{center} | |
| 236 \scalebox{0.35}{\includegraphics{figure/tree1.pdf}} | |
| 237 \end{center} | |
| 238 \caption{} | |
| 239 \label{fig:tree1} | |
| 240 \end{minipage} | |
| 241 \begin{minipage}{0.2\hsize} | |
| 242 \begin{center} | |
| 243 \scalebox{0.35}{\includegraphics{figure/tree2.pdf}} | |
| 244 \end{center} | |
| 245 \caption{\rectype} | |
| 246 \label{fig:tree2} | |
| 247 \end{minipage} | |
| 248 \end{figure} | |
| 249 | |
| 250 | |
| 251 | |
| 252 --Method other than \rectype | |
| 253 | |
| 254 struct interface { | |
| 255 __code (*next)(struct interface); | |
| 256 }; | |
| 257 | |
| 258 __code csA(struct interface p) { | |
| 259 struct interface ds = { csB }; | |
| 260 goto p.next(ds); | |
| 261 } | |
| 262 | |
| 263 int main() { | |
| 264 struct interface ds = { print }; | |
| 265 goto csA(ds); | |
| 266 return 0; | |
| 267 } | |
| 268 | |
| 269 | |
| 270 | |
| 271 | |
| 272 | |
| 273 __code fibonacci(__rectype *p, int num, int count, int result, int prev) { | |
| 274 | |
| 275 | |
| 276 | |
| 277 \section{Comparision} | |
| 278 | |
| 279 | |
| 280 \begin{table}[htpb] | |
| 281 \centering | |
| 282 \small | |
| 283 \begin{tabular}{|l|r|r|r|} \hline | |
| 284 (unit: s) & ./conv1 1 & ./conv1 2 & ./conv1 3 \\ \hline | |
| 285 Micro-C(32bit) & 9.93 & 6.31 & 7.18 \\ \hline | |
| 286 Micro-C(64bit) & 5.03 & 5.12 & 5.00 \\ \hline \hline | |
| 287 GCC -O3(32bit) & 2.52 & 2.34 & 1.53 \\ \hline | |
| 288 GCC -O3(64bit) & 1.80 & 1.20 & 1.44 \\ \hline | |
| 289 \end{tabular} | |
| 290 \caption{Micro-C, GCC bench mark (in sec)} | |
| 291 \label{tab:mc,gcc,compare} | |
| 292 \end{table} | |
| 293 | |
| 294 | |
| 295 |