Changes between Version 7 and Version 8 of Proposal1.2


Ignore:
Timestamp:
Jun 15, 2010, 4:22:36 PM (8 years ago)
Author:
sacerdot
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Proposal1.2

    v7 v8  
    4848The interaction is done in several steps. We illustrate them using the quicksort program above.
    4949
    50   1. The user writes her code in C�(see Fig.�[[node6.html#code|2]]) and compiles it with our CerCo (Certified Complexity) compiler.
    51   1. The CerCo compiler outputs both the object code and an annotated copy of the C source (Fig.�[[#annotated|4]]). '''Figure 4:''' Cost annotated C code (generated by the compiler)||  ||
    52   '''Figure 5:''' Automatic inference of cost annotations from assembly code|| ||
     50  1. The user writes her code in C (see Fig.2) and compiles it with our CerCo (Certified Complexity) compiler.
     51  1. The CerCo compiler outputs both the object code and an annotated copy of the C source (Fig.4).
     52
     53     [[Image(img20.png)]]
     54     '''Figure 4:''' Cost annotated C code (generated by the compiler)
     55
     56     '''Figure 5:''' Automatic inference of cost annotations from assembly code|| ||
    5357     ||<tablestyle="width:30%"> C source[[BR]]� [[BR]]`~- void quicksort(t,l,r) {[[BR]] if (l < r) {[[BR]] int i = l + 1;[[BR]] int m = l;[[BR]] int v = t[l];[[BR]] while (i <= r) {[[BR]] if (t[i] < v) { [[BR]] m++; [[BR]] swap(t, i, m); }[[BR]] i++;}[[BR]] swap(t, l, m);[[BR]] quicksort(t, l, m - 1);[[BR]] quicksort(t, m + 1, r);[[BR]]}[[BR]]-~` || || ||<tablestyle="width:30%"> Pseudo-Assembly code[[BR]]� [[BR]]`~- 24: r <- r3[[BR]]29: l <- r2[[BR]]34: cmp l r[[BR]]36: t <- r1[[BR]]3a: jump c4 if l >= r[[BR]]40: i <- l + 1[[BR]]44: r8 <- t[[BR]]48: r7 <- l[[BR]]4b: m <- l[[BR]][[BR]]img20.png[[BR]][[BR]]97: r1 <- t[[BR]]9b: r3 <- m[[BR]]9e: r2 <- l[[BR]]a1: call swap[[BR]]a6: r1 <- t[[BR]]aa: r3 <- m - 0x1[[BR]]af: r2 <- l[[BR]]b2: call quicksort[[BR]]bc: l <- r6[[BR]]bf: call quicksort[[BR]]c4: ret -~` || || ||<tablestyle="width:30%"> Execution Paths[[BR]]� [[BR]]`~- l >= r img21.png [[BR]]24: r <- r3[[BR]]29: l <- r2[[BR]]34: cmp l r[[BR]]36: t <- r1[[BR]]3a: jump c4 if l >= r[[BR]]c4: ret[[BR]]�[[BR]]total: 6 clock cycles[[BR]]�[[BR]]l < r img21.png [[BR]]24: r <- r3[[BR]]29: l <- r2[[BR]]34: cmp l r[[BR]]36: t <- r1[[BR]]3a: jump c4 if l >= r[[BR]]40: i <- l + 1[[BR]]44: r8 <- t[[BR]]48: r7 <- l[[BR]]4b: m <- l[[BR]]while loop[[BR]]97: r1 <- t[[BR]]9b: r3 <- m[[BR]]9e: r2 <- l[[BR]]a1: call swap [[BR]]swap [[BR]]a6: r1 <- t[[BR]]aa: r3 <- m - 0x1[[BR]]af: r2 <- l[[BR]]b2: call quicksort[[BR]]quicksort[[BR]]bc: l <- r6[[BR]]bf: call quicksort[[BR]]quicksort[[BR]]c4: ret[[BR]]�[[BR]]total: 21 clock cycles + function calls -~` || || ||
    5458   Each loop and function body is annotated with the cost of one iteration, along all its possible execution paths. The cost is expressed as a function of the state of the program, which comprises the value of every variable. (In the example, we use a textual annotation for simplicity, but we expect to produce a more structured output.) The leftmost column of Fig.�[[#runs|5]] shows the original source code. Colours are used to relate source code statements with their respective (human readable) assembly instructions, reported in the central column. That assembly was produced by gcc[[footnode.html#foot390|^3^]] with a moderate level of optimizations for an Intel 386 family microprocessor. We used ''l,r,t,v'' and ''m'' to mention locations (registers and/or stack frame temporaries) in which the corresponding C variables are placed, while ''r1,...,r9'' are other register or temporaries that have no direct mapping to C. The calling convention puts the first three parameters in ''r1,r2'' and ''r3'', and it is up to the callee to eventually store them in local temporaries. Assignment is denoted with `<-`, addition and multiplication with `+` and `*`; the jump instruction is followed by the target address, and when the jump is conditional a C like expression follows (but its evaluation is performed early by the `cmp` instruction, that sets a CPU flag recording the result of the comparison). The only tricky expression is ```*(r8 + r7 * 4)`'', that exploits an advanced addressing mechanism corresponding to array indexing (4 is the size of an array cell in bytes, ''r7'' is the index and ''r8'' is the address at which the array starts). It amounts to the C statement ```t[l]`'' that computes the pivot.The rightmost column shows two possible execution paths, with a precise estimation of their cost (here 6 and 21 CPU cycles plus the cost of function calls) and the algebraic conditions characterizing these paths.More precisely