Changeset 3319

Jun 5, 2013, 7:26:25 PM (4 years ago)

added some more text describing the output pf the cost plugin

1 edited


  • Papers/fopara2013/fopara13.tex

    r3318 r3319  
    206206In order to illustrate the typical workflow we envision, we will
    207207follow what is done on an example program (on the left of \autoref{test1},
    208                                            while on the right a depiction of the workflow can be found).
     208while on the right a depiction of the workflow can be found).
    209209The user writes the C program and feeds it to the Cerco compiler, which outputs
    210 an annotated version of the same program. The annotated program can then be enriched
     210an instrumented version of the same program. The annotated program can then be enriched
    211211with complexity assertions in the style of Hoare logic, that are passed to a deductive
    212212platform (in our case Frama-C). Optionally a part of these assertions can be automatically
    217217\autoref{itest1} shows the result of the process as far as the CerCo part is
    218 concerned. The original code is annotated by two kinds of annotations:
     218concerned. The red lines show the instrumentation of the code as given by the CerCo
     219compiler. We can keep track of the time and stack cost by reasoning on
     220variables added by the instrumentation. \texttt{\_\_cost} holds the clock cycles
     221incurred by executing the compiled program, while \texttt{\_\_stack} and
     222\texttt{\_\_max\_stack} hold respectively the current and maximal stack usage,
     223including the space used up by global variables. We therefore have two kinds of annotations:
    219224time increments (in clock cycles) and stack variations (in bytes). In this particular case
    220225all data (including the return address) is kept in hardware registers, so no stack is used.
    221226The initialisation of the \texttt{\_\_cost} and \texttt{\_\_stack} variables tell respectively
    222227the initialisation time cost (before \texttt{main} is called) and the amount of memory occupied by global data.
    223 The output shown is verified by the automatic prover CVC3 in 8 seconds.
     291The lines in blue in \autoref{itest1} show the output of the Frama-C cost plugin. Of particular interest
     292are the annotations of the \texttt{main} function. Proving those correct (which
     293the automatic prover CVC3 preforms in 8 seconds), together with the results on the
     294CerCo compiler, provides the mechanical proof that the function does not
     295use stack and takes 1228 cycles to run. More complex annotations can outline the
     296dependency of the costs from the function parameters..
    287298\section{Main S\&T results}
    288299We will now review the main S\&T results achieved in the CerCo project. We will address them in the following order:
Note: See TracChangeset for help on using the changeset viewer.