Changeset 3437
- Timestamp:
- Feb 14, 2014, 7:56:01 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Papers/fopara2013/fopara13.tex
r3436 r3437 120 120 by combining user annotations (e.g. preconditions and invariants) with a 121 121 multitude 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 122 interpretation, theorem proving, and so on). By contrast, many non-functional properties 123 are 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.} 127 but also demand information 124 128 about high-level functional behaviour that must somehow be reconstructed. 125 129 … … 134 138 the estimates. 135 139 136 \paragraph{Vision and approach.} We want to reconcile functional and 140 \paragraph{Vision and approach.} 141 We want to reconcile functional and 137 142 non-functional analyses: to share information and perform both at the same time 138 143 on source code. … … 159 164 components. 160 165 161 \paragraph{Contributions.} We have developed what we refer to as \emph{the labelling approach} \cite{labelling}, a 166 \paragraph{Contributions.} 167 We have developed what we refer to as \emph{the labelling approach} \cite{labelling}, a 162 168 technique to implement compilers that induce cost models on source programs by 163 169 very lightweight tracking of code changes through compilation. We have studied 164 170 how to formally prove the correctness of compilers implementing this technique. 165 171 We have implemented such a compiler from C to object binaries for the 8051 166 micro-controller, and verified it in an interactive theorem prover. 172 micro-controller for predicting execution time and stack space usage, 173 and verified it in an interactive theorem prover. As we are targeting 174 an embedded micro-controller we do not consider dynamic memory allocation. 167 175 168 176 To demonstrate source-level verification of costs we have implemented … … 276 284 changes to the program architecture. 277 285 278 \subsection{CerCo }286 \subsection{CerCo's approach} 279 287 280 288 In CerCo we propose a radically new approach to the problem: we reject the idea … … 300 308 The CerCo approach has the potential to dramatically improve the state of the 301 309 art. By performing control and data flow analyses on the source code, the error 302 prone translation of invariants is completely avoided. I t is in fact performed303 by the compiler itself when it induces the cost model on the source language. 304 Moreover, any available technique for the verification of functional properties310 prone translation of invariants is completely avoided. Instead, this 311 work is done at the source level using tools of the user's choice. 312 Any available technique for the verification of functional properties 305 313 can be immediately reused and multiple techniques can collaborate together to 306 infer and certify cost invariants for the program. Parametric cost analysis 314 infer and certify cost invariants for the program. There are no 315 limitations on the types of loops or data structures involved. Parametric cost analysis 307 316 becomes the default one, with non-parametric bounds used as a last resort when 308 317 trading the complexity of the analysis with its precision. \emph{A priori}, no … … 1063 1072 1064 1073 In 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. 1074 applied to a small range of cryptographic code. See~\cite{labelling} 1075 for more details. The example in Section~\ref{sec:workflow} was also 1076 produced using the plug-in. The variant was calculated automatically 1077 by 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 1080 give the cost of the loop. 1066 1081 1067 1082 \paragraph{C programs with pointers.}
Note: See TracChangeset
for help on using the changeset viewer.