Changeset 3122
 Timestamp:
 Apr 11, 2013, 3:55:54 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D6.3/report.tex
r3120 r3122 659 659 int i; 660 660 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; 666 662 res = 1; 667 663 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; 671 665 res = res * i; 672 666 } 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; 677 668 return res; 678 669 } … … 681 672 { 682 673 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; 688 675 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; 693 677 return t; 694 678 } … … 698 682 \end{figure} 699 683 684 \paragraph{Considerations on the instrumentation} 685 The example of instrumentation in the previous paragraph shows that the 686 approach we are proposing exposes at the source level a certain amount 687 of information about the machine behavior. Syntactically, the additional 688 details, are almost entirely confined into the \texttt{\_\_next} and 689 \texttt{\_\_K} functions and they do not affect at all the functional behaviour 690 of the program. In particular, all invariants, proof obligations and proofs 691 that deal with the functional behavior only are preserved. 692 693 The interesting question, then, is what is the impact of the additional 694 details on non functional (intensional) invariants and proof obligations. 695 At the moment, without a working implementation to perform some large scale 696 tests, it is difficult to understand the level of automation that can be 697 achieved and the techniques that are likely to work better without introducing 698 major approximations. In any case, the preliminary considerations of the 699 project 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} 700 731 701 732 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.