Index: /Deliverables/D6.3/report.tex
===================================================================
--- /Deliverables/D6.3/report.tex (revision 3121)
+++ /Deliverables/D6.3/report.tex (revision 3122)
@@ -659,20 +659,11 @@
int i;
int res;
- int k;
- __view = __next(__label,1,__view);
- k = __K(__view,1);
- __cost_incr(k);
- __label = 1;
+ __view = __next(__label,1,__view); __cost_incr(_K(__view,1)); __label = 1;
res = 1;
for (i = 1; i <= n; i = i + 1) {
- __view = __next(__label,2,__view);
- __cost_incr(__K(__view,2));
- __label = 2;
+ __view = __next(__label,2,__view); __cost_incr(__K(__view,2)); __label = 2;
res = res * i;
}
- __view = __next(__label,3,__view);
- k = __K(__view,3);
- __cost_incr(k);
- __label = 3;
+ __view = __next(__label,3,__view); __cost_incr(K(__view,3)); __label = 3;
return res;
}
@@ -681,14 +672,7 @@
{
int t;
- int k;
- __view = __next(__label,0,__view);
- k = __K(__view,0);
- __cost_incr(k);
- __label = 0;
+ __view = __next(__label,0,__view); __cost_incr(__K(__view,0)); __label = 0;
t = fact(10);
- __view = __next(__label,4,__view);
- k = __K(__view,4);
- __cost_incr(k);
- __label = 4;
+ __view = __next(__label,4,__view); __cost_incr(__K(__view,4)); __label = 4;
return t;
}
@@ -698,4 +682,51 @@
\end{figure}
+\paragraph{Considerations on the instrumentation}
+The example of instrumentation in the previous paragraph shows that the
+approach we are proposing exposes at the source level a certain amount
+of information about the machine behavior. Syntactically, the additional
+details, are almost entirely confined into the \texttt{\_\_next} and
+\texttt{\_\_K} functions and they do not affect at all the functional behaviour
+of the program. In particular, all invariants, proof obligations and proofs
+that deal with the functional behavior only are preserved.
+
+The interesting question, then, is what is the impact of the additional
+details on non functional (intensional) invariants and proof obligations.
+At the moment, without a working implementation to perform some large scale
+tests, it is difficult to understand the level of automation that can be
+achieved and the techniques that are likely to work better without introducing
+major approximations. In any case, the preliminary considerations of the
+project remain valid:
+\begin{itemize}
+ \item The task of computing and proving invariants can be simplified,
+ even automatically, trading correctness with precision. For example, the
+ most aggressive approximation simply replaces the cost function
+ \texttt{\_\_K} with the function that ignores the view and returns for each
+ label the maximum cost over all possible views. Correspondingly, the
+ function \texttt{\_\_next} can be dropped since it returns views that
+ are later ignored.
+
+ A more refined possibility consists in approximating the output only on
+ those labels whose jitter is small or for those that mark basic blocks
+ that are executed only a small number of times. By simplyfing the
+ \texttt{\_\_next} function accordingly, it is possible to considerably
+ reduce the search space for automated provers.
+ \item The situation is not worse than what happens with time analysis on
+ the object code (the current state of the art). There it is common practice
+ to analyse larger chunks of execution to minimize the effect of later
+ approximations. For example, if it is known that a loop can be executed at
+ most 10 times, computing the cost of 10 iterations yields a
+ better bound than multiplying by 10 the worst case of a single interation.
+
+ We clearly can do the same on the source level.
+ More generally, every algorithm that works in standard WCET tools on the
+ object code is likely to have a counterpart on the source code.
+ We also expect to be able to do better working on the source code.
+ The reason is that we assume to know more functional properties
+ of the program and more high level invariants, and to have more techniques
+ and tools at our disposal. Even if at the moment we have no evidence to
+ support our claims, we think that this approach is worth pursuing in the
+ long term.
+\end{itemize}
\end{document}