Changeset 3437 for Papers


Ignore:
Timestamp:
Feb 14, 2014, 7:56:01 PM (5 years ago)
Author:
campbell
Message:

Deal more directly with some reviewer's comments.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3436 r3437  
    120120by combining user annotations (e.g. preconditions and invariants) with a
    121121multitude of automated analyses (invariant generators, type systems, abstract
    122 interpretation, theorem proving, and so on). By contrast, non-functional properties
    123 are generally checked on low-level object code, but also demand information
     122interpretation, theorem proving, and so on). By contrast, many non-functional properties
     123are generally checked on low-level object code,
     124%\footnote{A notable
     125%  exception is the explicit allocation of heap space in languages like C, which
     126%  can be handled at the source level.}
     127but also demand information
    124128about high-level functional behaviour that must somehow be reconstructed.
    125129
     
    134138the estimates.
    135139
    136 \paragraph{Vision and approach.} We want to reconcile functional and
     140\paragraph{Vision and approach.}
     141 We want to reconcile functional and
    137142non-functional analyses: to share information and perform both at the same time
    138143on source code.
     
    159164components.
    160165
    161 \paragraph{Contributions.} We have developed what we refer to as \emph{the labelling approach} \cite{labelling}, a
     166\paragraph{Contributions.}
     167We have developed what we refer to as \emph{the labelling approach} \cite{labelling}, a
    162168technique to implement compilers that induce cost models on source programs by
    163169very lightweight tracking of code changes through compilation. We have studied
    164170how to formally prove the correctness of compilers implementing this technique.
    165171We have implemented such a compiler from C to object binaries for the 8051
    166 micro-controller, and verified it in an interactive theorem prover.
     172micro-controller for predicting execution time and stack space usage,
     173and verified it in an interactive theorem prover.  As we are targeting
     174an embedded micro-controller we do not consider dynamic memory allocation.
    167175
    168176To demonstrate source-level verification of costs we have implemented
     
    276284changes to the program architecture.
    277285
    278 \subsection{CerCo}
     286\subsection{CerCo's approach}
    279287
    280288In CerCo we propose a radically new approach to the problem: we reject the idea
     
    300308The CerCo approach has the potential to dramatically improve the state of the
    301309art. By performing control and data flow analyses on the source code, the error
    302 prone translation of invariants is completely avoided. It is in fact performed
    303 by the compiler itself when it induces the cost model on the source language.
    304 Moreover, any available technique for the verification of functional properties
     310prone translation of invariants is completely avoided. Instead, this
     311work is done at the source level using tools of the user's choice.
     312Any available technique for the verification of functional properties
    305313can be immediately reused and multiple techniques can collaborate together to
    306 infer and certify cost invariants for the program. Parametric cost analysis
     314infer and certify cost invariants for the program.  There are no
     315limitations on the types of loops or data structures involved. Parametric cost analysis
    307316becomes the default one, with non-parametric bounds used as a last resort when
    308317trading the complexity of the analysis with its precision. \emph{A priori}, no
     
    10631072
    10641073In addition to the loop-free Lustre code, this method was successfully
    1065 applied to a small range of cryptographic code.  See~\cite{labelling} for more details.
     1074applied to a small range of cryptographic code.  See~\cite{labelling}
     1075for more details.  The example in Section~\ref{sec:workflow} was also
     1076produced using the plug-in.  The variant was calculated automatically
     1077by noticing that \lstinline'j' is a loop counter with maximum value
     1078\lstinline'len'.  The most expensive path through the loop body
     1079($78+136 = 214$) is then multiplied by the number of iterations to
     1080give the cost of the loop.
    10661081
    10671082\paragraph{C programs with pointers.}
Note: See TracChangeset for help on using the changeset viewer.