Changes between Version 10 and Version 11 of Proposal1.2
 Timestamp:
 Jun 15, 2010, 6:08:14 PM (10 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

Proposal1.2
v10 v11 62 62 3. The user computes (by hand or semiautomatically) 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 63 [[Image(img29.png)]] 64  '''Figure 6:''' Invariants annotated C code. The invariants are user provided. 64  '''Figure 6:''' Invariants annotated C code. The invariants are user provided. 65 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 ''rl'' 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 ''(rl)*(rl)''. The coefficients are those returned by the costannotating compiler. Similarly, the user has to give a complexity invariant for the inner while loop. 66 4. The user and compiler annotated C code is fed into an already existing tool (in this example, Caduceus, [[[node60.html#caduceusFilli�tre and March�]]]) that produces one complexity obligation for each execution path (Fig.7). 65 67 [[Image(img30.png)]] 66 68 '''Figure 7:''' Complexity obligations (automatically generated). The user should prove every complexity obligation. 67 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 ''rl'' 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 ''(rl)*(rl)''. The coefficients are those returned by the costannotating compiler. Similarly, the user has to give a complexity invariant for the inner while loop. 68 4. The user and compiler annotated C code is fed into an already existing tool (in this example, Caduceus, [[[node60.html#caduceusFilli�tre and March�]]]) that produces one complexity obligation for each execution path (Fig.�[[#obligations7]]). 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 adhoc procedure. For instance, to prove the complexity obligations of Fig.�[[#obligations7]], 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. 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 adhoc procedure. For instance, to prove the complexity obligations of Fig. 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. 70 70 71 The right part of Fig. �[[#interaction3]]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 adhoc proof generator to produce a machinechecked 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.71 The right part of Fig.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 adhoc proof generator to produce a machinechecked 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. 72 72 73 73 [[BR]]