annotate paper/rectype.ind @ 22:f1839aae06dc

modify
author Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
date Fri, 15 Jun 2012 16:14:28 +0900
parents 88899c193e6d
children e9d317e4ea70
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
11
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 -title: Recursive type syntax in Continuation based C
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 --author: Shinji Kono, Nobuyasu Oshiro
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 --abstract:
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 We have implemented Continuation based C (CbC).
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 CbC is an extension of C, which has parameterized goto statement.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 It is useful for finite state automaton or many core tasks.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 Goto statement is a way to force tail call elimination.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 The destination of goto statement is called Code Segment, which is actually a normal function of C.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 To represent recursive function call, the type system of C is not enough, because
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 it has no recursive types.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 We introduce \rectype keyword for recursive type, and it is implemented in GCC-4.6.0.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 We will compare the conventional methods, \rectype keyword and a method using C structure.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 Also we show usage of CbC and it's benchmark.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 --Continuation based C
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 CbC's basic programming unit is a code segment. It is not a subroutine, but it
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 looks like a function, because it has input and output. We can use C struct
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 as input and output interfaces.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 struct interface1 { int i; };
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 struct interface2 { int o; };
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 __code f(struct interface1 a) {
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 struct interface2 b; b.o=a.i;
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 goto g(b);
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 }
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 In this example, a code segment
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 \verb+f+ has \verb+input a+ and sends \verb+output b+ to a code segment \verb+g+.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 There is no return from code segment \verb+b+, \verb+b+ should call another
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 continuation using \verb+goto+. Any control structure in C is allowed in CwC
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 language, but in case of CbC, we restrict ourselves to use \verb+if+ statement
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 only, because it is sufficient to implement C to CbC translation. In this case,
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 code segment has one input interface and several output interfaces (fig.\ref{code}).
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 \includegraphics[width=6cm]{
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 \begin{figure}[htb]
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 \begin{center}
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 \includegraphics[width=6cm]{figure/code.pdf}
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 \caption{code}
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 \end{center}
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 \label{code}
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 \end{figure}
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 \verb+__code+ and parameterized global goto statement is an extension of
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 Continuation based C. Unlike \verb+C--+ \cite{cminusminus}'s parameterized goto,
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 we cannot goto into normal C function.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 --Intermix with C
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 In CwC, we can go to a code segment from a C function and we can call C functions
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 in a code segment. So we don't have to shift completely from C to CbC. The later
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 one is straight forward, but the former one needs further extensions.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 void *env;
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 __code (*exit)(int);
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 __code h(char *s) {
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 printf(s);
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 goto (*exit)(0),env;
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 }
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 int main() {
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 env = __environment;
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 exit = __return;
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 goto h("hello World\n");
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 }
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 In this hello world example, the environment of \verb+main()+
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 and its continuation is kept in global variables. The environment
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 and the continuation can be get using \verb+__environment+,
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 and \verb+__return+. Arbitrary mixture of code segments and functions
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 are allowed (in CwC). The continuation of \verb+goto+ statement
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 never returns to original function, but it goes to caller of original
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 function. In this case, it returns result 0 to the operating system.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 --What's good?
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 CbC is a kind of high level assembler language. It can do several
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 original C language cannot do. For examples,
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 {\small
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 \begin{verbatim}
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 Thread Scheduler
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 Context Switch
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 Synchronization Primitives
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 I/O wait semantics
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 \end{verbatim}
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 }
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 are impossible to write in C. Usually it requires some help of
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 assembler language such as \verb+__asm+ statement extension which is
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 of course not portable.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 --Scheduler example
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 We can easily write these things in CbC, because
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 CbC has no hidden information behind the stack frame of C.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 A thread simply go to the scheduler,
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 goto scheduler(self, task_list);
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 and the scheduler simply pass the control to the next
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 thread in the task queue.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 code scheduler(Thread self,TaskPtr list)
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 {
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 TaskPtr t = list;
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 TaskPtr e;
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 list = list->next;
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 goto list->thread->next(list->thread,list);
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 }
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 Of course it is a simulator, but it is an implementation
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 also. If we have a CPU resource API, we can write real multi
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 CPU scheduler in CbC.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 This is impossible in C, because we cannot access the hidden
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 stack which is necessary to switch in the scheduler. In CbC,
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 everything is visible, so we can switch threads very easily.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 This means we can use CbC as an executable specification
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 language of OS API.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
136
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 --Self Verification
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
138
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
139 Since we can write a scheduler in CbC, we can also enumerate
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140 all possible interleaving of a concurrent program. We have
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141 implement a model checker in CwC. CbC can be a self verifiable
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 language\cite{kono08a}.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
144 SPIN\cite{holzmann97model} is a very reliable model checker, but it have to
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 use special specification language PROMELA. We cannot directly
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 use PROMELA as an implementation language, and it is slightly
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
147 difficult to study its concurrent execution semantics including
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 communication ports.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 There are another kind of model checker for real programming
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151 language, such as Java PathFinder\cite{havelund98model}. Java PathFinder use
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152 Java Virtual Machine (JVM) for state space enumeration which
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153 is very expensive some time.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 In CbC, state enumerator itself is written in CbC, and its concurrency
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 semantics is written in CbC itself. Besides it is very close
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 to the implementation. Actually we can use CbC as an implementation
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158 language. Since enumerator is written in the application itself, we
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159 can perform abstraction or approximation in the application specific
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 way, which is a little difficult in Java PathFinder. It is possible
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
161 to handle JVM API for the purpose, although.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
162
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
163 We can use CPS transformed CbC source code for verification, but
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
164 we don't have to transform all of the source code, because CwC
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
165 supports all C constructs. (But not in C++... Theoretically it is
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
166 possible with using cfront converter, it should be difficult).
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
167
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
168
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169 --As a target language
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
170
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
171 Now we have GCC implementation of CbC, it runs very fast. Many
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
172 popular languages are implemented on top of C. Some of them
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
173 uses very large switch statement for the byte code interpreter.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
174 We don't have to use these hacks, when we use CbC as an implementation
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
175 language.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
176
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
177 CbC is naturally similar to the state charts. It means it is very
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
178 close to UML diagrams. Although CbC does not have Object Oriented
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
179 feature such as message passing nor inheritance, which is not
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
180 crucial in UML.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
181
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182
14
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
183 --Recursive type syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
184
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
185 CbC's program pass next pointer of code segment on argument.
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
186 It is passed as follows.
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
187
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
188 __code csA( __code (*p)() ) {
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
189 goto p(csB);
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
190 }
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
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
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
193 But, This declarationd is not right.
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
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
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
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
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
199 goto p(csB);
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
200 }
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
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
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
214
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
215 __code csA( __rectype *p) {
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
216 goto p(csB);
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
217 }
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
218
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
219 *p represent pointer of csA at \ref{code:rectype} .
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
220 p's argument type is same csA that function pointer.
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
221
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
222
21
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
223 --Problems with implementation of \rectype.
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
224 Segmentation fault has occurred in the following program on compile.
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
225
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
226 __code csA(__rectype *p) {
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
227 goto p(3);
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
228 }
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
229
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
230 The above code is the wrong argument of p.
22
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
231 The p's argument is converted by GCC.
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
232 3 of type int is converted to a pionter type of code segment.
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
233 At this time, GCC looks at the type of the argument.
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
234 p's argument is pointer of csA.
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
235 csA's argument is p.
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
236 GCC is also an infinite recursion happens to see the type of tye argument of the argument.
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
237
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 21
diff changeset
238 In order to the solve this problem.
21
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
239
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
240
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
241
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
242
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
243
16
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
244 --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
245 \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
246 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
247 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
248 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
249
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
250 \begin{figure}[htpb]
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
251 \begin{minipage}{0.5\hsize}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
252 \begin{center}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
253 \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
254 \end{center}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
255 \caption{AST of function pointer}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
256 \label{fig:tree1}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
257 \end{minipage}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
258 \begin{minipage}{0.2\hsize}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
259 \begin{center}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
260 \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
261 \end{center}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
262 \caption{AST of \rectype}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
263 \label{fig:tree2}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
264 \end{minipage}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
265 \end{figure}
b5bef0479ef5 modify how to implement rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
266
17
02bd9a41010f modify How to implement rectype syntax
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 16
diff changeset
267 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
268 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
269 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
270 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
271 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
272 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
273 We have to override it in the pointer of csA.
11
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
274
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
275
18
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
276 --
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
277
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
278
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
279
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
280
11
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
281 --Method other than \rectype
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
282
18
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
283 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
284 For example, if we write
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
285
11
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
286 struct interface {
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
287 __code (*next)(struct interface);
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
288 };
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
289
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
290 __code csA(struct interface p) {
18
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
291 struct interface ds;
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
292 ds.next = csB;
11
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
293 goto p.next(ds);
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
294 }
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
295
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
296 int main() {
18
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
297 struct interface ds;
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
298 ds = print;
11
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
299 goto csA(ds);
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
300 return 0;
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
301 }
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
302
18
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
303 there is no need to write recursively.
33b7a54edaa9 method other rectype
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
304 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
305 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
306 Recursively program does not occur.
11
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
307
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
308
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
309
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
310 \section{Comparision}
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
311
19
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
312 Here is our bench mark program.
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
313 {\small
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
314 f0(int i) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
315 int k,j;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
316 k = 3+i;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
317 j = g0(i+3);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
318 return k+4+j;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
319 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
320
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
321 g0(int i) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
322 return h0(i+4)+i;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
323 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
324
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
325 h0(int i) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
326 return i+4;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
327 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
328 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
329
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
330 It is written in C, we perform CPS transformation in several
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
331 steps by hands. There are several optimization is possible.
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
332
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
333 {\small
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
334 /* straight conversion case (1) */
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
335
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
336 typedef char *stack;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
337
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
338 struct cont_interface {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
339 // General Return Continuation
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
340 __code (*ret)();
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
341 };
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
342
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
343 __code f(int i,stack sp) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
344 int k,j;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
345 k = 3+i;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
346 goto f_g0(i,k,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
347 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
348
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
349 struct f_g0_interface {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
350 // Specialized Return Continuation
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
351 __code (*ret)();
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
352 int i_,k_,j_;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
353 };
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
354
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
355 __code f_g1(int j,stack sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
356
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
357 __code f_g0(int i,int k,stack sp) { // Caller
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
358 struct f_g0_interface *c =
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
359 (struct f_g0_interface *)(
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
360 sp -= sizeof(struct f_g0_interface));
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
361
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
362 c->ret = f_g1;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
363 c->k_ = k;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
364 c->i_ = i;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
365
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
366 goto g(i+3,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
367 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
368
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
369 __code f_g1(int j,stack sp) { // Continuation
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
370 struct f_g0_interface *c =
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
371 (struct f_g0_interface *)sp;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
372 int k = c->k_;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
373 sp+=sizeof(struct f_g0_interface);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
374 c = (struct f_g0_interface *)sp;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
375 goto (c->ret)(k+4+j,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
376 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
377
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
378 __code g_h1(int j,stack sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
379
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
380 __code g(int i,stack sp) { // Caller
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
381 struct f_g0_interface *c =
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
382 (struct f_g0_interface *)(
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
383 sp -= sizeof(struct f_g0_interface));
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
384
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
385 c->ret = g_h1;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
386 c->i_ = i;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
387
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
388 goto h(i+3,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
389 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
390
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
391 __code g_h1(int j,stack sp) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
392 // Continuation
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
393 struct f_g0_interface *c =
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
394 (struct f_g0_interface *)sp;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
395 int i = c->i_;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
396 sp+=sizeof(struct f_g0_interface);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
397 c = (struct f_g0_interface *)sp;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
398 goto (c->ret)(j+i,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
399 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
400
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
401 __code h(int i,stack sp) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
402 struct f_g0_interface *c =
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
403 (struct f_g0_interface *)sp;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
404 goto (c->ret)(i+4,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
405 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
406
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
407 struct main_continuation {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
408 // General Return Continuation
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
409 __code (*ret)();
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
410 __code (*main_ret)();
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
411 void *env;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
412 };
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
413
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
414 __code main_return(int i,stack sp) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
415 if (loop-->0)
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
416 goto f(233,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
417 printf("#0103:%d\n",i);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
418 goto (( (struct main_continuation *)sp)->main_ret)(0),
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
419 ((struct main_continuation *)sp)->env;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
420 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
421 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
422
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
423 This is awfully long, but it is straight forward. Several forward
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
424 prototyping is necessary, and we find strict prototyping is
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
425 painful in CbC, because we have to use many code segments to
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
426 perform simple thing. CbC is not a language for human, but for
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
427 automatic generation, verification or IDE directed programming.
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
428
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
429 We can shorten the result in this way.
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
430 {\small
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
431 /* little optimized case (3) */
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
432
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
433 __code f2_1(int i,char *sp) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
434 int k,j;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
435 k = 3+i;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
436 goto g2_1(k,i+3,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
437 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
438
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
439 __code g2_1(int k,int i,char *sp) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
440 goto h2_11(k,i+4,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
441 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
442
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
443 __code f2_0_1(int k,int j,char *sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
444 __code h2_1_1(int i,int k,int j,char *sp) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
445 goto f2_0_1(k,i+j,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
446 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
447
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
448 __code h2_11(int i,int k,char *sp) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
449 goto h2_1_1(i,k,i+4,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
450 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
451
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
452 __code f2_0_1(int k,int j,char *sp) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
453 goto (( (struct cont_interface *)
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
454 sp)->ret)(k+4+j,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
455 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
456
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
457 __code main_return2_1(int i,stack sp) {
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
458 if (loop-->0)
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
459 goto f2_1(233,sp);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
460 printf("#0165:%d\n",i);
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
461 goto (( (struct main_continuation *)sp)->main_ret)(0),
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
462 ((struct main_continuation *)sp)->env;
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
463 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
464 }
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
465
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
466 In this example, CPS transformed source is faster than
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
467 original function call form. There are not so much area for the
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
468 optimization in function call form, because function call API
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
469 have to be strict.
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
470 CbC does not need standard call API other than interface which
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
471 is simply a struct and there are no need for register save. (This
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
472 bench mark is designed to require the register save).
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
473
20
203699cf5384 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
474 Here is the result in x86_64 architecture (Table.\ref{tab:gcc,compare}).
19
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
475 is function call. \verb+conv1 2+, \verb+conv1 3+ is optimized CPS transformed
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
476 source.
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
477
11
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
478 \begin{table}[htpb]
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
479 \centering
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
480 \small
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
481 \begin{tabular}{|l|r|r|r|} \hline
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
482 (unit: s) & ./conv1 1 & ./conv1 2 & ./conv1 3 \\ \hline
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
483 GCC -O3(32bit) & 2.52 & 2.34 & 1.53 \\ \hline
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
484 GCC -O3(64bit) & 1.80 & 1.20 & 1.44 \\ \hline
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
485 \end{tabular}
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
486 \caption{Micro-C, GCC bench mark (in sec)}
20
203699cf5384 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
487 \label{tab:gcc,compare}
11
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
488 \end{table}
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
489
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
490
bf3c780d3039 changed to outline format
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
491
19
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
492 --Conclusion
dc62dc1fe059 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 18
diff changeset
493
20
203699cf5384 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
494
203699cf5384 modify compression
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 19
diff changeset
495
21
Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
parents: 20
diff changeset
496