Changeset 3461 for Papers/fopara2013


Ignore:
Timestamp:
Feb 21, 2014, 11:50:26 AM (6 years ago)
Author:
mulligan
Message:

more fiddling

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3460 r3461  
    330330obtained using invariant generators, tools to produce proof obligations from
    331331generated invariants and automatic theorem provers to verify the obligations. If
    332 the automatic provers are able to generate proof traces that can be
     332these tools are able to generate proof traces that can be
    333333independently checked, the only remaining component that enters the trusted code
    334334base is an off-the-shelf invariant generator which, in turn, can be proved
     
    441441\end{tikzpicture}
    442442\end{tabular}
    443 \caption{On the left: code to count the array's elements
    444  that are less than or equal to the threshold. On the right: CerCo's interaction
    445  diagram. CerCo's components are drawn solid.}
     443\caption{On the left: C code to count the number of elements in an array
     444 that are less than or equal to a given threshold. On the right: CerCo's interaction
     445 diagram. Components provided by CerCo are drawn with a solid border.}
    446446\label{test1}
    447447\end{figure}
     
    474474Twelve proof obligations are generated from~\autoref{itest1} (to prove
    475475that the loop invariant holds after one execution if it holds before,
    476 to prove that the whole program execution takes at most 1358 cycles,
    477 etc.).  Note that the synthesised time bound for \lstinline'count',
     476to prove that the whole program execution takes at most 1358 cycles, and so on).  Note that the synthesised time bound for \lstinline'count',
    478477$178+214*(1+\text{\lstinline'len'})$ cycles, is parametric in the length of
    479478the array. The CVC3 prover
     
    10091008soundness does not depend on the cost plugin, which can in
    10101009principle produce any synthetic cost. However, in order to be able to actually
    1011 prove a WCET of a C function, we need to add correct annotations in a way that
     1010prove the WCET of a C function, we need to add correct annotations in a way that
    10121011Jessie and subsequent automatic provers have enough information to deduce their
    10131012validity. In practice this is not straightforward even for very simple programs
     
    10291028The cost annotations added by the CerCo compiler take the form of C instructions
    10301029that update a fresh global variable called the cost variable by a constant.
    1031 Synthesizing a WCET of a C function thus consists of statically resolving an
     1030Synthesizing the WCET of a C function thus consists of statically resolving an
    10321031upper bound of the difference between the value of the cost variable before and
    10331032after the execution of the function, i.e. finding the instructions
Note: See TracChangeset for help on using the changeset viewer.