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