Changeset 801 for Deliverables/addenda


Ignore:
Timestamp:
May 13, 2011, 5:50:24 PM (9 years ago)
Author:
mulligan
Message:

Changes to english in letter.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/addenda/letter.tex

    r800 r801  
    7272The first Scientific Review Report contains several valuable comments and
    7373recommendations by the scientific reviewers. We discuss here the three
    74 main recommendations, committing ourselves on taking them in account during the
     74main recommendations, committing ourselves to taking them in account during the
    7575next project period.
    7676
    7777\begin{enumerate}
    7878\item The reviewers are worried by the possible limitations that derive from
    79  the choice of a very old architecture layout. They recommend to adapt a
     79 the choice of a very old architecture layout. They recommend we adopt a
    8080 modified form of labelling such that basic complexity annotations can be
    8181 obtained from program pieces of larger granularity.
    8282
    8383 We will investigate this issue. In particular, the integration of some WCET
    84  techniques seem to be feasible. For instance, let us consider the use of
    85  a simple abstract interpretation technique to improve accuracy of WCET in
    86  case of caches. The analysis performed on loops associates to each memory
    87  access an abstract value in the three valued domain made of cache-hits,
     84 techniques seem feasible. For instance, let us consider the use of
     85 a simple abstract interpretation technique to improve the accuracy of WCET in
     86 the presence of caches. The analysis performed on loops, associates to each memory
     87 access an abstract value in a three valued domain, consisting of cache-hits,
    8888 cache misses and unknown cache behaviour. With this valuable information, we
    8989 can assign a different cost to each single instruction: while the analysis
    90  is done on a large chunk of code, the cost is finally associated to single
    91  instructions as in our approach. Since our approach is totally parametric
    92  on the function that assigns costs to target instructions, nothing needs
    93  to be changed in this simple case. Realistic tools, however, also use a bound
    94  on the number of loops iteration to augment precision of the analysis.
     90 is done on a large chunk of code, the cost is finally associated with single
     91 instructions, as in our approach. Since our approach is totally parametric
     92 in the function that assigns costs to target instructions, nothing needs
     93 to be changed in this simple case.
     94
     95 Realistic tools, however, also use a bound
     96 on the number of loop iterations to augment precision of the analysis.
    9597 Moreover, they assign different costs to the first iteration of a loop and to
    96  successive ones. In these cases, the problem posed to our approach consists
    97  in formally verifying that bounds specified by the user (or automatically
     98 successive ones. In these cases, the problem posed with our approach consists
     99 of formally verifying that bounds specified by the user (or automatically
    98100 inferred by some invariant generator) on the source code are preserved in the
    99101 target code. We believe that the labelling technique we have adopted should
    100  allow us to accomodate also these invariants. In the following project
     102 allow us to also accomodate these invariants. In the following project
    101103 period we will perform a theoretical investigation of this issue and we will
    102104 evaluate the feasibility of the implementation of a prototype.
    103105
    104 \item The reviewers suggest to quickly outline paper-and-pencil correctness
    105  proofs for each of the seven stages of the compiler in order to allow for an
     106\item The reviewers suggest to quickly outline pencil-and-paper correctness
     107 proofs for each of the seven stages of the compiler in order to establish an
    106108 estimation.
    107109
Note: See TracChangeset for help on using the changeset viewer.