Changes between Version 9 and Version 10 of Proposal1.2


Ignore:
Timestamp:
Jun 15, 2010, 6:04:55 PM (8 years ago)
Author:
sacerdot
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Proposal1.2

    v9 v10  
    4949
    5050  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 
    55      '''Figure 4:''' Cost annotated C code (generated by the compiler)
    56 
    57      [[Image(assembly.png)]]
    58 
    59      '''Figure 5:''' Automatic inference of cost annotations from assembly code
    60 
     51  2. The CerCo compiler outputs both the object code and an annotated copy of the C source (Fig.4).
    6152   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.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
    6253    * The CerCo compiler avoids intra-procedural optimisations and loop optimisations that may change the number of iterations performed in a non trivial way.
    6354    * Some intra-procedural or loop optimisations (like the `while` to `repeat` pre-hoisting optimisation applied by gcc in Fig.�[[#runs|5]]) can be allowed, provided that the compiler records them precisely.
    6455    * Once the assembly code is produced, the assembly-level control flow graph is analysed in order to compute the cost of execution paths. Fig.�[[#runs|5]] shows two of them in the rightmost column; the analysis of the `while` loop has been omitted, but is similar.
    65   1. The user computes (by hand or semi-automatically) the complexity invariants of each cycle and (recursive) function, and he adds them to the C code as special comments[[footnode.html#foot404|^4^]] (Fig.�[[#invariants|6]]). '''Figure 6:''' Invariants annotated C code. The invariants are user provided.|| img28.png ||
    66   '''Figure 7:''' Complexity obligations (automatically generated). The user should prove every complexity obligation.|| img29.png ||
     56     ||[[Image(img20.png)]] ||
     57     ||'''Figure 4:''' Cost annotated C code (generated by the compiler) ||
     58   
     59     || [[Image(assembly.png,1200)]] ||
     60     ||'''Figure 5:''' Automatic inference of cost annotations from assembly code||
     61
     62  3. The user computes (by hand or semi-automatically) the complexity invariants of each cycle and (recursive) function, and he adds them to the C code as special comments[[footnode.html#foot404|^4^]] (Fig.6).
     63  ||[[Image(img29.png)]]||
     64  || '''Figure 6:''' Invariants annotated C code. The invariants are user provided.||
     65  ||[[Image(img30.png)]]||
     66  ||'''Figure 7:''' Complexity obligations (automatically generated). The user should prove every complexity obligation.||
    6767   The quicksort complexity invariant states the maximum number of clock cycles required by its execution on an array delimited by ''l'' and ''r''. Since the procedure can be called with wrong indices (''r<l'') the formula has to take into account that ''r-l'' could be negative using the ''max'' function to raise that difference to zero when needed. The literature suggests that this quicksort implementation (where the pivot ''v'' is chosen deterministically) has a quadratic complexity in the worst case. Cleaning up the formula from multiplicative and additive constants one obtains the expected asymptotic complexity ''(r-l)*(r-l)''. The coefficients are those returned by the cost-annotating compiler. Similarly, the user has to give a complexity invariant for the inner while loop.
    68   1. The user and compiler annotated C code is fed into an already existing tool (in this example, Caduceus, [[[node60.html#caduceus|Filli�tre and March�]]]) that produces one complexity obligation for each execution path (Fig.�[[#obligations|7]]).
    69   1. The user should prove all complexity obligations. The proofs are the certificate that the user provided complexity invariant is correct. In many cases, the obligations can be proved automatically using a general purpose automatic theorem prover or an ad-hoc procedure. For instance, to prove the complexity obligations of Fig.�[[#obligations|7]], we must show that a system of inequations holds, which may be done automatically. When an automatic proof is not possible, the user can resort to an interactive proof.
     68  4. The user and compiler annotated C code is fed into an already existing tool (in this example, Caduceus, [[[node60.html#caduceus|Filli�tre and March�]]]) that produces one complexity obligation for each execution path (Fig.�[[#obligations|7]]).
     69  5. The user should prove all complexity obligations. The proofs are the certificate that the user provided complexity invariant is correct. In many cases, the obligations can be proved automatically using a general purpose automatic theorem prover or an ad-hoc procedure. For instance, to prove the complexity obligations of Fig.�[[#obligations|7]], we must show that a system of inequations holds, which may be done automatically. When an automatic proof is not possible, the user can resort to an interactive proof.
    7070
    7171The right part of Fig.�[[#interaction|3]] describes a planned case study for the automation of the complexity proof. We start with a synchronous program which is compiled to C code. The CerCo compiler then produces suitable cost annotations which are used by an invariant synthesizer to build complexity assertions on the C code. The synthesizer can take advantage of the high level control flow information contained in the source synchronous program. The deductive platform (Caduceus) generates complexity obligations which are passed to an ad-hoc proof generator to produce a machine-checked proof from which we can extract a certified bound on the reaction time of the original synchronous program. The proof generator can also take advantage of the high level information coming from the original source program, and user interaction can be used to drive the generator in critical cases.