Changeset 3298 for Deliverables/D1.3


Ignore:
Timestamp:
May 16, 2013, 12:51:08 AM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.3/Presentations/WP1-claudio.tex

    r3296 r3298  
    229229\begin{frame}
    230230 \frametitle{Recommendations from the reviewers}
    231   ``In order to not limit the results that can be obtained in the
    232   project to processors with very old architectures \ldots the  project
    233   partners  should  explicitly  consider  how  the  assumptions  on  the
    234   hardware architecture influence the results obtained and in how far these
    235   assumptions could be a threat to the validity and generality of the results''
    236 
    237   Limiting assumptions for the basic labelling approach:
    238   \begin{enumerate}
    239    \item \alert{The compiler should not alter significantly the control flow}\\
    240          Loss of precision and/or correctness
    241    \item \alert{Existence of a function that associates a cost to each basic
    242          block independently from the processor status}\\
    243          Serious loss of precision
    244   \end{enumerate}
     231  ``The consortium should concentrate on positioning the project with
     232    respect to the state of the art which requires a detailed literature
     233    survey. In particular, the consortium should clearly formulate what
     234    distinguishes the project from existing work and which results are
     235    clear improvements.''
     236
     237  \begin{itemize}
     238   \item We got in touch with \alert{other EU projects} active in the area of WCET,
     239         in particular EMBounded, PROARTIS, TACLe, PARMERASA, T-CREST, REMS.
     240   \item Direct contacts during the \alert{CerCo events}
     241   \item It \alert{really helped} in understanding what are the relevant novelties,
     242         the possible application scenarios and the weaknesses
     243         from the engineering perspective
     244   \item More details in D1.4 and the \alert{final presentation}
     245  \end{itemize}
    245246\end{frame}
    246247
    247248\begin{frame}
    248249 \frametitle{Recommendations from the reviewers}
    249  Case study for the alteration of control flow:\\
    250  \alert{loop optimizations} (peeling, unrolling)
    251 
    252  Description:\\
    253 
    254  \alert{in peeling/unrolling different iterations are compiled differently and
    255  they receive a different cost}.
    256 
    257  Alternative reading:\\
    258  \alert{after peeling/unrolling the cost of an iteration is a function of the
    259  program state (iteration number)}.
    260 
    261  Symptom:\\
    262  \alert{serious loss of precision} (if we take the maximum cost).
    263 
    264  Solution sketched at the previous review:\\
    265  \alert{dependent costs: the cost is a function of the state}
     250 ``The consortium should as soon as possible start with the verification of
     251   the compiler.'' ``The reviewers are worried that the whole verification tasks
     252   cannot be successfully completed by the end of the third project period.''
     253
     254  \begin{itemize}
     255   \item The formal proof for the While language (1st period) was \alert{misleading}:
     256    function calls introduce a \alert{much larger set of novel intensional invariants}
     257   \item Moreover, the invariants are no longer expressed in terms of static
     258         code $\Rightarrow$ complete redesign of the proof strategy
     259   \item Had to consider \alert{stack space} too
     260   \item \alert{Contingency plan}: focus on the \alert{novel parts}
     261         (preservation of non functional properties), also exploiting the
     262         \alert{uniform representation of backend languages}
     263   \item Proof of preservation of costs \alert{completed up to} proofs\\
     264         of preservation of functional properties
     265  \end{itemize}
    266266\end{frame}
    267267
    268268\begin{frame}
    269269 \frametitle{Recommendations from the reviewers}
    270  Case study for advanced hardware features:\\
    271  \alert{cache}
    272 
    273  Description:\\
    274  \alert{using caches different iterations of a loop are executed with
    275  a different cost}.
    276 
    277  Alternative reading:\\
    278  \alert{using caches the cost of an iteration is a function of the
    279  processor state (cache)}.
    280 
    281  Symptom:\\
    282  \alert{serious loss of precision} (if we take the maximum cost).
    283 
    284  Solution sketched at the previous review:\\
    285  \alert{dependent costs: the cost is a function of the state}
     270 ``The consortium should develop a code extractor for MATITA which allows
     271obtaining executable code from specifications s.t. an executable
     272version of the trusted CerCo compiler can be automatically generated. This
     273extraction will be crucial to apply the CerCo approach to practical case studies
     274and to present it to industry.''
     275
     276 \vspace{-0.25cm}
     277 \begin{itemize}
     278  \item \alert{Done}
     279  \item Many issues faced on the \alert{quality of the extracted code}
     280        (e.g. because of dependent types) (D5.2)
     281  \item \alert{Very nice example of very weakly typed extracted code}:
     282        opens several nice research directions
     283   \begin{itemize}
     284    \item Targeting OCaml's new \alert{first class modules} to capture $\Sigma$-types
     285    \item Targeting \alert{GADTs} to capture most dependent types
     286    \item A new technique to represent \alert{polymorphic variants} and
     287          \alert{extensible records} (had to be presented at TYPES'13)
     288    \item Targeting GHC \alert{$F_\omega$-like} language (working prototype,\\
     289          does not accept all programs, much harder than expected)
     290   \end{itemize}
     291 \end{itemize}
    286292\end{frame}
    287293
    288294\begin{frame}
    289295 \frametitle{Recommendations from the reviewers}
    290  The two scenarios are analogous, yet the first is simpler:\\
    291  \begin{enumerate}
    292   \item Loop optimization\\
    293    \alert{program state always known and available in the source code}\\
    294    Total precision can be achieved.\\
    295    Problem: are the dependent annotations easy to understand and work with
    296    (manually or automatically)? Probably yes
    297  \item Cache\\
    298    \alert{\makebox[0pt][l]{cache state only (?) approximated (via abstract interpretation)}}\\
    299    Total precision impossible (?) to achieve\\
    300    Problem: are the dependent annotations easy to understand and work
    301    with? Open question
    302  \end{enumerate}
    303 \end{frame}
    304 
    305 \begin{frame}
    306  \frametitle{Recommendations from the reviewers: action taken}
    307  Dr. Paolo Tranquilli hired at UNIBO at month 19 to
    308  \begin{itemize}
    309   \item Develop the dependent labelling approach (completed)
    310   \item Apply it to the loop optimization scenarios (completed)
    311   \item Apply it to the cache scenario (to be started)
    312  \end{itemize}
    313 
    314  Theoretical achievement:\\
    315  \alert{dependent labelling approach} and pen\&paper certification of a toy
    316  compiler based on it
    317 
    318  Practical achievement:\\
    319  Branch of all CerCo software (compiler, etc.) that implements
    320  \alert{loop optimizations, redundancy elimination, improved constant
    321  propagation}.
    322 \end{frame}
    323 
    324 \begin{frame}
    325  \frametitle{Recommendations from the reviewers: action taken}
    326  \alert{No impact on planning}\\
    327  Dr. Tranquilli and Dr. Boender (Post-Docs) replaced the
    328  senior researcher position which was made impossible during the first period.\\
    329  ~\\
    330 
    331  \alert{No impact on budget}\\
    332  Minor delays so far on the project plan (Dr. Boender alone is less experienced
    333  than the originally expected candidate)\\
     296 ``The consortium should concentrate on further developing and publishing
     297the dependent labelling approach. In particular, the approach should be
     298extended to further compiler optimizations, apart from loop peeling and
     299hoisting, and be applied to more modern processor architectures, eventually
     300aiming at multi-level caches and pipelines.''
     301
     302 \begin{itemize}
     303  \item Dependent labelling \alert{published} at QAPL (journal version in preparation)
     304  \item One Post-Doc hired by UNIBO to work on \alert{application of dependent
     305        labelling to history sensitive hardware components} (pipelines, caches)
     306  \item Outcome in my next talk
     307 \end{itemize}
    334308\end{frame}
    335309
    336310\begin{frame}
    337311 \frametitle{Recommendations from the reviewers}
    338  ``The authors should quickly outline a paper-and-pencil correctness proof for
    339    each of the seven stages \ldots in order to allow for an estimation of the
    340    complexity and time required''~\\~\\
    341 
    342  Done.
    343  \begin{itemize}
    344   \item This made explicit the need to consider \emph{structured traces}.\\
    345         Not needed in the proof of the toy compiler.
    346   \item The overall \alert{effort} required is \alert{consistent} with the
    347         person-months allocated to the project.
    348   \item The estimation is based on our \alert{judgement of the proof complexity} and on \alert{projections} obtained from code size and coefficients computed
    349         from CompCert.
    350  \end{itemize}
     312 The reviewers required a revision of some deliverables and a few addenda.\\~\\
     313
     314 The new versions and addenda were submitted to the EU as expected.
    351315\end{frame}
    352316
     
    427391 (no significant impact on the schedule):
    428392 \begin{enumerate}
    429   \item At month XXX (+XXX): submission of the
     393  \item At month 28: submission of the
    430394    addenda required by the reviewers. \alert{Done}
    431   \item Late delivery of D6.3 (at end of project, planned
    432     at month XXX).\\
     395  \item Late delivery of D5.3 (at end of project, planned at 36).\\
     396    Most job completed during the 2nd period, we needed to test it again
     397    on the last version of the trusted compiler.
     398  \item Late delivery of D6.6 (at end of project, planned
     399    at 33).\\
    433400    The source code of the Debian packages and the infrastructure for the
    434     Live CD were ready on time, but the extracted code was changing because
    435     of adjustments to the proofs.
     401    Live CD were ready on time, but the extracted code came later and was
     402    changing because of adjustments to the proofs.
    436403 \end{enumerate}
    437404\end{frame}
     
    478445 During second period:
    479446 \begin{enumerate}
     447  \item \alert{amend} the DoW for administrative reasons (organizational changes
     448        in UNIBO) and to \alert{extend the duration to 38 months}
    480449  \item transmission \alert{pre-financing} to all beneficiaries
    481450  \item \alert{collecting and checking} partner's \alert{financial information} for the
     
    484453  \item gathering all necessary information and submission of \alert{management
    485454   reports, activity reports and deliverables}
     455  \item two sites (UNIBO and UEDIN) are undergoing the \alert{financial
     456        auditing}
    486457 \end{enumerate}
    487458\end{frame}
     
    489460\begin{frame}
    490461 \frametitle{Periodic Meetings}
    491  Three project meetings during 2nd period (one planned in DoW):
    492  \begin{itemize}
    493   \item Project meeting, Edinburgh, February 2011.\\
     462 Two project meetings and two short meetings during 3rd period
     463 (one planned in DoW):
     464 \begin{itemize}
     465  \item Short project meeting, Paris, March 2012.\\
    494466   %Planning; review of decisions taken during implementor's meeting, discussion on the proof strategy and on the actions to be taken as an answer to the reviewer's recommendations.
    495   \item Project meeting, Paris, September 2011.\\
    496    \alert{Federated CerCo and Eternal meeting}
     467  \item Short project meeting, Tallin, March 2012.\\
     468   At ETAPS, negotiation of the CerCo event at next ETAPS
    497469   %(for dissemination and to establish co-operation). Review of deliverables due at month 18. Invited speaker from WCET community.
    498   \item Implementer's meeting, Edinburgh, November 2011\\
     470  \item Project meeting, Bologna, May 2012\\
    499471   %Discussion of issues found in the global proof strategy; introduction of the notion of structured traces and re-planning of the global proof strategy. Integration problems\\ addressed.
    500  \end{itemize}
    501 \end{frame}
    502 
    503 \begin{frame}
    504 \begin{tabular}{lrlrr}
    505 Pass   & Lines & CompCert & Effort   & Effort \\
    506 Origin &       & ratio    & computed & adjusted \\
    507 \hline
    508 Common &  4864 & 4.25 \permil & 20.67 & 17.0 \\
    509 Clight &  1057 & 5.23 \permil & 5.53  &  6.0 \\
    510 Cminor &  1856 & 5.23 \permil & 9.71  & 10.0 \\
    511 RTLabs &  1252 & 1.17 \permil & 1.48  &  5.0 \\
    512 RTL    &   469 & 4.17 \permil & 1.95  &  2.0 \\
    513 ERTL   &   789 & 3.01 \permil & 2.38  & 2.5 \\
    514 LTL    &    92 & 5.94 \permil & 0.55  & 0.5 \\
    515 LIN    &   354 & 6.54 \permil & 2.31  &   1.0 \\
    516 ASM    &   984 & 4.80 \permil & 4.72  &  10.0 \\
    517 \hline
    518 Tot co &  4864 & 4.25 \permil & 20.67 & 17.0 \\
    519 Tot fe &  2913 & 5.23 \permil & 15.24 & 16.0 \\
    520 Tot be &  6853 & 4.17 \permil & 13.39 & 21.0 \\
    521 \hline
    522 Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\
    523 \end{tabular}
    524 \end{frame}
    525 
     472  \item Implementer's meeting, Edinburgh, August 2012\\
     473 \end{itemize}
     474\end{frame}
    526475
    527476\end{document}
Note: See TracChangeset for help on using the changeset viewer.