# Changeset 3298

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

...

File:
1 edited

### Legend:

Unmodified
 r3296 \begin{frame} \frametitle{Recommendations from the reviewers} In order to not limit the results that can be obtained in the project to processors with very old architectures \ldots the  project partners  should  explicitly  consider  how  the  assumptions  on  the hardware architecture influence the results obtained and in how far these assumptions could be a threat to the validity and generality of the results'' Limiting assumptions for the basic labelling approach: \begin{enumerate} \item \alert{The compiler should not alter significantly the control flow}\\ Loss of precision and/or correctness \item \alert{Existence of a function that associates a cost to each basic block independently from the processor status}\\ Serious loss of precision \end{enumerate} The consortium should concentrate on positioning the project with respect to the state of the art which requires a detailed literature survey. In particular, the consortium should clearly formulate what distinguishes the project from existing work and which results are clear improvements.'' \begin{itemize} \item We got in touch with \alert{other EU projects} active in the area of WCET, in particular EMBounded, PROARTIS, TACLe, PARMERASA, T-CREST, REMS. \item Direct contacts during the \alert{CerCo events} \item It \alert{really helped} in understanding what are the relevant novelties, the possible application scenarios and the weaknesses from the engineering perspective \item More details in D1.4 and the \alert{final presentation} \end{itemize} \end{frame} \begin{frame} \frametitle{Recommendations from the reviewers} Case study for the alteration of control flow:\\ \alert{loop optimizations} (peeling, unrolling) Description:\\ \alert{in peeling/unrolling different iterations are compiled differently and they receive a different cost}. Alternative reading:\\ \alert{after peeling/unrolling the cost of an iteration is a function of the program state (iteration number)}. Symptom:\\ \alert{serious loss of precision} (if we take the maximum cost). Solution sketched at the previous review:\\ \alert{dependent costs: the cost is a function of the state} The consortium should as soon as possible start with the verification of the compiler.'' The reviewers are worried that the whole verification tasks cannot be successfully completed by the end of the third project period.'' \begin{itemize} \item The formal proof for the While language (1st period) was \alert{misleading}: function calls introduce a \alert{much larger set of novel intensional invariants} \item Moreover, the invariants are no longer expressed in terms of static code $\Rightarrow$ complete redesign of the proof strategy \item Had to consider \alert{stack space} too \item \alert{Contingency plan}: focus on the \alert{novel parts} (preservation of non functional properties), also exploiting the \alert{uniform representation of backend languages} \item Proof of preservation of costs \alert{completed up to} proofs\\ of preservation of functional properties \end{itemize} \end{frame} \begin{frame} \frametitle{Recommendations from the reviewers} Case study for advanced hardware features:\\ \alert{cache} Description:\\ \alert{using caches different iterations of a loop are executed with a different cost}. Alternative reading:\\ \alert{using caches the cost of an iteration is a function of the processor state (cache)}. Symptom:\\ \alert{serious loss of precision} (if we take the maximum cost). Solution sketched at the previous review:\\ \alert{dependent costs: the cost is a function of the state} The consortium should develop a code extractor for MATITA which allows obtaining executable code from specifications s.t. an executable version of the trusted CerCo compiler can be automatically generated. This extraction will be crucial to apply the CerCo approach to practical case studies and to present it to industry.'' \vspace{-0.25cm} \begin{itemize} \item \alert{Done} \item Many issues faced on the \alert{quality of the extracted code} (e.g. because of dependent types) (D5.2) \item \alert{Very nice example of very weakly typed extracted code}: opens several nice research directions \begin{itemize} \item Targeting OCaml's new \alert{first class modules} to capture $\Sigma$-types \item Targeting \alert{GADTs} to capture most dependent types \item A new technique to represent \alert{polymorphic variants} and \alert{extensible records} (had to be presented at TYPES'13) \item Targeting GHC \alert{$F_\omega$-like} language (working prototype,\\ does not accept all programs, much harder than expected) \end{itemize} \end{itemize} \end{frame} \begin{frame} \frametitle{Recommendations from the reviewers} The two scenarios are analogous, yet the first is simpler:\\ \begin{enumerate} \item Loop optimization\\ \alert{program state always known and available in the source code}\\ Total precision can be achieved.\\ Problem: are the dependent annotations easy to understand and work with (manually or automatically)? Probably yes \item Cache\\ \alert{\makebox[0pt][l]{cache state only (?) approximated (via abstract interpretation)}}\\ Total precision impossible (?) to achieve\\ Problem: are the dependent annotations easy to understand and work with? Open question \end{enumerate} \end{frame} \begin{frame} \frametitle{Recommendations from the reviewers: action taken} Dr. Paolo Tranquilli hired at UNIBO at month 19 to \begin{itemize} \item Develop the dependent labelling approach (completed) \item Apply it to the loop optimization scenarios (completed) \item Apply it to the cache scenario (to be started) \end{itemize} Theoretical achievement:\\ \alert{dependent labelling approach} and pen\&paper certification of a toy compiler based on it Practical achievement:\\ Branch of all CerCo software (compiler, etc.) that implements \alert{loop optimizations, redundancy elimination, improved constant propagation}. \end{frame} \begin{frame} \frametitle{Recommendations from the reviewers: action taken} \alert{No impact on planning}\\ Dr. Tranquilli and Dr. Boender (Post-Docs) replaced the senior researcher position which was made impossible during the first period.\\ ~\\ \alert{No impact on budget}\\ Minor delays so far on the project plan (Dr. Boender alone is less experienced than the originally expected candidate)\\ The consortium should concentrate on further developing and publishing the dependent labelling approach. In particular, the approach should be extended to further compiler optimizations, apart from loop peeling and hoisting, and be applied to more modern processor architectures, eventually aiming at multi-level caches and pipelines.'' \begin{itemize} \item Dependent labelling \alert{published} at QAPL (journal version in preparation) \item One Post-Doc hired by UNIBO to work on \alert{application of dependent labelling to history sensitive hardware components} (pipelines, caches) \item Outcome in my next talk \end{itemize} \end{frame} \begin{frame} \frametitle{Recommendations from the reviewers} The authors should quickly outline a paper-and-pencil correctness proof for each of the seven stages \ldots in order to allow for an estimation of the complexity and time required''~\\~\\ Done. \begin{itemize} \item This made explicit the need to consider \emph{structured traces}.\\ Not needed in the proof of the toy compiler. \item The overall \alert{effort} required is \alert{consistent} with the person-months allocated to the project. \item The estimation is based on our \alert{judgement of the proof complexity} and on \alert{projections} obtained from code size and coefficients computed from CompCert. \end{itemize} The reviewers required a revision of some deliverables and a few addenda.\\~\\ The new versions and addenda were submitted to the EU as expected. \end{frame} (no significant impact on the schedule): \begin{enumerate} \item At month XXX (+XXX): submission of the \item At month 28: submission of the addenda required by the reviewers. \alert{Done} \item Late delivery of D6.3 (at end of project, planned at month XXX).\\ \item Late delivery of D5.3 (at end of project, planned at 36).\\ Most job completed during the 2nd period, we needed to test it again on the last version of the trusted compiler. \item Late delivery of D6.6 (at end of project, planned at 33).\\ The source code of the Debian packages and the infrastructure for the Live CD were ready on time, but the extracted code was changing because of adjustments to the proofs. Live CD were ready on time, but the extracted code came later and was changing because of adjustments to the proofs. \end{enumerate} \end{frame} During second period: \begin{enumerate} \item \alert{amend} the DoW for administrative reasons (organizational changes in UNIBO) and to \alert{extend the duration to 38 months} \item transmission \alert{pre-financing} to all beneficiaries \item \alert{collecting and checking} partner's \alert{financial information} for the \item gathering all necessary information and submission of \alert{management reports, activity reports and deliverables} \item two sites (UNIBO and UEDIN) are undergoing the \alert{financial auditing} \end{enumerate} \end{frame} \begin{frame} \frametitle{Periodic Meetings} Three project meetings during 2nd period (one planned in DoW): \begin{itemize} \item Project meeting, Edinburgh, February 2011.\\ Two project meetings and two short meetings during 3rd period (one planned in DoW): \begin{itemize} \item Short project meeting, Paris, March 2012.\\ %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. \item Project meeting, Paris, September 2011.\\ \alert{Federated CerCo and Eternal meeting} \item Short project meeting, Tallin, March 2012.\\ At ETAPS, negotiation of the CerCo event at next ETAPS %(for dissemination and to establish co-operation). Review of deliverables due at month 18. Invited speaker from WCET community. \item Implementer's meeting, Edinburgh, November 2011\\ \item Project meeting, Bologna, May 2012\\ %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. \end{itemize} \end{frame} \begin{frame} \begin{tabular}{lrlrr} Pass   & Lines & CompCert & Effort   & Effort \\ Origin &       & ratio    & computed & adjusted \\ \hline Common &  4864 & 4.25 \permil & 20.67 & 17.0 \\ Clight &  1057 & 5.23 \permil & 5.53  &  6.0 \\ Cminor &  1856 & 5.23 \permil & 9.71  & 10.0 \\ RTLabs &  1252 & 1.17 \permil & 1.48  &  5.0 \\ RTL    &   469 & 4.17 \permil & 1.95  &  2.0 \\ ERTL   &   789 & 3.01 \permil & 2.38  & 2.5 \\ LTL    &    92 & 5.94 \permil & 0.55  & 0.5 \\ LIN    &   354 & 6.54 \permil & 2.31  &   1.0 \\ ASM    &   984 & 4.80 \permil & 4.72  &  10.0 \\ \hline Tot co &  4864 & 4.25 \permil & 20.67 & 17.0 \\ Tot fe &  2913 & 5.23 \permil & 15.24 & 16.0 \\ Tot be &  6853 & 4.17 \permil & 13.39 & 21.0 \\ \hline Total           & 14630 & 3.75 \permil & 49.30 & 54.0 \\ \end{tabular} \end{frame} \item Implementer's meeting, Edinburgh, August 2012\\ \end{itemize} \end{frame} \end{document}