Changeset 3122


Ignore:
Timestamp:
Apr 11, 2013, 3:55:54 PM (4 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D6.3/report.tex

    r3120 r3122  
    659659  int i;
    660660  int res;
    661   int k;
    662   __view = __next(__label,1,__view);
    663   k = __K(__view,1);
    664   __cost_incr(k);
    665   __label = 1;
     661  __view = __next(__label,1,__view); __cost_incr(_K(__view,1)); __label = 1;
    666662  res = 1;
    667663  for (i = 1; i <= n; i = i + 1) {
    668      __view = __next(__label,2,__view);
    669      __cost_incr(__K(__view,2));
    670      __label = 2;
     664     __view = __next(__label,2,__view); __cost_incr(__K(__view,2)); __label = 2;
    671665    res = res * i;
    672666  }
    673   __view = __next(__label,3,__view);
    674   k = __K(__view,3);
    675   __cost_incr(k);
    676   __label = 3;
     667  __view = __next(__label,3,__view); __cost_incr(K(__view,3)); __label = 3;
    677668  return res;
    678669}
     
    681672{
    682673  int t;
    683   int k;
    684   __view = __next(__label,0,__view);
    685   k = __K(__view,0);
    686   __cost_incr(k);
    687   __label = 0;
     674  __view = __next(__label,0,__view); __cost_incr(__K(__view,0)); __label = 0;
    688675  t = fact(10);
    689   __view = __next(__label,4,__view);
    690   k = __K(__view,4);
    691   __cost_incr(k);
    692   __label = 4;
     676  __view = __next(__label,4,__view); __cost_incr(__K(__view,4)); __label = 4;
    693677  return t;
    694678}
     
    698682\end{figure}
    699683
     684\paragraph{Considerations on the instrumentation}
     685The example of instrumentation in the previous paragraph shows that the
     686approach we are proposing exposes at the source level a certain amount
     687of information about the machine behavior. Syntactically, the additional
     688details, are almost entirely confined into the \texttt{\_\_next} and
     689\texttt{\_\_K} functions and they do not affect at all the functional behaviour
     690of the program. In particular, all invariants, proof obligations and proofs
     691that deal with the functional behavior only are preserved.
     692
     693The interesting question, then, is what is the impact of the additional
     694details on non functional (intensional) invariants and proof obligations.
     695At the moment, without a working implementation to perform some large scale
     696tests, it is difficult to understand the level of automation that can be
     697achieved and the techniques that are likely to work better without introducing
     698major approximations. In any case, the preliminary considerations of the
     699project remain valid:
     700\begin{itemize}
     701 \item The task of computing and proving invariants can be simplified,
     702   even automatically, trading correctness with precision. For example, the
     703   most aggressive approximation simply replaces the cost function
     704   \texttt{\_\_K} with the function that ignores the view and returns for each
     705   label the maximum cost over all possible views. Correspondingly, the
     706   function \texttt{\_\_next} can be dropped since it returns views that
     707   are later ignored.
     708
     709   A more refined possibility consists in approximating the output only on
     710   those labels whose jitter is small or for those that mark basic blocks
     711   that are executed only a small number of times. By simplyfing the
     712   \texttt{\_\_next} function accordingly, it is possible to considerably
     713   reduce the search space for automated provers.
     714 \item The situation is not worse than what happens with time analysis on
     715   the object code (the current state of the art). There it is common practice
     716   to analyse larger chunks of execution to minimize the effect of later
     717   approximations. For example, if it is known that a loop can be executed at
     718   most 10 times, computing the cost of 10 iterations yields a
     719   better bound than multiplying by 10 the worst case of a single interation.
     720
     721   We clearly can do the same on the source level.
     722   More generally, every algorithm that works in standard WCET tools on the
     723   object code is likely to have a counterpart on the source code.
     724   We also expect to be able to do better working on the source code.
     725   The reason is that we assume to know more functional properties
     726   of the program and more high level invariants, and to have more techniques
     727   and tools at our disposal. Even if at the moment we have no evidence to
     728   support our claims, we think that this approach is worth pursuing in the
     729   long term.
     730\end{itemize}
    700731
    701732\end{document}
Note: See TracChangeset for help on using the changeset viewer.